Two approaches to concurrency

Uri Abraham Departments of mathematics and computer science Ben Gurion University of the Neguev Beer Sheva, Israel.

January 11, 2003

Abstract The aim of this lecture is to introcude my course “models for concurrency” to potential students and to explain some basic ideas of my research to colleagues. The lecture is based on an informal description of two proofs to a critical section algorithm that relies on a semaphore: one based on the notion of a global state, and the other on an abstract specification of semaphores ^{1}.

1 A simple critical-section protocol

In this lecture we first describe a very simple and well-known critical-section protocol which is based on the usage of a semaphore. Then we give two correctness proofs. Both prove the mutual exclusion property, but they differ in the ways that they approach reality and describe it. The first proof expresses the traditional point of view which describes an execution as a sequence of global states. The second expresses my view on concurrency, and is based on the distinction between internal and external semantics of concurrent protocols. In the second proof there are no global states and the semaphore is specified abstractly.

We assume N processes P_{1}, …, P_{N} which execute the code of Figure 1. The external event encompasses activities of the process that are not connected to its critical section. This operation may well be non-terminating. The two operations request and release access a semaphore, Sem, which can hold the values 0 and 1, and which is initially set by the system to 1. The meaning of these operations is surely known, at least informally, to all of you. An execution of request by P_{i} can be terminating or non-terminating. If it terminates, then P_{i} is ready to execute line 2, namely its critical section denoted here CS. If in some execution of line 1 the request never terminates, then process P_{i} will never reach again its critical section. We are not worried here by this possibility since we concentrate on the mutual exclusion property (which suffices for our Protocol for P_{i} repeat for ever:

1I would like to thank Prof. Yefim Dinitz who insisted that I give full proofs in the lecture and listen to a preliminary exposition and thus improved it considerably.

0 external;

1 request;

2 CS;

3 release;

Figure 1: A simple mutual-exclusion protocol with semaphore operations request and release.

pedagogical needs, even if it doesn’t completely satisfy the starving process). Anyhow, a process reaching its critical section execution of line 2 can terminate this operation and then it executes line 3, which is a release operation. We assume that release operations always terminate. Then P_{i} returns to line 0 for another external event.

We shall give here two different proofs for the fact that the mutual exclusion property holds: it is never the case that two processes are simultaneously at their critical sections.

2 First proof: global states and histories

For each process P_{i} we introduce a variable PC_{i} (“program counter” of P_{i}) which can hold the values {0, 1, 2, 3}, that is

type(PC_{i}) = {0, 1, 2, 3}

referring to lines 0, 1, 2, and 3 and their instructions. The value of PC_{i} being 0 (1, 2, or 3) indicates that P_{i} is ready to execute line 0 (1, 2, or 3). Then variable Sem is also introduced and

type(Sem) = {0, 1}.

Thus we have N + 1 variables in our system.

V = {PC_{i}, …, PC_{N}, Sem}.

A State is a function S, with dom(S) = V, and such that S(v) ∈ type(v) for every variable v ∈ V. Such states are called here “global states” because they describe a possible instantaneous situation of all processes and their devices (semaphore Sem in our case).

The initial state is defined to be the state S such that S(PC_{i}) = 0 for all 1 ≤ i ≤ N and S(Sem) = 1.

A step is a pair of states ⟨S_{1}, S_{2}⟩ that describe an execution of a single instruction (corresponding to some line of the protocol) by one of the processes. We have the following steps here.

Executions of line 0 by P_{i} These are all pairs ⟨S_{1}, S_{2}⟩ of states such that S_{1}(PC_{i}) = 0, S_{2}(PC_{i}) = 1, and S_{2}(v) = S_{1}(v) for every variable v ∈

V \ {PC_{i}}.

Executions of line 1 by P_{i}. These are all pairs ⟨S_{1}, S_{2}⟩ of states such that S_{1}(PC_{i}) = 1, S_{1}(Sem) = 1, S_{2}(PC_{i}) = 2, S_{2}(Sem) = 0, and for every

v ∈ V \ {PC_{i}, Sem} S_{2}(v) = S_{1}(v).

Executions of line 2 by P_{i}. These are all pairs ⟨S_{1}, S_{2}⟩ of states such that one of the following holds.

1. S_{1}(PC_{i}) = 2, SS_{2}(PC_{i}) = 3, and S_{2}(v) = S_{1}(v) for every v ∈ V \ {PC_{i}}, or

2. S_{1}(PC_{i}) = 2 and S_{2} = S_{1} (indicating a prolongation of P_{i}’s stay at its critical section).

Executions of line 3 by P_{i}. These are all pairs ⟨S_{1}, S_{2}⟩ of states such that S_{1}(PC_{i}) = 3, S_{1}(Sem) = 0, S_{2}(PC_{i}) = 1, S_{2}(Sem) = 1, and S_{2}(v) = S_{1}(v) for every v ∈ V \ {PC_{i}, Sem}.

A history for our critical section algorithm is an infinite sequence of states ⟨S_{i} | i ∈ I⟩ such that the following properties hold. I is either ω, the set of all natural numbers, or a finite initial segment of ω. For simplicity we deal here only with the possibility that I = ω is infinite. (In order to achieve this uniformity, one may add all transitions of the form ⟨S, S⟩ such that S(PC_{i}) = 0 for some i. These transitions reflect external executions of operations that are not manifest in the variables described here.)

1. S_{0} is the initial state.

2. For every k ∈ ω, ⟨S_{k}, S_{k+1}⟩ is a step by some P_{i}, 1 ≤ i ≤ N.

Now the correctness proof is the following.

Theorem 2.1 If ⟨S_{i} | i ∈ ω⟩ is a history, and if k ∈ ω is any index, then it is not the case that S_{k}(PC_{i}) = 2 and S_{k}(PC_{j}) = 2 for i ≠ j in {1, …, N}.

Proof. Given a history, we prove by induction on k ∈ ω the following invariant assertion.

\begin{matrix}∀1 ≤ i ≤ N : S_{k}(PC_{i}) ∈ \{2, 3\} → [∀1 ≤ j ≤ N(j ≠ i → S_{k}(PC_{j}) ∈ \{0, 1\}) \\ ∧S_{k}(Sem) = 0]. \end{matrix} (1)

The proof of this assertion for k = 0 is trivial, since S_{0} is the initial state and S_{0}(PC_{i}) = 0 for all i’s.

Assume that the invariant holds for S_{k} and we prove it for S_{k+1}. By definition of a history, s = ⟨S_{k}, S_{k+1}⟩ is a step by some P_{i_{0}}, and we analyze the different possibilities for such a step.

Case 0: Step s is an execution by process P_{i_{0}} of line 0. Since the only change from S_{k} to S_{k+1} is in PC_{i_{0}} which has changed from 0 to 1, it is trivial to check that the assertion remains true in S_{k+1} since it did hold in S_{k}.

Case 1: Step s is an execution by process P_{i_{0}} of line 1. By definition of this type of step, S_{k}(Sem) = 1. Since the invariant holds for S_{k}, it follows that S_{k}(PC_{i}) = 1 for all 1 ≤ i ≤ N (or else S_{k}(Sem) = 0 follows). Thus S_{k+1}(PC_{i_{0}}) = 2 and S_{k+1}(PC_{j}) = 1 for all j ≠ i_{0} and S_{k+1}(Sem) = 0, proving the invariant for S_{k+1}.

case 2: Step s is an execution process P_{i_{0}} of line 2. There are two possibilities in this case, and the proof of the invariant for P_{k+1} is a routine.

Case 3 Step s is an execution process P_{i_{0}} of line 3. Again the proof follows trivially from the definitions.

3 Second proof: unrestricted and restricted semantics

In the second proof there are no global states. We consider executions instead of histories. In an execution each process P_{i} generates a sequence of events which correspond to an execution of the protocol. These events are described by means of predicates and functions. For example, the statement P_{i}(e) says that event e is an execution by P_{i} of an instruction from the protocol. So P_{i} is used here as a unary predicate. There are three sorts of events predicated by request, cs, and release. These are unary predicates. For example, request(e) ∧ P_{i}(e) says that e is a request event (an execution of line 1) by process P_{i}. Any event may be terminating or not, and the statement terminating(e) says that event e is terminating. So the statement that P_{i} contains a non-terminating event (which may be true or false in an execution) is the following.

∃e(P_{i}(e) ∧ ¬terminating(e)).

The events by P_{i} are issued one after the other in a serial ordering denoted <_{i}. So <_{i} is an ordering of P_{i} (that is of the set {e | P_{i}(e)}) which is either finite or of the order-type of ω.

Suppose that we don’t know anything about the semantics of the request and release operations and that we haven’t heard anything about semaphores. What can we say about executions of the critical-section protocol described here. Surely not much, but some simple facts which follow the structure of the protocol and are not related to the meaning of the semaphore can still be concluded. For example, that between any two critical-section events by P_{i} there exists a terminating request event. The “unrestricted semantics” is defined to be that information about executions of the protocol that do not depend on the correct behavior of the communication devices. We group the properties of our protocol that pertain to its unrestricted semantics into four groups: U0, U1, U2, and U3.

U0 For every i ≠ j in {1, …, N}, there is no event e such that P_{i}(e) ∧ P_{j}(e). For every event e, one and only one of the following possibilities holds: external(e), request(e), cs(e), and release(e).

U1 For each 1 ≤ i ≤ N, <_{i} is a linear ordering of the set {e | P_{i}(e)}. If this set of events is infinite then its <_{i} order-type is ω

U2 Every terminating event e in P_{i} has a successor e′ in P_{i} (that is, e <_{i} e′ and there is no x such that e < x < e′). If e is non-terminating (that is ¬terminating(e)) and P_{i}(e), then e is the last event in P_{i} (there is no y with e <_{i} y).

U3 The first event in each P_{i} (for 1 ≤ i ≤ N) is an external event. Suppose that e and e′ are in P_{i} and e′ is the successor of e in P_{i}:

1. If external(e) then request(e′).

2. If request(e) then cs(e′).

3. If cs(e) then release(e′).

4. If release(e) then external(e′).

Now we discuss the semaphore and its semantics. This discussion leads to a definition of three properties R0, R1, and R2 which enable us to define the “restricted semantics” namely the semantics of the protocol assuming that the request/release operations are restricted to operate properly. To express the properties of the semaphore we need a binary relation < defined on the events, and a unary (partial) function δ : Event → Event. The relation < is called the “precedence relation” and for events e_{1} and e_{2} (not necessarily in the same process) e_{1} < e_{2} means, intuitively, that e_{1} terminates before e_{2} begins. The function δ is called the “delay function”. It is defined on all terminating request events (and only on terminating request events) and its values are release events. Intuitively, we think of the semaphore as some signaling device that may suspend the process that invokes the request operation, r, and delays its subsequent operation, e, until the release δ(r) is obtained. Although the executing process in not aware of this potential delay and release, the observer of the system sees that δ(r) < e. That is, if the request r terminates and is followed in P_{i} by an event e (that is r <_{i} e), then necessarily δ(r) < e. The “restriction properties” are stated as follows.

R0 < is a partial ordering of all events. The restriction of < to the set of events in P_{i} is exactly <_{i} (equivalently, e_{1} <_{i} e_{2} implies e_{1} < e_{2} for all e_{1}, e_{2} in P_{i}). If the set of release events is infinite, then its order-type under < is ω.

The restriction of < to the set of release events is a linear ordering of these events. That is, for every two distinct release events e_{1} and e_{2}, e_{1} < e_{2} or e_{2} < e_{1}).

There exists an event rl_{0} such that 1. release(rl_{0}), and rl_{0} < e for every event e different from rl_{0}.

2. For every i, ¬P_{i}(rl_{0}), but for every event e different from rl_{0}, P_{i}(e) holds for some (unique) index i.

We think of rl_{0} as the initial release event given by the system before the processes began their executions. The assumption that rl_{0} exists replaces the assumption that the initial value of the semaphore is 1, made in the first proof.

R1 The domain of the function δ is the collection of all terminating request events. If r is a terminating request event, then δ(r) is a release event. The function δ is one-to-one

R2 If r <_{i} e are events by P_{i}, and request(r), then terminating(r) and δ(r) < e.

The following theorem expresses the mutual-exclusion property in the formalism of the second proof.

Theorem 3.1 Suppose that U0—U3 and R0—R2 hold. Then

∀e_{1}, e_{2}(cs(e_{1}) ∧ cs(e_{2}) ∧ e_{1} ≠ e_{2} → e_{1} < e_{2} ∨ e_{2} < e_{1}).

Proof. We define first a function, R, on all cs events and on all release events except the initial rl_{0} event. If c is any cs event, then P_{i}(c) holds for some unique i (by R0), and there exists then a request event rq in P_{i} such that c is the successor of rq in <_{i}. This follows mainly from U3, but the fact that very event in P_{i} (except the first one) is the successor of an event in P_{i} is laso used, and we need to know that c is not the initial event (which follows from the fact that a cs event is not a release event, U0). Since a non-terminating event is necessarily the last event in its process (by U2), rq is terminating, and hence δ(rq) is defined (by R1). We define

R(c) = δ(rq).

Now we define R on non-initial release events. If ℓ is any release event that is not the initial release event, then P_{i}(ℓ) holds for some i and there exists then a cs event c such that c <_{i} ℓ, and ℓ is the successor of c in P_{i}. But R(c) is already defined, and so we define

R(ℓ) = R(c).

We make the following claims:

Lemma 3.2 1. The restriction of R to the cs events is one-to-one, so is its restriction to the non-initial release events.

2. If ℓ is any release event in P_{i}, then ℓ is the <_{i} successor of a cs event c in P_{i}, and R(ℓ) = R(c) < c < ℓ holds.

Proof. It is easy to show that R is one-to-one on the cs events. If c_{1} ≠ c_{2} are cs events, and rq_{1}, rq_{2} are the request events so that c_{k} is the successor of rq_{k} in its process (fro k = 1, 2), then rq_{1} ≠ rq_{2} is easily obtained. (If c_{1} and c_{2} are in different processes, then this is clear since the processes are disjoint, but if these events are all in one process, then rq_{1} ≠′ 2 is concluded from the fact that in a linear ordering no point has two successors). But δ is one-to-one and hence δ(rq_{1}) ≠ δ(rq_{2}). That is, R(c_{1}) ≠ R(c_{2}).

A similar argument shows that if ℓ_{1} ≠ ℓ_{2} are non-initial release events, then R(ℓ_{1}) ≠ R(ℓ_{2}).

We prove item 2. If ℓ is a release event in P_{i}, then R(ℓ) was defined as follows. We determined the request event rq and cs event c such that ℓ is the successor of c and c is the successor of rq in <_{i}, and we defined R(ℓ) = R(c) = δ(rq). But then δ(rq) < c by property R2. Hence

R(ℓ) < c < ℓ

follows (c < ℓ is a consequence of c <_{i} ℓ). Q.E.D.

The following lemma is formulated for the ordering (ω, <) of the natural numbers with their natural ordering, but it holds (of course) for any finite or infinite ordering of order-type ω.

Lemma 3.3 Suppose that R is any function defined on the non-zero integers and into the integers, and is such that

1. R is one-to-one.

2. R(n) < n for every n > 0.

Then R(n) = n − 1 for every n > 0. That is, every n > 0 is the successor of R(n).

Proof. Suppose that n_{0} > 0 is the least counter-example to the lemma, and there exists some n such that R(n_{0}) < n < n_{0}. Choose n to be minimal (i.e. n = R(n_{0}) + 1). Since n > 0, R(n) is defined. Compare now R(n) and R(n_{0}). If R(n_{0}) < R(n), then R(n_{0}) < R(n) < n < n_{0} contradicts the minimality of n. If R(n_{0}) = R(n), then n < n_{0} contradicts the assumption that R is one-to-one. Finally, if R(n) < R(n_{0}), then n is also a counter-example to the lemma, because R(n) < R(n_{0}) < n. This contradicts the minimality of n_{0}. Q.E.D.

We return now to use R as the function defined above on the release and cs events. Since the release events are linearly ordered by < and their order type is either finite or ω (by R0) we can translate the lemma above and obtain the following conclusion.

If a release event ℓ is not the initial release event, then ℓ is the successor of R(ℓ) in the < ordering of the release events.

The last lemma needed is the following:

Lemma 3.4 Suppose that cs(c) and ℓ is any release event such that R(c) < ℓ. Then c is terminating. Intuitively, this lemma says that if c is non-terminating cs event, then R(c) is the last release event.

Proof. The proof is by induction on the position of ℓ in the set of release events. Clearly, ℓ is not the initial release event (as R(c) < ℓ) and we know already that ℓ is the successor of R(ℓ) in the ordering < restricted to the release events. As R(c) < ℓ, R(c) ≤ R(ℓ) is obtained. There are two possibilities now. If R(c) < R(ℓ), then the inductive assumption can be applied to R(ℓ), and then c is terminating as required. In case R(c) = R(ℓ), then the definition of R(ℓ) shows that ℓ is necessarily the successor of c in P_{i}, and then c is terminating (by U2). Thus the lemma is proved. Q.E.D.

Now we can prove theorem 3.1. Actually we shall prove a slightly stronger version.

Claim 3.5 If c_{1} and c_{2} are cs events and R(c_{1}) < R(c_{2}), then c_{1} < c_{2}. (Hence if c_{1} and c_{2} are distinct cs events, then R(c_{1}) and R(c_{2}) are < comparable (being distinct release events) and thus c_{1} < c_{2} or c_{2} < c_{1} follows.)

Proof. Assume that R(c_{1}) < R(c_{2}). Say c_{1} is in P_{i}, and write R(c_{2}) = ℓ. Then by the lemma above, c_{1} is terminating, and hence it is followed by a release event ℓ in its process P_{i} (by U2). So c_{1} < ℓ and R(ℓ) = R(c_{1}) (by definition). But since ℓ is the successor of R(ℓ) (Lemma 3.3) ℓ ≤ R(c_{2}) (follows from R(c_{1}) < R(c_{2})) and hence R(c_{2}) < c_{2} implies that c_{1} < c_{2}. Q.E.D.

4 Discussion

Let’s compare the two proofs described here. Since my research in concurrency is based on the second approach, my aim is to advocate it and I will argue in favor of that approach. However, this does not mean that I take the first approach to be useless. I believe that both represent valid attitudes which can be useful in different circumstances. The first proof is simpler, I have to admit that. (However, in my experience, the simplicity of the second approach is revealed when more complex algorithms are investigated.)

Both proofs given here are informal. When I stated this in the lecture, the audience gazed in disbelief since both proofs are quite rigorous mathematically. There is a simple test that can discern a formal from an informal text. It consists of two questions.

1. Is there a formally (mathematically) defined language in which this text is written?

2. If yes, then ask the following question: is the semantics of that language well defined?

The second proof given here is “semi-formal”. Namely it is a standard routine to transform it into a formal proof. The language involves the predicates request cs etc. formed according to the rules of logical languages, and the statements U1 etc. which were written in mathematical English can be easily transformed into statements of that logical language (some parts of the statements are secondorder, saying that the order-type of some ordering is ω, but this is fine, since second-order is as formal as first-order). The second question is answered positively of course (by the classical work of Tarski the notions of structure or model and satisfiability is defined).

For the first proof there seems to be two avenues for formalization. The first one is to employ the language and development of set theory. States and transitions, for example, being functions and pairs of functions are objects in the universe of discourse. So one can quantify over states and transitions, and even over histories (all these objects are points in the universe of set-theory). This approach is rarely used, and the “concurrency community” has embraced the usage of “temporal logic” (for example Z. Manna and A. Pnueli [3] “The Temporal Logic of Reactive and Concurrent Systems”). In this approach, there is no possibility to quantify over states or steps taken in a history, and there are no predicates defined over them. Temporal language is rather restricted to temporal operators instead of quantifications. This restrictiveness can be regarded as an advantage, and it may be an advantage in certain circumstances, however in my taste temporal logic is non-intuitive and quite unnatural.

The second proof is easily turned into a formal proof as I’ve claimed, but there seems to be a natural question (asked in my lecture): how can one justify the axioms U1—U2 and R1—R2 that were used to derive the proof. For example, the statement U1—U3 were written without any justification, just by appealing to our intuitive understanding of the protocol. If we want formal correctness proofs of distributed algorithms this seems to be an illegitimate procedure. An answer is given in my book and it will be a major part of my course, to define the unrestricted semantics of protocols. Yet, even if this is accepted, one can still question the specification of semaphores given here. How can we be sure that we can rely on properties R1–R2? Again, a detailed answer is in my book.

5 More realistic semaphores

The semantics of the semaphore as it was described in the first proof (section 1) is based on a description found in [3]. Although it is suitable for explanatory purposes, it seems to be too crude and not to conform to the usual description (which we call the “textbook description”) of semaphores. The problem is the following. In a history it is possible that there exists a state S such that the semaphore has value 1 in S and there exists a process P_{i} that is in line 1 in S (ready to execute the request instruction), and yet P_{i} does not move to its critical-section in the next state despite the fact that all other processes are in their external states in S. In fact it is possible that some other process P_{j} that was in its external position in S enters its critical-section before P_{i}.

The textbook semantics of semaphores assumes a queue of suspended processes. Any release operation can remove a process P from that queue and change the program counter of P to point to the critical section, or (if the queue is empty) increase the semaphore by one. In executing a request operation, a process is suspended and added to that queue (in case the semaphore is zero), or proceedes directly to the critical-section and decrease the semaphore by one. There are two possibilities to deal with the release operations. The first is to assume that in case that there are several processes in the queue of suspended processes, the release operation removes an arbitrary suspended process and moves it into its critical-section. The second possibility is to assume a FIFO queue and to demand that processes are removed in the order of their suspension. In any case, if the semaphore is 1, then no process is suspended. In the following we assume that the queue of suspended processes is a FIFO queue.

To define the states and steps of the textbook semaphores, we add a variable Q to denote the queue of suspended processes. In executing a request operation there are two possibilities. If the value of the semaphore is 1 (then Q is necessarily empty), then the executing process changes its PC variable to 2 (to be ready to execute its critical-section) and the semaphore value is reduced to 0 at once. If, however, the semaphore is 0, then the process is added to the queue Q (to its tail). In executing a release operation there are two possibilities. If Q is empty, then the semaphore variable is simply increased by 1. If however Q is non-empty, then the process at head of Q is dequeued and its program counter is set to 2.

So the set of variables is now V = {Q, P C_{1}, …, PC_{N}}. The possible values of PC_{i} are as before {0, 1, 2, 3}, and the additional variable Q can hold values that are finite (one-to-one) sequences of indices from {1, …, N}. (Any such sequence p_{0}, …, p_{K} denotes a queue of processes with these indices, where p_{0} is at the head of the sequence (the first to be released). We have the following steps for the textbook semaphore.

1. Executions of line 0 by P_{i}. These are all pairs ⟨S_{1}, S_{2}⟩ of states such that S_{1}(PC_{i}) = 0, S_{2}(PC_{i}) = 1 and S_{2} agrees with S_{1} on the value of any other variable.

2. Executions of line 1 by P_{i} (a request). These are all pairs ⟨S_{1}, S_{2}⟩ such that S_{1}(PC_{i}) = 1 and there are 2 possibilities.

(a) If S_{1}(Sem) = 1, then S_{2}(Sem) = 0, S_{2}(PC_{i}) = 2, and for all other variables S_{1} and S_{2} agree.

(b) If S_{1}(Sem) = 0, then S_{2}(Q) is obtained from S_{1}(Q) by executing an enqueue operation of value i on S_{1}(Q). (I assume that this is so clearly understood.) Again, all other variables retain in S_{2} their S_{1} values. In particular S_{2}(PC_{i}) = 1.

3. An execution of the cs instruction at line 2 by P_{i} is as before. There are two possibilities, Either P_{i} remains in its critical-section and nothing changes, or else it ends its critical-section activity and advances PC_{i} to 3.

4. Executions of line 3 by P_{i} (release executions). These are all pairs ⟨S_{1}, S_{2}⟩ of states such that S_{1}(PC_{i}) = 3 and one of the following possibilities hold.

(a) S_{1}(Q) is non-empty and we let p be the value at head of S_{1}(Q). i ≠ p. Then S_{2}(Q) is obtained by dequeueing S_{1}(Q), S_{2}(PC_{p}) = 2, S_{2}(PC_{i}) = 0, and for any other variables P_{1} and P_{2} agree.

(b) S_{1}(Q) is empty, and in this case S_{2}(Sem) = 1, S_{2}(PC_{i}) = 0, and the two states agree on any other variable.

The two proofs given in sections 2 and 3 can be extended to the more realistic semaphore semantics described here. For the first proof, one states and proves the same assertion and shows that it remains invariantly true in all states of any history. The proof is somewhat different, simply because the steps are different and they involve the new variable Q. It is necessary to reprove the invariance property because the behaviour of the textbook semaphores is different from the simple semaphores described first. The second proof has here an advantage because it needs no change and it can simply be quoted. The properties U1— U3 remain valid for the protocol with the new semantics, simply because these properties did not reflect any assumption on the semaphore. Properties R1–R2 hold for the textbook semaphore as well, and an additional property R3 has to be formulated, in order to reflect the usage of a FIFO queue of suspended processes.

R3 If r_{1} < r_{2} are request events, then δ(r_{1}) < δ(r_{2}).

Since the proof of section 3 relies only on properties U1—U3 and R1-R2 taken as axioms, it certainly remains valid when a new axiom is added. The abstract approach thus has an advantage in that it has a wider range of applications.

6 Conclusion

Two approaches to concurrency were compared here by analyzing how they treat the same algorithm, which was chosen to be the simplest possible: Dijkstra’s mutual exclusion protocol with a binary semaphore. A typical representation of the first approach is [3] and in numerous articles by these and by other authors that adopt some form of temporal logic for the specification and correctness proofs of concurrently operating systems. In temporal logic, as it is applied to concurrency, the notion of state is of prime importance. State formulas are statements about states, and they can also charcterize transitions by using primed and unprimed variables in the same formula. Then temporal operators amplify the state formulas and produce temporal formulas that apply to histories. Yet these temporal formulas cannot treat the states and transitions as elements. One cannot, for example, quantify over the history steps in a temporal formula, one cannot employ predicates or functions over the steps, and, most importantly, one cannot collect hisotry steps to form higher-level events. All of these natural mathematical procedures (Defining predicats and functions over your prime objects, and collecting these objects into compound objects) are lacking from the logics adopted by the followers of the first proof.

In the second approach (desribed in [1]) global states are of secondary importance, and in fact they can be totally avoided. Events have taken their place. Semaphores and other communication devices are specified abstractly, and in such specifications functions, predicates, and quantifiers can be applied to the events.

It is also possible to assemble events into sets that form “higher-level events”. We have not seen in this lecture an example of this procedure, but the possibility of forming higher-level events and remaining within the same framework (in which events are the prime objects) is an appealing advantage of this approach. (It seems that Lamport [2] was the first to have recognized the importance of relating higher-level and lower-level events.)

References

[1] U. Abraham, Models for Concurrency, Gordon and Breach, 1999.

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

[3] Z. Manna, and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Vol.1 “Specification” Springer Verlag, 1992.