Skewed Timestamps

Uri Abraham Department of mathematics and computer science Ben-Gurion University, Be’er Sheva, ISRAEL.

January 5, 1996

Abstract

In the well known timestamp algorithm each writing process reads all the registers of the other processes, and then sets a higher timestamp (natural number) to itself. In the ‘skewed algorithm’ only one writing process in each pair reads the other. Categories and Subjects Descriptors: D.2.4 [Software Engineering]: Programs Verification—correctness proofs; F.3.1 [Logic and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs.

1 Preface

Messages are often timestamped. In a fax, the timestamp includes the date and exact time of the day, and in a book only the publication year, but in all cases this information guides the reader in choosing and processing the data. The antiquarian may choose the oldest book, and the student the newest edition, but in the general timestamp protocol the reader (called scanner) returns all the messages in their issuing order. ^{∗}

Neither clocks nor calendars are needed in the Unbounded Timestamp Algorithm (Figure 1) which uses the natural numbers as timestamps. Each writer (called in this protocol Labeler) first reads the registers of all its fellow Labelers and sets its timestamp above all the numbers thus found. A Scanner reads all the Labelers, and orders their messages in accordance with their timestamps. This unbounded protocol stimulated much research, dealing mostly with the problem of devising timestamping systems with only bounded values. (See Israeli and Li [10], and Dolev and Shavit [7].) We will not deal here with this interesting problem but ask another question: to find an unbounded timestamp algorithm in which, for any two Labelers, only one reads the other. Such an algorithm is given in Section 2 and is called “the skewed timestamp algorithm”. Before answering this question, the very notion of “timestamp algorithm” must be specified, so that the answer can be checked against the specifications. We will adapt the formal specifications of “concurrent timestamp system” (ctss) given by LABEL (of value a by Labeler_{i})

∗That the use of timestamps is old and natural is illustrated by ancient ostracons (about 800 BC)

from Sumeria which show how offerings of vin and oil were marked by date, place of origin, and destination.

1. FORALL k ≠ i CONCURRENTLY DO read(Head(k).timestamp; h[k]);

2. Let h[i] be bigger than max{h[k]∥1 ≤ k ≤ n}

3. write(Head(i); ⟨a, h[i]⟩). SCAN

1. FORALL k(1 ≤ k ≤ n) CONCURRENTLY DO read(Head(k), ⟨m[k], h[k]⟩);

2. let < be the ordering on {1, …, n} defined by i < j iff h[i] < h[j] or h[i] = h[j] and i < j;

3. RETURN (m, <).

Figure 1: The unbounded timestamping protocol. Register Head(i) contains two fields: messages, and timestamps.

Dolev and Shavit [7] (and based on Israeli and Li [10]). These specifications will be fully quoted, and a discussion of some of their aspects will explain why we believe in the necessity of using system executions (with functions) in specifying concurrent objects. This is done in section 2 which also describes some notions used in the paper (such as System executions and higher-level and lower-level views). These are from the theory of interprocess communication developed in Lamport [12], and Pratt [13] to which the reader is referred for a fuller treatment.

2 Timestamps and system executions

Concurrent Time Stamp Systems (ctss) were defined by Dolev and Shavit [7] and their definition is quoted below. We omit the references, footnotes, and some explanations which do not properly belong to the definition. Other omissions are indicated with […].

A Concurrent Time Stamp System is an abstract data type shared among n concurrent and completely asynchronous processes. There are two waitfree operations that any process can execute on the ctss, a labeling operation and a scan operation. Assume that each process’ program consists of these two operations, whose execution generates a sequence of elementary operation executions, totally ordered by the precedes relation (denoted “⟶”), and where any number of scan operation executions is allowed between any two labeling operation executions. […] L_{i}^{[k]} denotes process i’s k^{th} execution of a labeling operation, and S_{i}^{[k]} the k^{th} execution of a scan operation (the superscript [k] is used for notation, and is not visible to the processes). A global time model of operation executions is assumed.

With each labeling operation execution L_{i}^{[k]}, a label l_{i}^{[k]} is associated. A scan operation returns a pair (\overline{l}, ≺), where the label view \overline{l} = \{l_{1}^{[k_{1} ]} …, l_{n}^{[k_{n} ]}\} is an ordered set of labels (one per process), and ≺ is an irreflexive total order among them, such that:

P1 ordering: There exists an irreflexive total order ⇒ on the set of labeling operations, such that:

1. precedence: For any pair of labeling operation executions L_{p}^{[a]} and L_{q}^{[b]} (where possibly p = q), if L_{p}^{[a]}⟶L_{q}^{[b]}, then L_{p}^{[a]} ⇒ L_{q}^{[b]}.

2. consistency: For any scan operation execution S_{i}^{[k]} returning (\overline{l}, ≺), l_{p}^{[a]} ≺ l_{q}^{[b]} if and only if L_{p}^{[a]} ⇒ L_{q}^{[b]}.

[…] One should bear in mind that the asynchronous nature of the operations allows situations where a scan overlaps many consecutive labeling operations of other processes. Also, several consecutive scans could possibly be overlapped by a single labeling operation. It is therefore important that a requirement be made that the label view \overline{l} returned by S_{i}^{[k]} be a meaningful one, namely reflecting the ordering among labeling events immediately before or concurrent with the scan, and not just any possible set of labels. This will eliminate uninteresting trivial solutions and introduce a measure of liveness into the system. This requirement is formalized in the following definition, where ^{- - - ->} is the can affect relation of Lamport [12] [That is a^{- - - ->}b if and only if it is not the case that b⟶a.]

P2 regularity: For any label l_{p}^{[a]} in \overline{l} of S_{i}^{[k]}, L_{p}^{[a]}^{- - - ->}S_{i}^{[k]}, and there is no L_{p}^{[b]} such that L_{p}^{[a]}⟶L_{p}^{[b]}⟶S_{i}^{[k]}. […]

P3 monotonicity: For any label l_{p}^{[a]} in \overline{l} of S_{i}^{[k]} there does not exist an S_{j}^{[k′]} with a label l_{p}^{[b]} in its label view \overline{l}′, such that S_{i}^{[k]}⟶S_{j}^{[k′]} and L_{p}^{[b]}⟶L_{p}^{[a]} (possibly i = j).

It seems to me that this definition of ctss is still lacking in rigorousness, and that the following two amendments should be made. First, the structures that the statements P1, P2, and P3 refer to should be formally defined, and, second, the notation l_{i}^{[k]} may lead to some confusion which must be clarified. Let us elaborate these two points.

1. When prime numbers are defined by the formula x is only divisible by x and 1, for example, it is clear that this definition refers to the structure of the natural numbers (with multiplication), but the underlying structure of the statements P1, P2 and P3 is not so clear. To define ctss one needs a first-order language L and a family of structures in this language such that the statements P1, P2, P3 are in this language, and the structures in which these statements hold (that is, the models of P1&P2&P3) indeed are faithful renderings of our intuitive understanding of concurrent time stamp systems. I believe that this process of explication (to use the terminology of Carnap [6]) can be achieved by using system executions as described below.

2. It is not clear whether the labels l_{i}^{[k]} are distinct for different k’s. If yes, that is to say, if k_{1} ≠ k_{2} implies l_{i}^{[k_{1} ]} ≠ l_{i}^{[k_{2} ]}, then the scan operations which return these labels must use unbounded values, and hence this definition is not suitable for bounded time-stamps. If, however, there are only boundedly many possible values of labels, then it must be the case that for some distinct L_{i}^{[k_{1}]} ≠ L_{i}^{[k_{2}]}, l_{i}^{[k_{1} ]} = l_{i}^{[k_{2} ]}. (Because there may be infinitely many labeling operation executions.) If so, then item 2 in P1, and items P2 and P3 are not well-defined, because they assume that we may go from l_{p}^{[a]} back to L_{p}^{[a]}! The solution to this problem is to introduce a function into our system executions which gives for each scan operation execution S_{i}^{[k]}, and index p of a labeler, a labeling operation L_{p}^{[a]}. Suitably specified, this function will describe exactly our intentions.

2.1 System Executions

If some omnipresent agent records the activities of the processes in one run, the result can be abstracted into a mathematical structure of a particular type, called System Execution. Any mathematical structure consists of a universe, relations, and functions on that universe. System executions are two-sorted structures, containing “events” and “fixed” objects. An example of an event is a read or write operation execution, and an example of a fixed object is the value (for example, a number) of an event. While events are extended in time, fixed objects are so called because they are not located in time. A system execution also contains a precedence relation x⟶y, indicating that event x ends before event y begins, and a collection of predicates and functions which are used to describe the properties of the execution. An example of such a predicate is one that tells about an event whether it is a ‘write’ event or not. An example of a function is value(x) that gives for a write or read event its value.

The precedence relation on the events (operation executions) will be modelled by “interval orderings”.

Definition 2.1. Suppose (L, <_{L}) is a linear ordering, and I and J are intervals in L. Define I ≺ J iff ∀x ∈ I ∀y ∈ J(x <_{L} y)

(For concreteness, the intervals can be assumed to be real or rational intervals.) Whatever the linear ordering L is, ≺ is easily seen to be a partial-order that satisfies the following definition:

Definition 2.2. A partial-order (A, <) is called an interval partial-ordering iff for every a, b, c, d ∈ A

(a < b, c ≮ b, c < d) ⇒ a < d.

The following theorem of N. Wiener shows that the concept of interval-ordering captures exactly the class of orderings that interests us. (See Fishburn [9] for proof and details.)

Theorem 2.3. Suppose (A, <) is an interval partial-order. Then (A, <) is isomorphic to a set of intervals of some linear-order, partially ordered with ≺.

Lamport [12] argues that in cases of interest to computer science, the following Finiteness Property should be assumed for ⟶:

For any a ∈ E, {x ∈ E | x^{- - - ->}a}is finite.  (1)

The formal definition of system executions can now be given.

Definition 2.4. A system execution is a structure S = (E, C, ⟶, F) such that (E, ⟶) is an interval ordering that satisfies the finiteness property, C is a set (of ‘fixed objects’), and F is a collection of functions and relations (defined on E ∪ C).

we will write x^{- - - ->}y as a shorthand of ¬(y⟶x). Also, x⟶^{=}y is a shorthand for

x⟶y or x = y.

This definition is indeed too wide and any particular application requires further specification. For example, to model the ctss of Figure 1, a system execution S = (E, C, ⟶, F) has the following objects in C and F:

1. There is in F a map “type” that assigns to each event, x ∈ E, a value, type(x) ∈ C, called “the type of x”. For example, an event can be of type “read (or write) of register Head(i)”. A function “value” (in F) is defined on those events that are of type “read” or “write” events. In the first case, value(r) is called ‘the return value’ of r, and when w ∈ E is a write event, then value(w) is called ‘the value written by w’. For each register, Head(i), there is a specific event of type “write onto Head(i)”, w_{0}, which is called “the initialization write”, and value(w_{0}) is called the “initial value of the register”. We assume that w_{0}⟶x for any other write or read of Head(i).

2. A finite list of process names is assumed in C, and a “membership” relation, ε, may connect events in E to processes’ names. (Here, Labeler_{i}, for 1 ≤ i ≤ n, and Scanner are the processes.) A process is identified with the set of events associated to it; thus we say ‘event e is in process P ’ or (‘P executes e’).

3. The SCAN and LABEL protocols are associated with the processes (the process’s id parameter is passed to the protocol). A process is said then to ‘execute’ its protocol. We leave the exact description of the semantics of the protocols to the reader. It is possible to use a map that takes each event in process P to an instruction in the protocol of P, so that these events together with the value function form an execution of the protocol (this mapping is in F). (The read/write events in P are mapped to read/write instructions, and are also called “operation executions”.)

The definition given here of system executions is a modification of the original definition of Lamport [12]. The reader interested in more details and justifications of our approach (the reason we choose to work with global-time) can consult Ben-David [4] and Abraham, Ben-David, and Magidor [3]. Abraham [1], [2] contain further developments.

To ensure that the protocols achieve a ctss we demand that the registers are serial.

Definition 2.5. Let S = (E, C, ⟶, F) be a system execution, and let R be a register there. We say R is serial in S iff all read and write events on R in E are linearly ordered by ⟶, and there is a function ω ∈ F defined on the read of R events such that for any read of R, r ∈ E,

1. ω(r) is a write onto R,

2. ω(r)⟶r, and there is no write onto R, w, such that ω(r)⟶w⟶r,

3. the value returned by r is the value written by ω(r) (that is value(r) = value(ω(r))).

In particular, 2 implies that every read event is preceded by a write event, so that the first write event (initial event) precedes all read events.

2.2 Higher and Lower-level Views of system executions

Depending on the granularity of its events, a system execution is said to be at a higher or a lower level. So, if the events are the simplest read/write communication events, then the system execution is at the lower level. Higher-level events are formed by collecting several lower-level events. For example, collecting the events of a single complete execution of the LABEL protocol forms a higher-level event which represents a higher-level execution of the LABEL operation (with the appropriate parameter), and collecting all the higher-level executions of the LABEL/SCAN protocol gives the higher-level view of the system execution. The notions of higher and lower-level views of system executions will be defined now formally.

Definition 2.6. Let S = (E, C, ⟶_{S}, F), and H = (H, J, ⟶_{H}, G) be system executions. We say that H is a higher-level view of S (or that S is an implementation of H) if the following holds.

1. Every h ∈ H is a subset of E. (In many cases, {h | h ∈ H} forms a partition of E, and in all cases we demand that the intersection of any infinite subset of H is empty.)

2. For every h, h′ ∈ H,

h⟶_{H}h′ iff ∀e ∈ h ∀e′ ∈ h′ (e⟶_{S}e′).

Sometimes, we even write “h⟶_{H}e” when h is a higher-level event and e is a lower-level event. In this case we mean that, for every x in h, x⟶_{S}e.

It is often necessary to be able to argue about the end of an event X, and to write expressions such as A⟶end(X). When X is represented by an interval, end(X) refers to the right-end of this interval. However, there is no need to bring in time intervals, and we adopt the following convention:

Definition 2.7. In any system execution S, A⟶end(X) is a shorthand for the following:

∀Y ∈ E_{S}(X⟶Y implies A⟶Y).

Observe that A⟶end(B) implies A^{- - - ->}B (otherwise A⟶A holds). Our definition implies that A⟶end(A) is always true.

In a similar fashion, begin(X)⟶A is a shorthand for ∀Y ∈ E_{S} (Y ⟶X implies Y ⟶A).

Lemma 2.8. A⟶X^{- - - ->}B imply A⟶end(B)

\underline{Proof.} Indeed, if B⟶Y then A⟶Y (by the property of Definition 2.2).

2.3 The higher–level language L

Higher and lower level views are quite useful to analyze behavior of protocols, where the lower-level “executes” the protocol, and the higher-level abstracts only those properties that are valuable to the understanding of the system. To apply this division to our protocol, let us first define a language, L, appropriate for higher-level executions of the form H = (E_{H}, C_{H}, ⟶, F_{H}). L consists of the following constants, functions, and predicates.

constants: Scanner, Labeler_{1}, …, Labeler_{n}. (n is a fixed natural number.)

predicates: E, C, ε, message type, [message type]^{n}.

functions: message, messages, <, Ω_{1}, …, Ω_{n}.

The intended meaning of these symbols is the following.

1. The constants Scanner, and Labeler_{i}, for 1 ≤ i ≤ n, are fixed objects (that is, they are interprated as members of C_{H}). These constants are called “processes” and they denote subsets of E_{H}. To do this, the “membership” relation ε is assumed in L, and the relation eεScanner may hold, for example, to denote that e is a scanner event. (The statement that each Labeler_{i} is sequential, for example, may be written as ∀x, y(x, yεLabeler_{i} → (x = y or x⟶y or y⟶x)).) The constant Labeler (with no index) denotes the union of all the Labeler_{i}’s.

2. E(x) denotes that x is an event (that is, interprated as member of E_{H}), C(x) that x is a fixed object, and ⟶ is the precedence relation, of course.

3. message type is a predicate that describes a subset of CH. This is the type of messages written by the Labelers and read by the Scanners. We assume that L can deal with n-tuples of values in message type. The set of such n-tuples is denoted [message type]^{n}. We assume that if s is in [message type]^{n} then expressions such as s[k] exist in L to denote the k-th value of the sequence s.

4. The function message gives to each Labeler event its value. message(L) for a Labeler event L is in message type and is called “the message (data) written by L”.

5. Another function is messages : Scanner → [message type]^{n}. The value messages(S) for a Scanner, S, is an n-tuple, ⟨messages(S)[1], …, messages(S)[n]⟩, of message type. messages(S) is called “the message sequence returned by S”.

6. The function < is defined on Scanner events. <(S) for a Scanner event, S, will be (in G) a linear order of the set of indices {1, …, n}. (It is called “the index order returned by S”. So, the values of < must be in CH, and we assume that L can deal with permutations (or total orderings) of the set of indices).

7. There are n functions, Ω_{i} : Scanner → Labeler_{i}, 1 ≤ i ≤ N. The exact role of these functions will be clarified in the following subsection. Intuitively, Ω_{i}(S) = M means that the Scanner event S “returned” the (value of the) Labeler_{i} event M. These “return” functions eliminate the inaccuracy pointed to in Section 2 in the specifications of Dolev and Shavit.

This ends the description of the language L. The following subsection contains a list of requirements formulated as sentences of L, and any system execution that satisfies these sentences is called a ctss. Then, ctss protocols will be defined as those (and only those) protocols that induce ctss higher-level views.

Definition 2.9. (of system executions ‘induced’ by a protocol) Suppose a protocol, such as the one of Figure 1, consisting of two procedures: LABEL that accepts a parameter a (of message type), and SCAN that returns a pair ⟨\overline{m}, σ⟩ consisting of an n-tuple \overline{m} of messages, and an ordering σ of the index set \{1, …, n\} of the Labelers. Suppose also that a definition of functions Ω_{1}, …, Ω_{n} is given in terms of lower-level events (cf. with the clarification given below). We say that a lower-level and higher-level system executions, S_{1} and S_{2} (respectively), are induced by the protocol iff

1. The language-type of S_{1} is appropriate for the execution of the protocol. The language-type of S_{2} is L. (In particular, the events in S_{2} are partitioned into Scanner and Labeler_{i} events (for 1 ≤ i ≤ n)).

2. Each Scanner event S in S_{2} is also an execution of the SCAN protocol in S_{1}, and each Labeler event in S_{2} (except the initial events) is an execution of the LABEL protocol.

3. The functions message, messages, and < are defined in S_{2} in accordance with the execution S_{1} of the protocol. This means that:

(a) For every Scanner, S, in S_{2} the pair ⟨messages(S), <(S)⟩ (in S_{2}) equals the value returned by S (as an execution of the SCAN protocol in S_{1})).

(b) Likewise, the value message(L) for L in Labeler, as it is defined in S_{2}, equals the value of the parameter a, in S_{1}.

(c) The functions Ω_{i} in S_{2} are induced by the given S_{1} definable relations. (This will be clarified below.)

Let us clarify this definition by defining the lower/higher level views induced by the protocol of Figure 1. So let S_{1} be a lower-level execution of the SCAN/LABEL procedures. (The registers are assumed to be serial, and ω is the function as in Definition 2.5 evidencing that the registers are serial). We have already explained how a higher-level view may be obtained by collecting lower-level events into higher-level SCAN/LABEL events. To expand this higher-level view into a system execution S_{2} such that the pair S_{1}, S_{2} is induced by the protocol, we must interprate the functions and relation symbols of L, to meet the requirements of Definition 2.9. It is obvious how to do that, except for the functions Ω_{i}, for 1 ≤ i ≤ n, which need a definition. For any SCAN event, S, let r ∈ S be the read of register Head(i) (corresponding to the execution of line 1). Then ω(r) is a write onto Head(i), belonging to a unique higher-level Labeler_{i} event M. Then we define Ω_{i}(S) = M.

2.4 Formal definition of concurrent timestamp systems

This subsection contains a list of axioms in the language L which constitutes the ctss specification. (We have in mind a system execution S = (E, C, ⟶, F) which is described by the axioms.) A certain measure of informality is allowed in this specification, and some of the statements are in English rather than in the first-order language L.

seriality: The processes (Scanner and Labeler_{i}, 1 ≤ i ≤ n) are pairwise disjoint.

(That is,

∀x, y(xεScanner & yεLabeler_{1} → x ≠ y)

and likewise for the other indices.) Each process is serial. There are n initial events: Each Labeler_{i} contains a single Initialization event which is the first event there, and any initialization event precedes any non-initial event. (In particular an Initialization event precedes any Scanner event.)

regularity: For each 1 ≤ i ≤ N, Ω_{i} is a regular function from Scanner to Labeler_{i}. That is:

1. Ω_{i}(S)^{- - - ->}S, for every S in Scanner, and

2. there is no Labeler_{i} event W such that Ω_{i}(S)⟶W ⟶S.

monotonicity: If S_{1}⟶S_{2} are in Scanner, then Ω_{p}(S_{2})⟶Ω_{p}(S_{1}) is not possible.

message: For every Scanner event, S, and index 1 ≤ i ≤ N, messages(S)[i] = message(Ω_{i}(S)).

global coherence (ordering): Let us define the following relation, ⇒, on the Labeler events, induced by the permutations <(S), for SεScanner, of the index set {1, …, }. For every Labeler events L and M,

L ⇒ M iff

either L⟶M or else, for some Scanner event S, L = Ω_{i}(S), M = Ω_{j}(S), and i <(S) j.

The global coherence requirement is then that ⇒ can be extended to a linear ordering of all the Labeler events.

In the presence of all other properties, monotonicity can be deduced from the following, which we call “the Bloom property” (see Bloom [5]).

For each SCAN S, and index 1 ≤ i ≤ n, Ω_{i}(S)⟶end(S)

Let us check that the property of Bloom implies monotonicity. So assume that S_{1}⟶S_{2} are in Scanner, but Ω_{p}(S_{2})⟶Ω_{p}(S_{1}). Since Ω_{p}(S_{1})⟶end(S_{1}) and as S_{1}⟶S_{2}, Ω_{p}(S_{1})⟶S_{2} follows. But then, Ω_{p}(S_{2})⟶Ω_{p}(S_{1})⟶S_{2} contradicts the regularity of Ω_{p}.

It may be of some interest to compare what we did so far with the specifications of Dolev and Shavit. Instead of enumerating the events of each process (for example as L_{i}^{[1]}⟶L_{i}^{[2]}⟶ …), we preferred to introduce a predicate Labeler_{i} and to state that it is serial (then, together with the finiteness condition, this implies that the order type of events in Labeler_{i} is either finite or of type ω). This is not an essential change, and the reader may still want to use the notation of Dolev and Shavit (which has a certain appeal) and view L_{i}^{[k]} as a function L(i, k) assigning to every indices i and k (in a certain range) a Labeler_{i} event L(i, k), such that L(i, k + 1) is the successor of L(i, k) (this requires the introduction of the natural numbers into our system execution). Another non-essential change is that we explicitly deal with the messages, or value fields, which Dolev and Shavit deferred to the appendix.

A more substantial change is that a scan operation S in Scanner returns a permutation of the indices, instead of the pair (\overline{l}, ≺). Thus, instead of saying that S ∈ Scanner returned the label view \overline{l} = \{l_{1}^{[k_{1} ]} … l_{n}^{[k_{n} ]}\} and the total order ≺, we would say that Ω_{i}(S) = L_{i}^{[k_{i}]}, and that <(S) is an ordering of the index set that puts i before j exactly when ≺ orders l_{i}^{[k_{i} ]} before l_{j}^{[k_{j} ]}, and that messages(S)[i] equals message(L_{i}^{[k_{i}]}). This way we avoid the problem that, in case of bounded values, it is not possible to find L_{i}^{[k_{i}]} from the value returned by the SCAN.

We are going to see in the next section a protocol that implements operations LABEL and SCAN so that the Timestamp Specifications described above hold.

3 The skewed protocol

The protocol uses n serial registers: Head(i), for 1 ≤ i ≤ n. Each register Head(i) can be written by Labeler_{i}, and read by all Scanners and by higher-indexed Labelers. The values carried by these registers is of type head type described below.

The following data-type are used. message type is the set of values transmitted by the processes. [messages type]^{n} is the set of n-tuples of message type. report type is the set of finite sequences of natural numbers, of length ≤ n. head type is a compound of three types; if h is a value of head type, then:

1. field h.message is in message type,

2. field h.phase is a natural number,

3. field h.report is in report type (of length i, if used by Labeler_{i}).

Since we always have the equality h.phase = h.report[i], for values in Labeler_{i}, two fields suffice, and the allocation of field “phase” is only for our convenience.

The initial values of fields that are numbers may be assumed to be 0. The lexical ordering on the finite sequences of natural numbers is the key ingredient

of our protocol. If s and t are sequences of natural numbers (that is, members of report type) of length l_{s} and l_{t} respectively, then s <_{LEX} t iff either (1) there is some k ≤ l_{s}, l_{t} such that s[k] ≠ t[k] and for the first such k s[k] < t[k], or else (2) there is no such k and l_{s} < l_{t} (in which case s is the restriction of t to the first l_{s} values). The protocol can now be given. LABEL(of message a, by Labeler_{i})

1. forall j < i concurrently do

(a) read(Head(j);h[j]);

(b) head.report[j] := h[j].phase;

2. (a) head.message := a; (b) head.phase := head.phase +1; head.report[i] := head.phase;

3. write(Head(i); head). SCAN

1. forall1 ≤ i ≤ n concurrently do read(Head(i); h[i]);

2. \overline{m} := ⟨h[1].message, …, h[n].message⟩

3. Let σ be the ordering of the index set {1, …, n} defined by iσj iff h[i].report <_{LEX} h[j].report;

4. return⟨\overline{m}, σ⟩

To understand the rationale of the protocol, let us observe the following four points:

(1) Each Labeler_{m} is serial, and the precedence relation is reflected by the phase numbers written onto Head(m) (since the phase number is always increased by 1). (2) This serial order of each Labeler induces a linear ordering on the vectors of the form ⟨L_{1}, …, L_{k}⟩ where L_{m} ∈ Labeler_{m}; we will call this ordering <_{R} (see Definition 3.10 below). (3) Each Labeler_{i} operation execution L reads (concurrently) all the registers with lower indices, and this defines a vector \overline{W} (L) = ⟨L_{1}, …, L_{i−1}, L⟩, of those Labeler_{m} events that determined the values read by L (the last event in this vector is L itself). Thus the linear ordering <_{R} induces a linear ordering on the Labelers. (4) The phase numbers in \overline{W} (L) are written by L in field head.report, and by reading this field, each SCAN can determine the induced ordering on the Labelers, and return this ordering.

If the time–complexity of a protocol is measured in such a way that concurrent executions of read/write instructions are counted as one, then the time complexity of the LABEL protocol is 2, and that of the SCAN protocol is 1.

3.1 Correctness proof

Let S_{1} be any lower-level system execution with serial registers, in which the protocol is executed. So the set of events, E_{1}, of S_{1} consists of the read/write operation executions on the serial registers Head(i). Recall that ω is the “return” function defined on the read events in E_{1} (see Definition 2.5).

Let S_{2} be the higher-level view of S_{1} obtained by transforming into a higher-level event each single execution of the SCAN/LABEL protocol, and let E_{2} be the set of higher-level events thus obtained (together with the initialization events). So, if X ∈ E_{2} is a Labeler_{i} (higher-level) event, for example, then X ⊆ E_{1} is either an execution of the LABEL protocol, or else the initial event (in which case X = {w_{0}} where w_{0} is the assumed initial write into Head(i)).

We are going to enrich S_{2} by defining the necessary functions so that the pair S_{1}, S_{2} is induced by the protocol, and then S_{2} will be shown to be a ctss (see subsection 2.4).

1. The functions message, messages, and < are naturallly transferred from S_{1} to S_{2} as follows:

(a) For any Labeler event, L ∈ E_{2}, message(L) is in message type: If w is the write onto Head(i) in L, then message(L) is defined to be the value of the field “message” in w.

(b) For any Scanner event, S ∈ E_{2}, messages(S) and <(S) are defined to be the pair returned by S. That is,

⟨message(S), <(S)⟩ = ⟨\overline{m}^{S}, σ^{S}⟩.

(We use here the convention that σ^{S}, for example, denotes the value of variable σ at the end of the execution S.)

2. The functions Ω_{i} are only required to be defined on the Scanner events, but we will define Ω_{i} on the Scanner events and on Labeler_{j} events, for j ≥ i (this will be useful later). First, for any X ∈ Labeler_{i}, define Ω_{i}(X) = X. Now assume that j > i. For any initialization event, X, in Labeler_{j}, Ω_{i}(X) is defined to be the initialization event in Labeler_{j}. Now, for X ∈ E_{2} that is either an execution of the SCAN, or the LABEL protocol by Labeler_{j} where j > i, X contains a unique read, r, of Head(i) (at line 1), let Ω_{i}(X) be the unique Labeler_{i} event containing ω(r).

Both regularity and the property of Bloom are easy to establish. Bloom’s condition holds because the write onto Head(i) is the last event in each Labeler_{i} higher-level event. (In details, the argument goes as follows. Assume Ω_{i}(S) = L. Then, by the definition of Ω_{i}, if r is the read in S of register Head(i), ω(r) ∈ L is the write onto Head(i) in L. Therefore ∀a ∈ L(a⟶_{S_{1}}r). Now to prove L⟶_{S_{2}}end(S), assume S⟶_{S_{2}}X (any X) and deduce L⟶_{S_{2}}X by proving

∀a ∈ L ∀b ∈ X (a⟶_{S_{1}}r⟶_{S_{1}}b).)

Since the first four properties in the specification list are quite obvious, we will concentrate on the proof of global coherence. To facilitate the proof, we will further enrich S_{2} by defining a function, REPORT:

For any Labeler, X, define REPORT (X) = head.report^{X} (this is, according to our convention, the field “report” as it is written by X onto its register).Thus, for X in Labeler_{i}, REPORT (X) is an array of length i of numbers.

Definition 3.10. The set R is the collection of all sequences L = ⟨L_{1}, …, L_{k}⟩, of length 1 ≤ k ≤ n, such that L_{m} ∈ Labeler_{m} for all m ≤ k. Using the precedence relation ⟶ of S_{2}, we will define on R a “lexicographical” ordering, denoted <_{R}, as follows:

For L, L′ ∈ R (with lengthes k and k′ respectively) define L <_{R} L′ iff either for some m ≤ min{k, k′}, L_{m} ≠ L′_{m} and for the first such m, L_{m}⟶L′_{m}, or else there is no such m and L is a proper initial segment of L′ (and thus k < k′ in this case).

Since ⟶ linearly orders each Labeler_{k}, <_{R} is easily seen to be a linear ordering of R. Intuitively, the Scanner’s protocol is correct because it successfully reflects the ordering <_{R} on the Labeler events given by the return functions Ω_{i}’s.

Let us agree on the following shorthand: For X ∈ Labeler_{k},

\overline{W} (X) = ⟨Ω_{1}(X), …, Ω_{k}(X)⟩.

Since X = Ω_{k}(X), \overline{W} is clearly a one-to-one map of Labeler onto R. Hence, <_{R} induces a linear ordering on Labeler which we denote <<:

For any L_{1}, L_{2} ∈ Labeler, L_{1} << L_{2} iff \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}).

We will show now that << is the ordering required to prove the global-coherence property.

Recall how ⇒ was defined (in global-coherence):

For every Labeler events L and M in S_{2}, L ⇒ M iff either L⟶M or else, for some Scanner event S, L = Ω_{i}(S), M = Ω_{j}(S), and i < (S)j.

The global-coherence property states that there is linear ordering of Labeler that extends ⇒. We will prove that << extends ⇒. This proof only relies on the following properties of S_{2} which can be easily established by considering the protocol.

Lemma 3.11. 1. For any Scanner event S,

i < (S)j iff REPORT (Ω_{i}(S)) <_{LEX} REPORT (Ω_{j}(S)).

2. For any L_{1} ∈ Labeler_{i}, L_{2} ∈ Labeler_{j}, (a)

REPORT (L_{1}) <_{LEX} REPORT (L_{2}) iff \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}).

(b) L_{1}⟶L_{2} implies for every k ≤ min{i, j}:

Ω_{k}(L_{1}) ⟶^{=} Ω_{k}(L_{2}).

Corollary 3.12. L_{1}⟶L_{2} implies L_{1} << L_{2}.

Proof. Assume L_{1} ∈ Labeler_{i}, L_{2} ∈ Labeler_{j}, and L_{1}⟶L_{2}. We will prove that \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}), which gives the corollary by the definition of <<. By (b) of the lemma, for every k ≤ min{i, j},

Ω_{k}(L_{1}) ⟶^{=} Ω_{k}(L_{2}).

This implies that \overline{W} (L_{1}) ≤_{R} \overline{W} (L_{2}), but we will prove the strict <_{R} relation. There are two cases to consider.

Case 1: There is k ≤ min{i, j} such that Ω_{k}(L_{1}) ≠ Ω_{k}(L_{2}). Then Ω_{k}(L_{1})⟶Ω_{k}(L_{2}) for the first such k, and hence (by definition of <_{R}) \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}).

Case 2: Not case 1, that is ∀k ≤ min{i, j} Ω_{k}(L_{1}) = Ω_{k}(L_{2}). There are two subcases:

1. i < j. Then i = min\{i, j\} and \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}) by definition.

2. i ≥ j. Then j = min{i, j} and hence

Ω_{j}(L_{1}) = Ω_{j}(L_{2}) = L_{2}.

This equality leads to a contradiction, because Ω_{j}(L_{1})⟶end(L_{1}) (Bloom’s condition) and L_{1}⟶L_{2} imply Ω_{j}(L_{1})⟶L_{2}, which is impossible since ⟶ is irreflexive.

Now we can prove:

Lemma 3.13. << extends ⇒.

Proof. Suppose L_{1} ∈ Labeler_{i}, L_{2} ∈ Labeler_{j}, and L_{1} ⇒ L_{2}. According to the definition of ⇒ there are two cases to consider. In the first case L_{1}⟶L_{2}, and then the corollary implies that L_{1} << L_{2}.

So now assume that for some Scanner event, S, L_{1} = Ω_{i}(S), L_{2} = Ω_{j}(S) and i < (S)j. Then, by Lemma 3.11(1),

REPORT (L_{1}) <_{LEX} REPORT (L_{2}).

But then \overline{W} (L_{1}) <_{R} \overline{W} (L_{2}), by item 2(a), and thus L_{1} << L_{2}.

4 Conclusion

A new timestamping algorithm was described and proved correct. This algorithm is ‘skewed’ in the sense that the writing processes are enumerated, Labeler_{1}, …, Labeler_{n}, and each Labeler_{j} only reads the registers of Labeler_{i} for i < j. The correctness proof relyed on the notion of system executions and was therefore behavioral in the sense that it argued about higher–level events rather than about states of computations. It was however formal and mathematical in the sense that it could easily be converted into a first-order proof.

I find two possible advantages in this approach.

1. The requirements that a timestamping protocol must meet are formally declared by writing down a list of sentences (the specifications of subsection 2.4) and demanding that the higher-level views induced by the protocol are all models of these sentences. When the original specifications of Dolev and Shavit [7] are viewed in this light, and translated into the language of system executions, some formal pitfall noticed in their work is avoided.

2. The ease of moving between lower-level and higher-level views, while remaining within a single framework—that of system executions— allows for clearer correctness proofs. The proof that the skewed protocol induces only system executions that satisfy the specifications is divided into two separate parts; the lower part deals with the protocol and establishes important higher-level properties (summerized in Lemma 3.11), and then these properties were shown to be sufficient to derive the ctss specifications as required.

It is not claimed that the skewed protocol is better than the ordinary protocol (of Figure 1), and our investigation is motivated by theoretical reasons: to find the possible basic ideas that can be used to implement ctss. (The two protocols are really different: It is not difficult to find a higher-level view of an execution of the skewed protocol that could not conceivably be seen as an execution of the ordinary protocol.)

Yet it seems to me that the idea involved in the skewed protocol will lead to efficient bounded timestamping protocols^{†}. Timestamping protocols can be divided into two categories. (We restrict our attention to protocol that use single-writer, multi-readers registers.)

1. Silent Scanners. In this category the scanners (readers) do not write anything at all. Such is the protocol of Dolev and Shavit [7] for example.

2. Writing Scanners. The scanners are allowed to write as well, usually only coordinating values (not messages). The protocols of Israeli and Pinhasov [11], and Dwork and Waarts [8] are in this category.

Let us discuss the concurrent time-complexity of these protocol (the time-complexity is the number of non-concurrent read/write events needed to execute the protocol). Let s and l be the number of scanners and labelers, and m = s+l. The time-complexity of the protocol of Dolev and Shavit [7] is in the order of l^{2} log(l), and that of Israeli and Pinhasov [11] is in the order of m. I have a protocol in category 1 with time complexity l^{2}, and it seems to be open to reduce this complexity. In the second category, I have a protocol with finite complexity: 8 concurrent events for the scan, and 6 for the label. The price paid for this time-efficiency is in longer registers: The scanners only write four possible values, but the labelers’ registers have length in the order m^{2}, compared with order m in [11].

†In fact, this skewed protocol is the basis of an unpublished 1990 manuscript which deals with bounded values protocols.

References

[1] U. Abraham. What is a state of a system? (an outline). In Semantics of programming languages and model theory, edited by M. Droste and Y. Gurevich, Gordon and Breach Science Publishers, pages 213–243. 1993.

[2] U. Abraham. On system executions and states, J. of Applied Intelligence, Vol. 3:17-30, 1993.

[3] U. Abraham, S. Ben-David, and M. Magidor. On global-time and inter-process communication. Semantics for Concurrency, Proceedings of the International BCS-FACS Workshop, Leicester, edited by M. Z. Kwiatkowska et al. Workshops in computing: Series published by Springer in collaboration with the British Computer Society. Pages 311 – 323. 1990.

[4] S. Ben David. The global-time assumption and semantics for distributed systems. Proceedings of the 7th ACM Symposium on Principles of Distributed Computing, pages 223–232. 1988.

[5] B. Bloom. Constructing two-writer atomic registers. Proceedings of the 6th ACM Symposium on Principles of Distributed Computing, pages 249 – 259. 1987.

[6] R. Carnap. Logical foundation of probability. The university of Chicago press, 1950.

[7] D. Dolev and N. Shavit. Bounded concurrent time-stamp systems are constructible. Proceedings of the 21st ACM Symposium on Theory of Computing, pages 454– 465. 1989.

[8] C. Dwork and O. Waarts. Simple and efficient bounded concurrent timestamping (or bounded concurrent timestamping are comprehensible!). Proceeding of the 24st ACM Symposium on Theory of Computing, pages 655–666. 1992.

[9] P. C. Fishburn. Interval orders and interval graphs. Wiley (Wiley-Interscience series in discrete mathematics), 1986.

[10] A. Israeli and M. Li. Bounded Time-Stamps. Proceedings of the 28th annual IEEE Symposium on Foundation of Computer Science, pages 371-382. 1987.

[11] A. Israeli and M. Pinhasov. A concurrent Time-Stamp scheme which is linear in time and space (Extended Abstract). Preprint from March 26, 1991.

[12] L. Lamport. On Interprocess Communication, Part I: Basic formalism, Part II: Algorithms. Distributed Computing, Vol. 1: 77 - 101, 1986.

[13] V. Pratt. Modeling concurrency with partial orders. International J. of Parallel Programming, Vol.15: 33 - 71, 1986.