Automated Verification of Highly Concurrent Algorithms

Motivation

prog-verif-640x480.pngThe 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.

Expected Results

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.

Approach

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.

Results

Publications

State-space exploration for concurrent algorithms under weak memory orderings. Bengt Jonsson. In SIGARCH Computer Architecture News, volume 36, number 5, pp 65-71, 2008. (DOI).
Using SPIN to model check concurrent algorithms, using a translation from C to Promela. Ke Jiang and Bengt Jonsson. In Proc. 2nd Swedish Workshop on Multi-Core Computing, pp 67-69, Department of Information Technology, Uppsala University, Uppsala, Sweden, 2009. (fulltext).
Monotonic Abstraction: on Efficient Verification of Parameterized Systems. Aziz Abdulla, Giorgio Delzanno, Ben Henda, and Ahmed Rezine. In International Journal of Foundations of Computer Science, volume 20, number 5, pp 779-801, 2009. (DOI).
Constrained monotonic abstraction: A CEGAR for parameterized verification. Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, and Ahmed Rezine. In CONCUR 2010 – Concurrency Theory, volume 6269 of Lecture Notes in Computer Science, pp 86-101, Springer-Verlag, Berlin, 2010. (DOI).
On Yen's path logic for Petri nets. Mohamed Faouzi Atig and Peter Habermehl. In International Journal of Foundations of Computer Science, volume 22, number 4, pp 783-799, 2011. (DOI).
Approximating Petri net reachability along context-free traces. Mohamed Faouzi Atig and Pierre Ganty. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science: FSTTCS 2011, volume 13 of Leibniz International Proceedings in Informatics, pp 152-163, Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2011. (DOI, fulltext).
Computing Optimal Coverability Costs in Priced Timed Petri Nets. Parosh Aziz Abdulla and Mayr Richard. In LICS'2011, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, IEEE Symposium on Logic in Computer Science, pp 399-408, 2011. (DOI).

Presentations, PR, press clippings

  • Presentation at the 21st International Conference on Concurrency Theory Concur 2010

Software

  • CMA: a prototype implementation of the Constrained Monotonic Abstraction technique using interpolation to automatically refine over-approximations of multithreaded programs (contact Ahmed Rezine ).

Staff

Senior: Parosh Abdulla (Contact), Bengt Jonsson, Ahmed Rezine, Mohammed Faouzi Atig, Lukas Holik
Ph.D. students: Frederic Haziza, Cong Quy Trinh, Carl Leonardsson, Jari Stenman, YunYun Zhu.