Synthesis of Fault-Tolerant Concurrent Programs

Paul C. Attie, Anish Arora, E. Allen Emerson

Research output: Contribution to journalArticle

44 Scopus citations

Abstract

Methods for mechanically synthesizing concurrent programs from temporal logic specifications obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of extant synthesis methods, however, is that they produce concurrent programs for models of computation that are often unrealistic. In particular, these methods assume completely fault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we show how to mechanically synthesize fault-tolerant concurrent programs for various fault classes. We illustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barrier synchronization problems.

Original languageEnglish (US)
Pages (from-to)125-185
Number of pages61
JournalACM Transactions on Programming Languages and Systems
Volume26
Issue number1
DOIs
StatePublished - Jan 1 2004
Externally publishedYes

Keywords

  • Concurrent programs
  • Fault-tolerance
  • Program synthesis
  • Specification
  • Temporal logic

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Synthesis of Fault-Tolerant Concurrent Programs'. Together they form a unique fingerprint.

  • Cite this