Date : 2009
Editeur / Publisher : [S.l.] : [s.n.] , 2009
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : anglais / English
SDL (langage de programmation)
Programmation orientée objets (informatique)
Programmation parallèle (informatique)
Java (langage de programmation)
Résumé / Abstract : First, we develop verification rules in separation logic for primitives concerning multithreading : the primitives fork and join that control how threads start and how threads wait, and the primitive for reentrant locks (locks that can be acquired and released more than once) that are used in Java. Second, we develop three analyses that use separation logic. The first analysis permits to specify sequences of method calls and to verify that they are correct w.r.t. method contracts. The second analysis presents a fast algorithm to disprove entailment between separation logic formulae. The third analysis shows how to parallelize and optimize programs by rewriting their proofs. This thesis develops a verification system in separation logic for multithreaded Java programs. In addition, this thesis shows three new analyses based on separation logic. Separation logic is a variant of linear logic that did a recent breakthrough in program verification. In the literature, separation logic has been applied to simple while programs, while programs with parallelism, and sequential object oriented programs. We complete these works by adapting separation logic to multithreaded object-oriented programs à la Java. To pursue this goal, we develop new verification rules for Java's primitives for multithreading. The basis of our work consists of a model language that we use throughout the thesis. All our formalisation is based on this model language. First, we propose new verification rules for fork and join. Fork starts a new thread while join waits until the receiver thread terminates. Fork and join are used in many mainstream languages including Java, C++, C#, and python. Then, we describe verification rules for reentrant locks i.e. Java's locks. Reentrant locks - as opposed to Posix locks - can be acquired multiple times (and released accordingly). This property eases the programmer's task, but it makes verification harder. Second, we present three new analyses based on separation logic. The first analysis completes Cheon et al.'s work on sequences of allowed method calls (i.e. protocols). We extend this work to multithreaded programs and propose a technique to verify that method contracts comply with class protocols. The second analysis permits to show that a separation logic formula does not entail another formula. This algorithm works as follows: given two formulas A and B, the size of A and B's models is approximated; then if the sizes of models are incompatible, the algorithm concludes that A does not entail B. This algorithm is useful in program verifiers, because they have to decide entailment often. The third analysis shows how to parallelize and optimize programs by looking at their proofs in separation logic. This algorithm is implemented in a tool called éterlou. Finally, we conclude and discuss possible future work.
Résumé / Abstract : En premier lieu, nous développons des règles de vérification en logique de séparation pour les primitives en rapport avec le parallélisme : les primitives fork et join qui contrôlent le départ et l’attente des processus, et les verrous rééentrants qui sont utilisés en Java. En second lieu, nous développons trois analyses utilisant la logique de séparation. La première analyse permet de spécifier les séquences d’appels de méthodes autorisées et de vérifier leur cohérence. La deuxième analyse permet de montrer qu’une formula de logique de séparation n’en implique pas une autre. La troisième analyse montre comment paralléliser et optimiser des programmes en réécrivant leurs preuves. Cette thèse développe un système de vérification en logique de séparation pour des programmes orientés-objets parallèles et de nouvelles analyses utilisant la logique de séparation. La logique de séparation est une variante de la logique linéaire qui connaît un récent succès pour la vérification de programmes. Dans la littérature, la logique de séparation a été appliquée à des programmes while simples, des programmes while parallèles, et des programmes objets séquentiels. Dans cette thèse nous continuons ces travaux en adaptant la logique de séparation aux programmes objets parallèles similaires à Java. Dans ce but, nous développons de nouvelles règles de vérification pour les primitives de Java concernant le parallélisme. Pour se faire, nous élaborons un langage modèle similaire à Java qui sert de base à la première partie de la thèse. Ensuite, nous mettons en œuvre un système de vérification en logique de séparation pour les programmes écrits dans ce langage modèle. Dans la première partie de la thèse, nous proposons des règles de vérification pour les primitives fork et join. La primitive fork démarre un nouveau thread et la primitive join permet d'attendre la terminaison d'un thread. Ces primitives sont utilisées par un certain nombre de langages: Java, C++, python, et C#. Ensuite, nous décrivons des règles de vérification pour les verrous réentrants i.e. les verrous utilisés en Java. Les verrous réentrants – contrairement aux verrous Posix – peuvent être acquis plusieurs fois. Cette propriété simplifie la tâche du programmeur mais complique la vérification. La suite de la thèse présente trois nouvelles analyses utilisant la logique de séparation. La première analyse continue le travail de Cheon et al. sur les séquences d'appels de méthodes autorisées (aka protocoles). Nous étendons ces travaux aux programmes parallèles et inventons une technique afin de vérifier que les spécifications des méthodes d'une classe sont conformes au protocole de cette classe. La deuxième analyse propose un algorithme pour montrer qu'une formule de logique de séparation n'en implique pas une autre. Cet algorithme fonctionne de la manière suivante: étant donné deux formules A et B, la taille des modèles potentiels de A et B est calculée approximativement, puis; si les tailles obtenues sont incompatibles, l'algorithme conclut que A n'implique pas B. Cet algorithme est utile dans les vérificateurs de programmes car ceux-ci doivent souvent décider des implications. Enfin, la troisième analyse montre comment paralléliser et optimiser des programmes en observant leurs preuves en logique de séparation. Cet algorithme est mis en œuvre dans l'outil éterlou. Pour finir, nous concluons et proposons des pistes pour compléter les résultats de la présente thèse.