Verifying Concurrent Algorithms

In the quest for tractable methods for reasoning about concurrent
algorithms both rely/guarantee logic and separation logic have made
great advances. They both seek to tame, or control, the complexity of
concurrent interactions, but neither is the ultimate approach. Rely-
guarantee copes naturally with interference, but its specifications
are complex because they describe the entire state. Conversely
separation logic has difficulty dealing with interference, but its
specifications are simpler because they describe only the relevant
state that the program accesses.

In this talk, I will describe our recent research on combining ideas
from both rely-guarantee and separation logic.  I will first present
RGSep, a new logic that allows reasoning about fine-grained and non-
blocking concurrent algorithms.  I will then present deny-guarantee a
reformulation of the rely-guarantee method that enables reasoning
about programs with dynamically allocated and deallocated threads.  I
will demonstrate these logics by showing how to verify a series of
concurrent algorithms.