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 theseiiResume 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 ...
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 theseiiResume
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.
iiiiv 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.
vvi 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.
viiviii REMERCIEMENTSContents
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