Synthesis of concurrent programs for an atomic read/write model of computation

Methods for mechanically synthesizing concurrent programs from temporal log ic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obv iate the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of these methods in practice, howeve r, is that they produce concurrent programs for models of computation that axe often unrealistic, involving highly centralized system architecture (Ma nna and Wolper), processes with global information about the system state ( Emerson and Clarke), or reactive modules that can read all of their inputs in one atomic step (Anuchitanukul and Manna, and Pnueli and Rosner). Even s imple synchronization protocols based on atomic read/write primitives such as Peterson's solution to the mutual exclusion problem have remained outsid e the scope of practical mechanical synthesis methods. In this paper, we sh ow how to mechanically synthesize in more realistic computational models so lutions to synchronization problems. We illustrate the method by synthesizi ng Peterson's solution to the mutual exclusion problem.