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

Paul C. Attie, Allen E. Emerson

Research output: Contribution to conferencePaper

Abstract

Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed (cf. [EC82, MW84, PR89, PR89b, AM94]). An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose 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 (cf. [MW84]) or processes with global information about the system state (cf. [EC82]). Even simple synchronization protocols based on atomic read / atomic 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)
Pages111-120
Number of pages10
StatePublished - Jan 1 1996
Externally publishedYes
EventProceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing - Philadelphia, PA, USA
Duration: May 23 1996May 26 1996

Conference

ConferenceProceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing
CityPhiladelphia, PA, USA
Period5/23/965/26/96

Fingerprint

Synchronization
Temporal logic
Specifications
Network protocols

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Cite this

Attie, P. C., & Emerson, A. E. (1996). Synthesis of concurrent systems for an atomic read/atomic write model of computation. 111-120. Paper presented at Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, USA, .

Synthesis of concurrent systems for an atomic read/atomic write model of computation. / Attie, Paul C.; Emerson, Allen E.

1996. 111-120 Paper presented at Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, USA, .

Research output: Contribution to conferencePaper

Attie, PC & Emerson, AE 1996, 'Synthesis of concurrent systems for an atomic read/atomic write model of computation', Paper presented at Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, USA, 5/23/96 - 5/26/96 pp. 111-120.
Attie PC, Emerson AE. Synthesis of concurrent systems for an atomic read/atomic write model of computation. 1996. Paper presented at Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, USA, .
Attie, Paul C. ; Emerson, Allen E. / Synthesis of concurrent systems for an atomic read/atomic write model of computation. Paper presented at Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, USA, .10 p.
@conference{faa9448604b540c8ac02e5e1b8b413b6,
title = "Synthesis of concurrent systems for an atomic read/atomic write model of computation",
abstract = "Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed (cf. [EC82, MW84, PR89, PR89b, AM94]). An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose 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 (cf. [MW84]) or processes with global information about the system state (cf. [EC82]). Even simple synchronization protocols based on atomic read / atomic 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.",
author = "Attie, {Paul C.} and Emerson, {Allen E.}",
year = "1996",
month = "1",
day = "1",
language = "English (US)",
pages = "111--120",
note = "Proceedings of the 1996 15th Annual ACM Symposium on Principles of Distributed Computing ; Conference date: 23-05-1996 Through 26-05-1996",

}

TY - CONF

T1 - Synthesis of concurrent systems for an atomic read/atomic write model of computation

AU - Attie, Paul C.

AU - Emerson, Allen E.

PY - 1996/1/1

Y1 - 1996/1/1

N2 - Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed (cf. [EC82, MW84, PR89, PR89b, AM94]). An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose 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 (cf. [MW84]) or processes with global information about the system state (cf. [EC82]). Even simple synchronization protocols based on atomic read / atomic 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 (cf. [EC82, MW84, PR89, PR89b, AM94]). An important advantage of these synthesis methods is that they obviate the need to manually construct a program and compose 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 (cf. [MW84]) or processes with global information about the system state (cf. [EC82]). Even simple synchronization protocols based on atomic read / atomic 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.

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

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

M3 - Paper

AN - SCOPUS:0029707467

SP - 111

EP - 120

ER -