Synthesis of Concurrent Programs for an Atomic Read/Write Model of Computation

Paul C. Attie, E. Allen Emerson

Research output: Contribution to journalArticle

27 Scopus citations

Abstract

Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (Manna 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 simple synchronization protocols based on atomic read/write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods. In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems. We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem.

Original languageEnglish (US)
Pages (from-to)187-242
Number of pages56
JournalACM Transactions on Programming Languages and Systems
Volume23
Issue number2
DOIs
StatePublished - Mar 1 2001
Externally publishedYes

Keywords

  • C.2.4 [Computer-Communication Networks]: Distributed Systems
  • D.1.2 [Programming Techniques]: Automatic Programming
  • D.1.3 [Programming Techniques]: Concurrent Programming
  • D.2.1 [Software Engineering]: Requirements/Specifications

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Synthesis of Concurrent Programs for an Atomic Read/Write Model of Computation'. Together they form a unique fingerprint.

  • Cite this