检索结果-内蒙古大学图书馆

Coordinated cooperative task computing using crash-prone processors with unreliable multicast

JOURNAL OF PARALLEL AND distributed COMPUTING 2017年 109卷 272-285页

作者： Davtyan, Seda De Prisco, Roberto Georgiou, Chryssis Hadjistasi, Theophanis Schwarzmann, Alexander A. Spotify R&D New York NY 10011 USA Univ Salerno I-84084 Fisciano SA Italy Univ Cyprus CY-1678 Nicosia Cyprus Univ Connecticut Storrs CT 06269 USA

This paper presents a new message-passing algorithm, called Do-UM, for distributed cooperative task computing in synchronous settings where processors may crash, and where any multicasts (or broadcasts) performed by crashing processors are unreliable. We specify the algorithm, prove its correctness and analyse its complexity. We show that its worst case available processor steps is S = Theta(t + n log n/log log n + f(n - f)) and that the number of messages sent is less than n (2t + nf/2) where n is the number of processors, t is the number of tasks to be executed and f is the number of failures. To assess the performance of the algorithm in practical scenarios, we perform an experimental evaluation on a planetary-scale distributed platform. This also allows us to compare our algorithm with the currently best algorithm that is, however, explicitly designed to use reliable multicast;the results suggest that our algorithm does not lose much efficiency in order to cope with unreliable multicast. (C) 2017 Elsevier Inc. All rights reserved.

关键词： Task computing fault-tolerant distributed algorithms Crash faults Unreliable multicast

来源：评论

学校读者我要写书评

暂无评论

On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability

On the completeness of bounded model checking for threshold-...

引用

25th Conference on Concurrency Theory (CONCUR) held jointly with the 9th International Symposium on Trustworthy Global Computing (TGC) / 8th International IFIP Conference on Theoretical Computer Science (IFIP-TCS)

作者： Konnov, Igor Veith, Helmut Widder, Josef TU Wien Vienna Univ Technol Vienna Austria

ISBN: (纸本)9783662445839

Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDA). Due to state space explosion, applying this technique to distributed algorithms with hundreds of local states is challenging for state-of-the-art model checkers. In this paper, we demonstrate that reachability properties of FTDAs can be verified by bounded model checking. To ensure completeness, we need an upper bound on the distance between states. We show that the diameters of accelerated counter systems of FTDAs, and of their counter abstractions, have a quadratic upper bound in the number of local transitions. Our experiments show that the resulting bounds are sufficiently small to use bounded model checking for parameterized verification of reachability properties of several FTDAs, some of which have not been automatically verified before. (C) 2016 The Authors. Published by Elsevier Inc. This is an open access article under the CC BY license.

关键词： Model checking fault-tolerant distributed algorithms Byzantine faults Computational models

来源：评论

学校读者我要写书评

暂无评论

On the impact of link faults on Byzantine agreement

引用

INFORMATION AND COMPUTATION 2014年 239卷 170-181页

作者： Biely, Martin Vienna Univ Technol Embedded Comp Syst Grp A-1040 Vienna Austria Ecole Polytech Fed Lausanne Lab Syst Repartis CH-1015 Lausanne Switzerland

Agreement problems and their solutions are essential to fault-tolerant distributed computing. Over the years, different assumptions on failures have been considered, but most of these assumptions were focusing on either processes or links. In contrast, we examine a model where both links and processes can fail. In this model we devise a unified lower bound for resilience to both classes of faults. We show that the bound is tight by devising a simple retransmission scheme that allows optimally resilient algorithms to be constructed from well known algorithms by transparently adding link-fault tolerance. Our results show that when considering multiple independent failure modes, resilience bounds are not necessarily additive. (C) 2014 Elsevier Inc. All rights reserved.

关键词： fault-tolerant distributed algorithms Consensus fault models Link faults Byzantine faults

来源：评论

学校读者我要写书评

暂无评论

HEX: scaling honeycombs is easier than scaling clock trees 13

HEX: scaling honeycombs is easier than scaling clock trees

引用

Proceedings of the twenty-fifth annual ACM symposium on Parallelism in algorithms and architectures

作者： Danny Dolev Matthias Függer Christoph Lenzen Martin Perner Ulrich Schmid Hebrew University of Jerusalem Jerusalem Israel Vienna University of Technology Vienna Austria Massachusetts Institute of Technology Cambridge MA USA

ISBN: (纸本)9781450315722

We argue that grid structures are a very promising alternative to the standard approach for distributing a clock signal throughout VLSI circuits and other hardware devices. Traditionally, this is accomplished by a delay-balanced clock tree, which distributes the signal supplied by a single clock source via carefully engineered and buffered signal *** approach, termed HEX, is based on a hexagonal grid with simple intermediate nodes, which both control the forwarding of clock ticks in the grid and supply them to nearby functional units. HEX is Byzantine fault-tolerant, in a way that scales with the grid size, self-stabilizing, and seamlessly integrates with multiple synchronized clock sources, as used in multi-synchronous Globally Synchronous Locally Asynchronous (GALS) architectures. Moreover, HEX guarantees a small clock skew between neighbors even for wire delays that are only moderately balanced. We provide both a theoretical analysis of the worst-case skew and simulation results that demonstrate very small typical skew in realistic runs.

关键词： time distribution in grids byzantine fault-tolerance self-stabilization fault-tolerant distributed algorithms

来源：评论

学校读者我要写书评

暂无评论

Verification of consensus algorithms using satisfiability solving

引用

distributed COMPUTING 2011年第5-6期23卷 341-358页

作者： Tsuchiya, Tatsuhiro Schiper, Andre Osaka Univ Suita Osaka 5650871 Japan Ecole Polytech Fed Lausanne CH-1015 Lausanne Switzerland

Consensus is at the heart of fault-tolerant distributed computing systems. Much research has been devoted to developing algorithms for this particular problem. This paper presents a semi-automatic verification approach for asynchronous consensus algorithms, aiming at facilitating their development. Our approach uses model checking, a widely practiced verification method based on state traversal. The challenge here is that the state space of these algorithms is huge, often infinite, thus making model checking infeasible. The proposed approach addresses this difficulty by reducing the verification problem to small model checking problems that involve only single phases of algorithm execution. Because a phase consists of a small, finite number of rounds, bounded model checking, a technique using satisfiability solving, can be effectively used to solve these problems. The proposed approach allows us to model check several consensus algorithms up to around 10 processes.

关键词： Consensus Model checking fault-tolerant distributed algorithms Formal verification

来源：评论

学校读者我要写书评

暂无评论

The Asynchronous Bounded-Cycle model

引用

THEORETICAL COMPUTER SCIENCE 2011年第40期412卷 5580-5601页

作者： Robinson, Peter Schmid, Ulrich Vienna Univ Technol Embedded Comp Syst Grp E182 2 A-1040 Vienna Austria

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 Theta-Model also works correctly in 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. (C) 2010 Elsevier B.V. All rights reserved.

关键词： fault-tolerant distributed algorithms Partially synchronous models Clock synchronization VLSI

来源：评论

学校读者我要写书评

暂无评论

The Theta-Model: achieving synchrony without clocks

引用

distributed COMPUTING 2009年第1期22卷 29-47页

作者： Widder, Josef Schmid, Ulrich Vienna Univ Technol Embedded Comp Syst Grp E182 2 A-1040 Vienna Austria Ecole Polytech Lab Informat LIX F-91128 Palaiseau France

We present a novel partially synchronous system model, which augments the asynchronous model by a (possibly unknown) bound I similar to on the ratio of longest and shortest end-to-end delays of messages simultaneously in transit. An upper bound on those delays need not exist, however, and even I similar to may hold only after some unknown global stabilization time. I similar to-algorithms are fully message-driven and do not have access to bounded drift local clocks, which makes them particularly suitable for VLSI Systems-on-Chip, for example. In this model, we provide a simulation of (eventually achieved) lock-step rounds, which even works in the presence of Byzantine failures. It follows that most problems in distributed computing have a solution in our model: Using the basic consensus algorithm for partially synchronous systems by Dwork et al. (J ACM 35(2):288-323, 1988), for example, Byzantine consensus can be solved. We also introduce a timing transformation technique that facilitates simple correctness proofs and performance analyses of I similar to-algorithms, and provide a detailed relation of the I similar to-Model to other partially synchronous system models.

关键词： Computing models fault-tolerant distributed algorithms Partially synchronous systems Clocks and time

来源：评论

学校读者我要写书评

暂无评论

IMPOSSIBILITY RESULTS AND LOWER BOUNDS FOR CONSENSUS UNDER LINK FAILURES

引用

SIAM JOURNAL ON COMPUTING 2009年第5期38卷 1912-1951页

作者： Schmid, Ulrich Weiss, Bettina Keidar, Idit Vienna Univ Technol Embedded Comp Syst Grp E182 2 A-1040 Vienna Austria Technion Haifa Dept Elect Engn Technion Haifa Israel

We provide a suite of impossibility results and lower bounds for the required number of processes and rounds for synchronous consensus under transient link failures. Our results show that consensus can be solved even in the presence of O(n(2)) moving omission and/or arbitrary link failures per round, provided that both the number of affected outgoing and incoming links of every process is bounded. Providing a step further toward the weakest conditions under which consensus is solvable, our findings are applicable to a variety of dynamic phenomena such as transient communication failures and end-to-end delay variations. We also prove that our model surpasses alternative link failure modeling approaches in terms of assumption coverage.

关键词： fault-tolerant distributed algorithms consensus transient link failures impossibility results lower bounds assumption coverage analysis

来源：评论

学校读者我要写书评

暂无评论

The Asynchronous Bounded-Cycle Model

The Asynchronous Bounded-Cycle Model

引用

10th International Symposium on Stabilization, Safety and Security of distributed Systems (SSS 2008)

作者： Robinson, Peter Schmid, Ulrich Vienna Univ Technol Embedded Comp Syst Grp E182 2 A-1040 Vienna Austria

ISBN: (纸本)9783540893349

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 any global constraints on communication 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 easily be implemented and proved correct in the ABC model, even in the presence of Byzantine failures. We also prove that any algorithm working correctly in the partially synchronous Theta-Model also works correctly in the ABC model. Finally, we relate our model to the classic partially synchronous model, and discuss aspects of its applicability in real systems.

关键词： fault-tolerant distributed algorithms partially synchronous models clock synchronization

来源：评论

学校读者我要写书评

暂无评论

FIT-IT Project DARTS: distributed fault-tolerant clock generation.

引用

ELEKTROTECHNIK UND INFORMATIONSTECHNIK 2007年第1-2期124卷 3-8页

作者： Schmid, U. Steininger, A. Sust, M. Tech Univ Wien Inst Tech Informat Embedded Comp Syst Grp Treitlstr 3 A-1040 Vienna Austria Austrian Aerosp GmbH A-1120 Vienna Austria

This paper describes objective and rationale of the award-winning FIT-IT "Embedded Systems'' Project "distributed algorithms for Robust Tick Synchronization'' (DARTS). Within DARTS a fault-tolerant alternative to the conventional clock generation and clock distribution scheme for VLSI chips, systems-on-chip and similar hardware systems is being developed. Rather than globally distributing the clock produced by a single oscillator over an elaborately balanced clock tree, we propose to equip each functional unit with its own local clock generator. This eliminates the "single point of failure'' constituted by a central clock. However, in contrast to the traditional "Globally Asynchronous Locally Synchronous'' (GALS) approach DARTS does not employ oscillators as local clock generators, but rather instances of a distributed algorithm. In this way fault-tolerant generation of globally synchronized local clock signals is accomplished.

关键词： fault-tolerant tick generation clock synchronization fault-tolerant distributed algorithms VLSI systems-on-chip

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：