Compact Course: Dr. Etienne Lozes, ENS Cachan

 

Separation Logic, Heap-Manipulating Programs, and Concurrency

 

4 Lectures in May/June 2010, Room 2002, Main Building, Informatikzentrum, Ahornstr. 55, Aachen

 

Please note the changed times and dates! (Changed 27 Apr 2010)

 

 

The course is open to students of the Research Training Groups "AlgoSyn"

and of the B-IT Research School. Other participants are welcome as well.

 

Hoare-Floyd logic is a well-known proof system for programs based on
so-called Hoare triples of the form {A} p {B}, meaning "if program p
can assume A as it starts, it ensures B as it stops". Separation Logic
is an extension of Hoare-Floyd logic for reasoning about programs. The
main ingredient of separation logic is a second-order connective
called separating conjunction: A*B asserts that the state is composed
of two disjoint parts, one satisfying A, the other satisfying B. This
connective yields a new reading of a Hoare triple {A} p {B}: "if p can
consume A as it starts, then it has enough resources to run safely,
and it produces B as it stops". Less than ten years after its
theoretical foundation, Separation Logic starts to prove, through
impressive automatic tools, to be a successful approach for checking
large low-level C code (Apache, Linux,...), and to nicely handle lots
of small but intricate concurrent algorithms (e.g. lock-free
concurrent data structures). The logical foundations, expressiveness
issues, and decision procedures, have been much clarified since
2000. However, for all of these aspects and others, Separation Logic
is still a very active field of research. This lecture aims at giving
a complete overview of the main ideas and results that were developed
during these first ten years, ranging from logical-theoretic aspects
to programs' design principles, and possibly to present some open
issues.

Lecture 1 - Foundations

In this lecture, we'll introduce the general problem of the
verification of heap-manipulating programs, we will define a simple
programming language and the core of separation logic's proof
system. We'll illustrate it on several examples of standard but subtle
algorithms for recursive data structures, with often a great gain of
conciseness and readability with respect to other formalisms. We'll
discuss semantics issues, so as ways of formally proving that a
well-proved program has some nice properties.

Lecture 2 - Decision procedures

In this lecture, we'll introduce several decision problems with regard
to separation logic, and show how a solution to them is helpful for
verifying heap-manipulating programs with more or less amount of
automation. While discussing these problems, it will be interesting to
consider expressiveness issues, and to look at the extension of
Separation Logic to arbitrary graph, sometimes called  "Spatial
Logic for Graphs". We'll try to give a complete overview of the
results, in particular connections with (monadic) second-order logic,
and explain which decision procedures are used in existing tools.

Lecture 3 - Race-free concurrency

In this lecture, we will extend the core proof system in order to
support synchronization constructs like Hoare monitors, locks,
semaphores, or asynchronous message-passing, for the support of which
separating conjunction allows quite elegant proof rules. This proof Â
system will ensure that proved programs are race-free, in the sense
that a memory cell cannot be accessed by two threads
simultaneously. We will then investigate a weaker notion of race,
where multiple readers are allowed to read (but not write) the same
cell simultaneously, which will drive us to the notion of permission
algebras. We will also consider the problem of distributed memory
leaks, and we will answer it by a notion of communication's contract.



Lecture 4 - Racy concurrency

In this lecture, we will introduce several fine-grained concurrent
algorithms that often rely on parsimonious usage of mutual exclusion,
and often allow races. We will explain the verification challenges
they pose in terms of functional soundness (sequential consistency,
linearizability), progress properties (wait-freedom, lock-freedom,
obstruction-freedom), and the approaches for solving these problems
that are based on Separation Logic. We will in particular extend the
previous proof system with a support for rely-guarantee, and show how
it can be embedded in a permission-based approach called
deny-guarantee.