03.05.15 - 08.05.15, Seminar 15191

Compositional Verification Methods for Next-Generation Concurrency

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.

Motivation

One of the major open problems confronting software developers today is how to cope with the complexity of building and maintaining large-scale concurrent programs. Such programs are increasingly important as a means of taking advantage of parallelism in modern architectures. However, their correctness frequently depends on subtle invariants governing the use of shared mutable data structures, which must take into account the potential interference between different threads accessing the state simultaneously. Just figuring out how to express such invariants at all has proven to be a very challenging problem; even more challenging is how to reason about such invariants locally, i.e. only within the components of the program that absolutely need to know about them.

Fortunately, we are now at a point where verification research has produced the critical foundations needed to tackle this problem: namely, compositional methods, which exploit the inherently modular structure of realistic concurrent programs in order to decompose verification effort along module boundaries. In the last several years, a variety of different but related compositional methods have been developed for verifying complex concurrent programs, including Hoare type theories, Kripke logical-relations models, and modal separation logics. But much work remains to be done. For example, the vast majority of existing methods for concurrency verification assume a sequentially consistent memory model. However, modern hardware implements---and real programs and compilers exploit---much weaker memory models, which enable more efficient reorderings of basic operations. Existing methods apply primarily to the verification of simple safety and partial correctness properties for imperative programs, whereas most large programs involve higher-order features and must also satisfy liveness properties. Grappling with these kinds of limitations is essential if our verification technology is to be relevant to real-world programs running on modern architectures, and as such it poses exciting new research questions that we as a community are just beginning to explore.

In this seminar, we aim to bring together a wide variety of researchers on concurrency verification, as well as leading experts on concurrent software development in both high- and low-level languages. The goal is to facilitate a stimulating interchange between the theory and practice of concurrent programming, and thereby foster the development of compositional verification methods that can scale to handle the realities of next-generation concurrency.

Among the concrete research challenges we hope to investigate in depth during the seminar are the following:

  • What are good ways of reasoning (compositionally) about programs that exploit weak memory semantics?
  • How can we adapt existing (or develop new) compositional techniques for reasoning about liveness properties of concurrent programs?
  • What are the right concurrency abstractions for higher-order concurrent programming idioms? And what is the best way to verify programs that use those abstractions?
  • Can the models and logics developed for reasoning about shared-memory concurrency be adapted to account for message-passing concurrency idioms?
  • Several logics have been developed recently for modeling complex shared-state invariants using more sophisticated forms of auxiliary state based on protocols (or transition systems). What is the relationship between these different approaches?
  • Toward the goal of compositional verification, what is the most useful way to characterize atomicity of concurrent objects?
  • Given the recent progress in compositional methods for verifying complex concurrent programs, can we abstract away common proof patterns that would be suitable for automation?