Compact Course on Separation Logic

Separation Logic, Heap-Manipulating Programs, and Concurrency

Organisation: see Aachen university web site.

Overview

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.

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 problems

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, 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.

À propos du LSV