TY - JOUR
T1 - The Asynchronous Bounded-Cycle model
AU - Robinson, Peter
AU - Schmid, Ulrich
N1 - Funding Information:
✩ This research is supported by the Austrian Science Foundation (FWF) projects P17757 and P20529. A preliminary version of this paper (Robinson and Schmid∗ Correspondingauthor.Tel.:+4315880118253;fax:+4315880118297.(2008))receivedthebestpaperawardatSSS’08. E-mail addresses: robinson@ecs.tuwien.ac.at (P. Robinson), s@ecs.tuwien.ac.at (U. Schmid).
PY - 2011/9/16
Y1 - 2011/9/16
N2 - This paper shows how synchrony conditions can be added to the purely asynchronous model in a way that avoids any reference to message delays and computing step times, as well as system-wide constraints on execution patterns and network topology. Our Asynchronous Bounded-Cycle (ABC) model just bounds the ratio of the number of forward-and backward-oriented messages in certain ("relevant") cycles in the space-time diagram of an asynchronous execution. We show that clock synchronization and lock-step rounds can be implemented and proved correct in the ABC model, even in the presence of Byzantine failures. Furthermore, we prove that any algorithm working correctly in the partially synchronous θ-Model also works correctlyin the ABC model. In our proof, we first apply a novel method for assigning certain message delays to asynchronous executions, which is based on a variant of Farkas' theorem of linear inequalities and a non-standard cycle space of graphs. Using methods from point-set topology, we then prove that the existence of this delay assignment implies model indistinguishability for time-free safety and liveness properties. We also introduce several weaker variants of the ABC model, and relate our model to the existing partially synchronous system models, in particular, the classic models of Dwork, Lynch and Stockmayer and the query-response model by Mostefaoui, Mourgaya, and Raynal. Finally, we discuss some aspects of the ABC model's applicability in real systems, in particular, in the context of VLSI Systems-on-Chip.
AB - This paper shows how synchrony conditions can be added to the purely asynchronous model in a way that avoids any reference to message delays and computing step times, as well as system-wide constraints on execution patterns and network topology. Our Asynchronous Bounded-Cycle (ABC) model just bounds the ratio of the number of forward-and backward-oriented messages in certain ("relevant") cycles in the space-time diagram of an asynchronous execution. We show that clock synchronization and lock-step rounds can be implemented and proved correct in the ABC model, even in the presence of Byzantine failures. Furthermore, we prove that any algorithm working correctly in the partially synchronous θ-Model also works correctlyin the ABC model. In our proof, we first apply a novel method for assigning certain message delays to asynchronous executions, which is based on a variant of Farkas' theorem of linear inequalities and a non-standard cycle space of graphs. Using methods from point-set topology, we then prove that the existence of this delay assignment implies model indistinguishability for time-free safety and liveness properties. We also introduce several weaker variants of the ABC model, and relate our model to the existing partially synchronous system models, in particular, the classic models of Dwork, Lynch and Stockmayer and the query-response model by Mostefaoui, Mourgaya, and Raynal. Finally, we discuss some aspects of the ABC model's applicability in real systems, in particular, in the context of VLSI Systems-on-Chip.
KW - Clock synchronization
KW - Fault-tolerant distributed algorithms
KW - Partially synchronous models
KW - VLSI
UR - http://www.scopus.com/inward/record.url?scp=84865704705&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84865704705&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2010.08.001
DO - 10.1016/j.tcs.2010.08.001
M3 - Article
AN - SCOPUS:84865704705
SN - 0304-3975
VL - 412
SP - 5580
EP - 5601
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 40
ER -