Illustrating the Use of Vector Clocks in Property Detection: An Example and a Counter-Example
Logical (scalar, vector or matrix) clocks are a powerful mechanism used by a lot of distributed algorithms. This paper is on vector clocks: it surveys their main features and is particularly focused on their power and their limitation. In that sense, this
- PDF / 245,582 Bytes
- 9 Pages / 431 x 666 pts Page_size
- 8 Downloads / 222 Views
1
Introduction
Logical (scalar, vector or matrix) clocks are a powerful mechanism used by a lot of distributed algorithms. This paper is on vector clocks: it surveys their main features and is particularly focused on their power and their limitation. In that sense, this paper complements [5, 6] and may be seen as a critical and practical introduction to vector clocks. The paper is divided into four main sections. Section 2 introduces a model for distributed executions. Section 3 describes vector clocks and their basic properties. Vector clocks are a simple mechanism that allows processes to track causality between the events they produce. Then, Section 4 and Section 5 study two problems related to causality. The first problem consists in detecting a conjunction of stable local predicates. The second problem consists in recognizing the occurrence of a very simple event pattern. It is shown that simple vector clocks are insufficient to solve the second problem which, actually, requires more sophisticated clocks, namely, vector of vector clocks. So, this paper exhibits a frontier between problems that can be solved using simple vector clocks and problems requiring more sophisticated vector clock systems.
2 2.1
Distributed Computations Partially Ordered Set of Events
Distributed Computations A distributed program is made up of n sequential local programs which can communicate and synchronize only by exchanging messages. The execution of a local program gives rise to a sequential process. Let P1 , . . . , Pn be this finite set of processes. We assume that, at run-time, each ordered pair of communicating processes (Pi , Pj ) is connected by a reliable channel. Message transmission delays are finite but unpredictable, process speeds are positive but arbitrary: the underlying computation model is asynchronous. Partial Order of Events Execution of an internal/send/receive statement produces a corresponding internal/send/receive event. Let exi be the x-th event produced by process Pi . The sequence hi = e1i e2i . . . exi . . . constitutes the history of Pi . Let H be the set of events produced by a distributed computation. This set is structured as a partial order by Lamport’s causal precedence relation [3], denoted “→” and defined as follows: P. Amestoy et al. (Eds.): Euro-Par’99, LNCS 1685, pp. 806–814, 1999. c Springer-Verlag Berlin Heidelberg 1999
Illustrating the Use of Vector Clocks in Property Detection
(i = j ∧ x ≤ y) (local precedence) ∨ y exi → eyj ⇔ (∃m : exi = send(m) ∧ ej = receive(m)) (msg prec. ) z x z z (∃ ek : ei → ek ∧ e k → eyj ) (transitive closure).
807
∨
b = (H, →) constitutes a model of the distributed compuThe partial order H tation it is associated with. Figure 1 depicts a distributed computation where events are denoted by black points. Two events e and f are concurrent (or causally independent) if ¬(e → f ) ∧ ¬(f → e). The causal past of event e is the partially ordered set of events f such that f → e. Similarly, the causal future of event e is the partially ordered set of events f such
Data Loading...
