THESE

UNIVERSITE DE NICE-SOPHIA ANTIPOLIS ECOLE DOCTORALE STIC SCIENCES ET TECHNOLOGIES DE L’INFORMATION ET DE LA COMMUNICATION THESE pour obtenir le titre de Docteur en Sciences de l’Universite de Nice-Sophia Antipolis presentee et soutenue par Clement HURLIN Speci cation and Veri cation of Multithreaded Object-Oriented Programs with Separation Logic These dirigee par Marieke HUISMAN soutenue le 14 septembre 2009 Jury: Mr. Lars BIRKEDAL Professeur Rapporteur Mr. Frank PIESSENS Rapp Mr. Claude MARCHE Directeur de recherche President Mme. Tamara REZK Charge de recherche Marieke HUISMAN Professeur assistant Directrice de theseiiResume Cette these developpe (1) un systeme de veri cation en logique de separation pour des pro- grammes a la Java paralleles et (2) de nouvelles analyses utilisant la logique de separation. La logique de separation est une variante de la logique lineaire [50] qui conna^ t un recent succes pour la veri cation de programmes [93, 84, 88]. Dans la litterature, la logique de separation a ete appliquee a des while simples [93], des programmes while paralleles [84], et des programmes objets sequentiels [88]. Ces remarques sont developpees dans l’introduction (chapitre 1). Dans cette these nous continuons ces travaux en adaptant la logique de separation aux programmes objets paralleles similaires a Java. Dans ce but, nous developons de nouvelles regles de veri cation pour les primitives de Java concernant le parallelisme. Pour se faire, nous elaborons un langage modele similaire a Java (chapitre 2) qui sert de base aux chapitres ulterieurs. Ensuite, nous mettons en uvre un systeme de veri cation en logique de separation pour les programmes ecrits dans ce langage modele (chapitre 3). Le chapitre 4 presente des regles de veri cation pour les primitives fork et join. La primitive fork demarre un nouveau thread et la primitive join permet d’attendre la termi- naison d’un thread. Ces primitives sont utilisees par un certain nombre de langages: C++, python, et C]. Le chapitre 5 decrit des regles de veri cation pour les verrous reentrants qui sont utilises en Java. Les verrous reentrants { contrairement aux verrous Posix { peuvent ^etre acquis plusieurs fois. Cette propriete simpli e la t^ache du programmeur mais complique la veri cation. La suite de la these presente trois nouvelles analyses utilisant la logique de separation. Au chapitre 7, nous continuons le travail de Cheon et al. sur les sequences d’appels de methodes autorisees (aka protocoles) [32]. Nous etendons ces travaux aux programmes paralleles et inventons une technique a n de veri er que les speci cations des methodes d’une classe sont conformes au protocole de cette classe. Au chapitre 8, nous developpons un algorithme pour montrer qu’une formule de logique de separation n’en implique pas une autre. Cet algorithme fonctionne de la maniere suivante: etant donne deux formules A et B, la taille des modeles potentiels de A et B est calculee approximativement, puis; si les tailles obtenues sont incompatibles, l’algorithme conclut que A n’implique pas B. Cet algorithme est utile dans les veri cateurs de programmes car ceux-ci doivent souvent decider des implications. En n, au chapitre 9, nous montrons comment paralleliser et optimiser des programmes en observant leurs preuves en logique de separation. Cet algorithme est implante dans l’outil eterlou. Pour nir, au chapitre 10, nous concluons et proposons des pistes pour completer les resultats de la presente these. iiiiv RESUME ET ABSTRACT Mots Cles Speci cation de programmes, veri cation de programmes, logique de separation, oriente- objet, parallelisme, Java, parallelisation automatique.Abstract This thesis develops a veri cation system in separation logic for multithreaded Java pro- grams. In addition, this thesis shows three new analyses based on separation logic. Separation logic is a variant of linear logic [50] that did a recent breakthrough in pro- gram veri cation [93, 84, 88]. In the literature, separation logic has been applied to simple while programs [93], while programs with parallelism [84], and sequential object oriented programs [88]. We complete these works by adapting separation logic to multithreaded object-oriented programs la Java. To pursue this goal, we develop new veri cation rules for Java’s primitives for multi- threading. The basis of our work consists of a model language that we use throughout the thesis (Chapter 2). All our formalisation is based on this model language. First, we propose new veri cation rules for fork and join (Chapter 4). 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 veri cation rules for reentrant locks i.e. Java’s locks (Chapter 5). 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 veri cation harder. Second, we present three new analyses based on separation logic. The rst analysis (Chapter 7) 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 (Chapter 8). 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 veri ers, 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 (Chapter 9). This algorithm is implemented in a tool called terlou. Finally, we conclude and discuss possible future work in Chapter 10. vvi RESUME ET ABSTRACT Keywords Program speci cation, program veri cation, separation logic, object-oriented, multithread- ing, Java, automatic parallelization.Remerciements Avant toute chose, je remercie mon amoureuse. Merci pour tes constants encourage- ments, surtout ces derniers mois : ton amour inconditionnel, malgre la distance, voil a ce qui me pousse. Toi et moi, c’est une these sans conclusion. . . Ces premieres lignes sont aussi dediees a mes parents, qui ne me tiennent pas rancune quand je ne donne pas signe de vie ; mais qui sont toujoursal quand j’ai besoin d’eux, et ce, dans tous les domaines. Scienti quement, mes plus profonds remerciements vont a Christian Haack et Marieke Huisman. Le premier car il a su trier le bon grain de l’ivraie dans mes divagations, il m’a enseigne la rigueur necessaire pour ecrire des preuves de qualite, et il m’a demontre l’importance d’avoir des formalisations claires comme de l’eau de roche. La seconde pour m’avoir appris a ecrire des articles, tout etait a faire, mais gr^ ace a sa patience et a sa diplomatie, j’ai enormement progresse. Je remercie egalement ceux qui m’ont entoure aussi bien scienti quement que sociale- ment. A ce titre, je remercie Gilles Barthe, Yves Bertot, Patrice Chalin, Amir Hossein Ghamarian, Joe Kiniry, Gustavo Petri, Erik Poll, Lo c Pottier, Arend Rensink, Tamara Rezk, Laurence Rideau, et Laurent Thery. Mentions speciales a Benjamin Gregoire, rare combinaison de marcels, de ma^ trise du poulailler, et d’humour ; et Anne Pacalet pour la prodigualite de ses conseils et nos nombreuses discussions. Je n’oublie pas ceux avec qui j’ai passe des moments au boulot et en dehors. Nicolas Julien pour son incroyable perspicacite a travailler juste ce qu’il faut, Radu Grigore, Sylvain Heraud, Alex Summers, et #linux. Merci aussi a celles qui ont un pied dans ce monde et { heureusement { un pied dans la realite : Nathalie Bellesso et Joke Lammerink. En n, il est des in uences qui resonnent en moi comme les plus belles lignes de basse. Leurs mots ou leurs choix m’ont guide : Jacques Ellul, Bernard Charbonneau, et ma princesse. viiviii REMERCIEMENTSContents Resume et Abstract iii Remerciements vii 1 Introduction 1 1.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 This Thesis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2 A Java-like Language 9 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.3 Related Work and Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . 15 3 Separation Logic for a Java-like Language 17 3.1 Logic: Informally . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.1.1 Separation Logic | Formulas as Access Tickets . . . . . . . . . . . 17 3.1.2 Logic | Local Reasoning . . . . . . . . . . . . . . . . . 18 3.1.3 Separation Logic | Abstraction . . . . . . . . . . . . . . . . . . . 19 3.1.4 Logic | Proofs Outlines . . . . . . . . . . . . . . . . . 19 3.2 Separation Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.2.2 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 3.2.3 Resources . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.2.4 Predicate Environments . . . . . . . . . . . . . . . . . . . . . . . . 27 3.2.5 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 3.2.6 Proof Theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.3 Hoare Triples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.4 Veri ed Interfaces and Classes . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.5 Veri ed Programs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 3.6 E