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 [EC82, MW84, PR89, PR89b, AM94]. 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, i.e., 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 language | English (US) |
---|---|
Pages | 173-182 |
Number of pages | 10 |
DOIs | |
State | Published - 1998 |
Externally published | Yes |
Event | Proceedings of the 1998 17th Annual ACM Symposium on Principles of Distributed Computing - Puerto Vallarta, Mexico Duration: Jun 28 1998 → Jul 2 1998 |
Conference
Conference | Proceedings of the 1998 17th Annual ACM Symposium on Principles of Distributed Computing |
---|---|
City | Puerto Vallarta, Mexico |
Period | 6/28/98 → 7/2/98 |
ASJC Scopus subject areas
- Software
- Hardware and Architecture
- Computer Networks and Communications