Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic
Clément Hurlin · 2009
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.