The Asynchronous Bounded-Cycle model

Peter Robinson, Ulrich Schmid

Research output: Contribution to journalArticlepeer-review

4 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)5580-5601
Number of pages22
JournalTheoretical Computer Science
Volume412
Issue number40
DOIs
StatePublished - Sep 16 2011
Externally publishedYes

Keywords

  • Clock synchronization
  • Fault-tolerant distributed algorithms
  • Partially synchronous models
  • VLSI

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'The Asynchronous Bounded-Cycle model'. Together they form a unique fingerprint.

Cite this