Traver: Taming memory models
Traver stands for Transformation Verification. The goal of the Traver project is to help programmers and compiler writers to understand the precise implications of program transformations of concurrent programs. Of particular interest are the effects of relaxed memory models, and how they impact the correctness of translations.
Who cares?
Compiler writers in particular are faced with the challenges of (1) ensuring that optimizations do not alter the program behavior, and (2) correctly expressing language-level synchronization (such as locks, volatiles, or interlocked operations) using hardware-level operations (as supported by the targeted platform).
What can Traver do for you?
The Traver project assists compiler writers and programmers as follows.
- We provide a rigorous theoretical foundation to prove correctness of program transformations.
- We provide a semi-automatic tool to assist with proving or refuting correctness.
Publications
- Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh, Verifying Local Transformations of Concurrent Programs, in CC 2010: International Conference on Compiler Construction, Springer Verlag, 25 March 2010
- Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, and Madanlal Musuvathi, On the Verification Problem for Weak Memory Models, in Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Association for Computing Machinery, Inc., 20 January 2010
- Sebastian Burckhardt, Madanlal Musuvathi, and Vasu singh, Verifying Compiler Transformations for Concurrent Programs, no. MSR-TR-2008-171, November 2008
- S. Burckhardt and M. Musuvathi, Effective Program Verification for Relaxed Memory Models, in Computer-Aided Verification (CAV), Springer Verlag, July 2008
- Sebastian Burckhardt and Madanlal Musuvathi, Memory Model Safety of Programs, July 2008
- Sebastian Burckhardt and Madanlal Musuvathi, Effective Program Verification for Relaxed Memory Models, no. MSR-TR-2008-12, January 2008
