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

Paul C. Attie, E. Allen Emerson

Research output: Contribution to journalArticle

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

Fingerprint

Synchronization
Temporal logic
Specifications
Network protocols

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

Cite this

Synthesis of Concurrent Programs for an Atomic Read/Write Model of Computation. / Attie, Paul C.; Emerson, E. Allen.

In: ACM Transactions on Programming Languages and Systems, Vol. 23, No. 2, 01.03.2001, p. 187-242.

Research output: Contribution to journalArticle

@article{9aac8163ba83462fb0aa92f23ea65cb6,
title = "Synthesis of Concurrent Programs for an Atomic Read/Write Model of Computation",
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.",
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",
author = "Attie, {Paul C.} and Emerson, {E. Allen}",
year = "2001",
month = "3",
day = "1",
doi = "10.1145/383043.383044",
language = "English (US)",
volume = "23",
pages = "187--242",
journal = "ACM Transactions on Programming Languages and Systems",
issn = "0164-0925",
publisher = "Association for Computing Machinery (ACM)",
number = "2",

}

TY - JOUR

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

AU - Attie, Paul C.

AU - Emerson, E. Allen

PY - 2001/3/1

Y1 - 2001/3/1

N2 - 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.

AB - 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.

KW - C.2.4 [Computer-Communication Networks]: Distributed Systems

KW - D.1.2 [Programming Techniques]: Automatic Programming

KW - D.1.3 [Programming Techniques]: Concurrent Programming

KW - D.2.1 [Software Engineering]: Requirements/Specifications

UR - http://www.scopus.com/inward/record.url?scp=0010342818&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0010342818&partnerID=8YFLogxK

U2 - 10.1145/383043.383044

DO - 10.1145/383043.383044

M3 - Article

AN - SCOPUS:0010342818

VL - 23

SP - 187

EP - 242

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 2

ER -