Computer-aided construction of concurrent systems

Virtually all chips today, from high-end to embedded, are being built with multiple processor cores and the number of cores per chip is increasing. To effectively exploit these changes in technology, all future software will have to be concurrent. This poses tremendous challenge for programmers as building correct and efficient concurrent programs is known to be a very difficult problem. In this paper, we briefly survey some of the most recent techniques we have developed for assisting the programmer in automatically building safe and efficient concurrent systems. Our approach takes as input a concurrent program and a specification that the output program should satisfy. It then automatically infers correct and efficient synchronization which is implemented in the final output program. Using our techniques, we have automatically inferred the usage of a range of classic concurrency constructs such as atomic sections, Hoare's conditional critical regions and memory fences in weak memory models. Copyright © 2010 ACM.