Automatic Inference of Synchronization

EPFL IC Tresor talks

by Martin Vechev Current practices for developing correct and efficient concurrent programs are rather limited and error-prone. In practice, manual ad-hoc use of low-level synchronization often leads to programs that are inefficient or incorrect (or both). High-level constructs (e.g. transactional memory) are not clearly easier to use. In this talk I will briefly discuss techniques for automatically inferring correct and efficient synchronization: atomic sections, scheduler control, guards in Hoare’s CCRs, and memory fences in weak memory models. We have implemented these techniques and used them to: create new practical linearizable concurrent data structures, new memory management algorithms, find and automatically correct errors in concurrent programs due to weak memory models. I will then discuss abstraction-guided synthesis of synchronization (an upcoming POPL’10 paper). In this work we combine abstraction interpretation with synchronization inference. We add the symmetrical choice to traditional abstraction refinement: at any step during abstract interpretation, we can refine the abstraction or change the program by adding more synchronization. This means for example that even if the original program is incorrect or unprovable under the abstraction, we may be able to add synchronization to make it provable. Throughout the talk, I will also mention various insights obtained in this work that pertain to concurrency verification, synthesis and program representation in general. (Joint work with Eran Yahav and Greta Yorsh)