Automated Verification of Highly Concurrent Algorithms
The multicore revolution forces software to exploit concurrency for performance. It is likely that application developers will be shielded from the complexity of concurrency, but performance-critical software will exploit the potential parallelism of the underlying architecture. Such highly concurrent software occurs in libraries for concurrent programming, run-time systems, network protocols, operating systems, etc. It will use fine-grained concurrency, avoid locks and other synchronization when possible. These features make it extremely difficult to find its defects and to ensure correctness. The difficulty of reasoning about the vast number of possible interactions between concurrently executing threads implies that testing is insufficient for detecting and reproducing error scenarios, and that new techniques are needed which can comprehensively cover all potential behavior of highly concurrent algorithms.
Long Term Goal
Developing techniques for automatically proving correctness of, and finding the errors in, highly concurrent algorithms and software.
New techniques, and implemented algorithms, that can automatically verify correctness of highly concurrent algorithms and programs, such as the ones found in, e.g., concurrent programming libraries, run-time program platforms, etc.
We will develop powerful techniques, based on model checking and static analysis, for analyzing highly concurrent programs. In particular, we will consider algorithms and tools to perform the following tasks:
- Parametrized verification of systems consisting of arbitrary numbers of components.
- Shape analysis of concurrent programs with dynamic data structures.
- Verification of distributed algorithms and cache coherence protocols.
- A new technique for verifying correctness programs with an unbounded number of threads, in which only configurations with a small number of process need be considered (publications submitted)
- New techniques for inferring that sequences of program statements can be considered atomic (see last publication)
Presentations, PR, press clippings
- Presentation at the 21st International Conference on Concurrency Theory Concur 2010
- CMA: a prototype implementation of the Constrained Monotonic Abstraction technique using interpolation to automatically refine over-approximations of multithreaded programs (contact Ahmed Rezine ).