Implémentation de TimbukLTA et CopsterLTA et expérimentations

Préliminaires : fonctionnement de Copster

Formalisation de la sémantique Java par des règles de réécriture Une description précise de la sémantique Java transformée en règles de réécriture peut être trouvée dans [Boichut et al., 2007]. Copster permet de transformer un programme Java en règles de réécritures modélisant une partie significative de la sémantique du bytecode Java : les piles, les frames, les objets, les références, les méthodes, les tas, les entiers, et également le multithread.

Formalisation des états et des frames

L’état d’une JVM est un terme de la forme IO(st, in, out) où st est l’état d’un programme, in un flux d’entrée et out un flux de sortie. Un état d’un programme Java est un terme de la forme state(f, fs, h, k), avec : 1. f la frame d’exécution courante, qui permet de donner les informations sur la méthode courante exécutée, 2. fs la pile des frames appelées par le programme : quand une nouvelle méthode est appelée, la frame courante est stockée dans la pile des frames et une nouvelle frame courante est appelée, 3. h un tas, pour stocker des objets et des tableaux, i.e. toutes les informations qui ne sont pas locales à l’exécution d’une méthode, 4. k un tas statique, qui permet de stocker les valeurs des champs statiques, i.e. les valeurs qui sont partagées par tous les objets d’une même classe. Une frame est un terme de la forme frame(m, pc, s, l), avec : 1. m un couple (n, c) où n est le nom de la méthode et c sa classe (par exemple, name(foo,A) représente la méthode foo de la classe A), 2. pc le point de programme courant. Soit x le nombre de points du programme p, le point de programme courant est une constante (i.e. d’arité 0) de l’alphabet Fpc(p) = {pp0, pp1, . . . , ppx}. 3. s la pile des opérandes (par exemple stack(a, stack(b, nil)) si les deux valeurs a et b ont été mises en haut de la pile par un push), et 4. l le tableau des variables locales. La référence d’un objet est encodée par le terme loc(c,a) où c est la classe de l’objet référencé, et a un entier permettant de donner la référence de l’objet. Par exemple, loc(foo,succ(zero)) est une référence pointant sur l’objet localisé à l’index 1 du tas de la classe foo. Formalisation des instructions. Pour un point de programme pc donné, dans une méthode m donnée, Copster construit un terme xframe très similaire au terme frame, mais dont l’instruction courante est indiquée explicitement, afin de compiler des étapes intermédiaires. En effet, le rôle des règles frame est simplement d’expliciter l’instruction bytecode de chaque point de programme. Elles dépendent donc du programme que l’on veut modéliser. À l’inverse, les règles xframe que les frame permettent d’appeler sont des règles génériques représentant la sémantique des instructions du bytecode Java, et sont donc indépendantes du programme à modéliser. Comme nous allons le voir dans la suite, les règles xframe sont générées par Copster quelque soit le programme, alors que les règles frame vont être construites selon les instructions que le programme va appeler. EXEMPLE 6.1 Considérons l’opération arithmétique ”300 − 400”. Dans Copster, comme décrit dans [Boichut et al., 2007], cette opération est représentée par le terme xsub(succ300(zero), succ400(zero)), qui se réduit grâce aux règles représentant la soustraction (décrites en 184  figure 6.2), et qui devront être appliquées 300 fois. Cela signifie qu’au point de programme pc = pp1 de la méthode m = name(foo, A), s’il y a le bytecode sub alors la frame bascule en xframe pour pouvoir calculer la soustraction, i.e. appliquer la règle : frame(name(foo, A), pp1, s, l) → xframe(sub, name(foo, A), pp1, s, l). Pour calculer le résultat de la soustraction des deux premiers éléments de la pile, nous devons appliquer la règle : xframe(sub, m, pc, stack(b(stack(a, s))), l) → xframe(xsub(a, b), m, pc, s, l). Une fois que le résultat est calculé grâce à toutes les règles de réécriture de xsub (voir figure 6.2), il est placé en sommet de pile et nous pouvons alors calculer la prochaine opération de la méthode m, i.e. aller au point de programme suivant en appliquant : xframe(result(x), m, pc, s, l) → frame(m, next(pc), stack(x, s), l), next(pp1) → pp2. J Ce même principe de basculement vers une xframe est appliqué pour chaque instruction. EXEMPLE 6.2 Supposons qu’au point de programme suivant de l’exemple 6.1 se trouve l’instruction pop, qui consiste à enlever le premier élément de la pile. Alors la frame va basculer en xframe pour pouvoir exécuter l’instruction, i.e. appliquer la règle : frame(name(foo, A), pp2, s, l) → xframe(pop, name(foo, A), pp2, s, l). L’instruction pop est ensuite exécutée (i.e. on enlève le premier élément de la pile) et on passe au point de programme suivant : xframe(pop, m, pc, stack(x, s0 ), l) → frame(m, next(pc), s0 , l), next(pp2) → pp3. J Étant donné que les entiers de Peano sont utilisés dans Copster pour représenter les entiers, l’évaluation de l’instruction « if » requiert plusieurs règles de réécriture. Par exemple, l’instruction « if a=b then go to the program point x » est encodé par le terme ifEqint(x, a, b), et les règles de la figure 6.3 seront appliquées. Si au point de programme pc de la méthode m nous avons un « if » dont la condition est une égalité entre deux éléments, alors on passe à une xframe possédant l’opération correspondante (un « if » avec une contrainte d’égalité entre les deux premiers éléments de la pile), et allant à un point de programme x si la condition est vérifiée. Alors nous pouvons appliquer la règle xframe(ifACmpEq(x), m, pc, stack(b, stack(a, s)), l) → xframe(ifEqint(x, a, b), m, pc, s, l) .

Intégration du multithread

. La gestion du multithread Java est intégrée dans Copster grâce à quelques règles de réécriture. Un programme est souvent conçu comme une suite (séquentielle) d’instructions. Néanmoins, il est possible de concevoir des programmes où plusieurs tâches se déroulent simultanément, en parallèle. Ces différentes tâches portent le nom de threads et on dit alors que l’application est multithread. Les threads partagent une mémoire commune et peuvent être utilisés pour exécuter plus rapidement une même portion de code. Cependant, pour éviter de quelconques conflits d’accès à la mémoire partagée, et éviter que les données manipulées ne soient altérées, il est possible de restreindre l’accès à certaines zones mémoires à un seul thread à la fois, i.e. réserver l’accès en lecture et en écriture d’un objet à un seul thread. Ceci est effectué en prenant un verrou (ou lock) sur l’objet réservé. Le lock est implémenté en Java par la méthode synchronize(x), où x est l’objet réservé. Cette méthode est suivie de la portion de code dans laquelle l’objet x ne peut être modifié que par un seul thread à la fois. Dans le bytecode Java, cette méthode est modélisée par les instructions : – monitorenter qui dénote l’entrée en section synchronisée et prend un lock sur l’objet en haut de pile de la frame, et – monitorexit pour notifier la fin de la section synchronisée et rendre le lock. Le scheduler (ou ordonnanceur) de thread va permettre de répartir les ressources le plus équitablement possible entre les différents threads. Les threads sont également munis d’opérations de contrôle depuis l’extérieur. En voici quelques exemples : – L’opération t.join() permet de bloquer le thread t jusqu’à l’arrêt d’un autre thread. – L’opération o.wait(), utilisée par un objet o dans la méthode synchronize(o) (pour le même objet) permet à l’objet o de mettre en attente le thread qui exécute l’instruction wait. Il est important de noter que lorsque la méthode wait suspend le thread en cours d’exécution, le lock sur l’objet o est rendu. – L’opération o.notify() permet de relancer un thread suspendu par l’opération o.wait(). – etc. Dans Copster, un thread est modélisé par un terme : thread(loc(c, a), frame(m, pc, s, l), callstack(storedframe(m0 , pc0 , s0 , l0 ), f)) où : 1. loc(c, a) indique la classe du thread (c) et sa référence (a), 2. frame(m, pc, s, l) indique la frame où le thread possède un lock. 3. callstack(storedframe(m0 , pc0 , s0 , l0 ), f) indique la pile d’appel du thread, i.e. la pile des frames que doit exécuter le thread. Étant donné que toutes les instructions sont exécutées par les différents threads, un état du programme Java est désormais modélisé par un terme : state(threadlist(thread(loc, f, cs), threadlist(t, tl)), h, k, tt