Rethinking Compositionality for Concurrent Program Proofs

Classical approaches to reasoning about concurrency are based on reductions to sequential reasoning.  Typical tactics are to reason about the global behavior of the system (commonly employed in model checking) or to reason about the behavior of each thread independently (such as in Owicki-Gries or Rely/Guarantee).  We will discuss a new foundation for reasoning about multi-threaded programs, which breaks from this mold. In the new approach, proof ingredients extracted from a few distinct program behaviors are used as building blocks to a program proof that is free to follow the program control structure when appropriate and break away from it when necessary. Our algorithmic solution to the automated construction of these proofs leverages the power of sequential reasoning similar to the classical techniques, but the sequential reasoning lines need not be drawn at thread boundaries.