Synthesis of fault-tolerant concurrent programs

被引:36
作者
Attie, PC
Arora, A
Emerson, EA
机构
[1] Northeastern Univ, Coll Comp & Informat Sci, Boston, MA 02115 USA
[2] MIT, Comp Sci & Artificial Intelligence Lab, Cambridge, MA 02139 USA
[3] Ohio State Univ, Dept Comp & Informat Sci, Columbus, OH 43210 USA
[4] Univ Texas, Dept Comp Sci, Austin, TX 78712 USA
来源
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2004年 / 26卷 / 01期
关键词
design; languages; reliability; theory; verification; concurrent programs; fault-tolerance; program synthesis; specification; temporal logic;
D O I
10.1145/963778.963782
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:125 / 185
页数:61
相关论文
共 46 条
[1]  
[Anonymous], P 16 ACM S PRINC PRO
[2]  
[Anonymous], 1994, OPERATING SYSTEM CON
[3]  
ANUCHITANUKUL A, 1994, LECT NOTES COMPUTER, V818, P156
[4]   CLOSURE AND CONVERGENCE - A FOUNDATION OF FAULT-TOLERANT COMPUTING [J].
ARORA, A ;
GOUDA, M .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1993, 19 (11) :1015-1027
[5]   Component based design of multitolerant systems [J].
Arora, A ;
Kulkarni, SS .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1998, 24 (01) :63-78
[6]   Wait-free Byzantine consensus [J].
Attie, P .
INFORMATION PROCESSING LETTERS, 2002, 83 (04) :221-227
[7]   Synthesis of concurrent programs for an atomic read/write model of computation [J].
Attie, PC ;
Emerson, EA .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (02) :187-242
[8]   Synthesis of concurrent systems with many similar processes [J].
Attie, PC ;
Emerson, EA .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1998, 20 (01) :51-115
[9]  
ATTIE PC, 1999, LECT NOTES COMPUTER, V1664
[10]  
ATTIE PC, 1996, 15 ANN ACM S PRINC D, P111