We present a framework that takes unsynchronized sequential processes along with a temporal specification of their global concurrent behaviour, and automatically generates a concurrent program with synchronization code ensuring correct global behaviour. The synthesized synchronization code is based on monitors with wait and notify operations on condition variables, and mutual-exclusion locks. Novel aspects of our framework include realistic low-level synchronization implementations, synthesis of both simple coarse-grained synchronization and more complex fine-grained synchronization, and accommodation of both safety and liveness in global correctness properties. The method is fully automatic as well as sound and complete. © 2011 Springer-Verlag.
CITATION STYLE
Emerson, E. A., & Samanta, R. (2011). An algorithmic framework for synthesis of concurrent programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6996 LNCS, pp. 522–530). https://doi.org/10.1007/978-3-642-24372-1_41
Mendeley helps you to discover research relevant for your work.