Automated Verification of Highly Concurrent Algorithms
Motivation
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.
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.
Recent results
- 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)
Publications
. In Formal Aspects of Computing, volume 24, number 4-6, pp 537-554, 2012. (DOI).. 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:postprint
).. 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).. In International Journal of Foundations of Computer Science, volume 22, number 4, pp 783-799, 2011. (DOI).. In CONCUR 2010 – Concurrency Theory, volume 6269 of Lecture Notes in Computer Science, pp 86-101, Springer-Verlag, Berlin, 2010. (DOI).. In International Journal of Foundations of Computer Science, volume 20, number 5, pp 779-801, 2009. (DOI).. In Proc. 2nd Swedish Workshop on Multi-Core Computing, pp 67-69, Department of Information Technology, Uppsala University, Uppsala, Sweden, 2009. (fulltext).. In SIGARCH Computer Architecture News, volume 36, number 5, pp 65-71, 2008. (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.