1: \documentclass[twocolumn,twosided]{IEEEtran}
2: \usepackage{amsmath,epsf}
3:
4:
5: \numberwithin{equation}{section} % in amsmath
6: \newtheorem{lemma}{Lemma}[section]
7: \newtheorem{theorem}[lemma]{Theorem}
8: \newtheorem{proposition}[lemma]{Proposition}
9: \newtheorem{fact}[lemma]{Fact}
10: \newtheorem{claim}[lemma]{Claim}
11: \newtheorem{corollary}[lemma]{Corollary}
12: \newtheorem{conjecture}[lemma]{Conjecture}
13: \newtheorem{definition}[lemma]{Definition}
14: \newtheorem{notation}[lemma]{Notation}
15: \newtheorem{ex}[lemma]{Example}
16: \newenvironment{example}{\begin{ex}}{\hspace*{\fill}$\diamondsuit$\end{ex}}
17: \newtheorem{rem}[lemma]{Remark}
18: \newenvironment{remark}{\begin{rem}}{\hspace*{\fill}$\diamondsuit$\end{rem}}
19: %\newenvironment{proof} {\vspace{0.01cm} {\bf Proof}. }{ \hfill $\diamond$}
20:
21:
22:
23: \newcommand{\nat}{I\!\!N}
24: \newcommand{\ar}{\rightarrow}
25: \newcommand{\arp}{\Rightarrow}
26:
27: \newcommand{\pcs}[1]{\mbox{process}(#1)}
28:
29: \newcommand{\half}{\frac{1}{2}}
30: \newcommand{\free}{\bot}
31: \newcommand{\pos}{\mbox{pos}}
32: \newcommand{\heads}{\mbox{heads}}
33: \newcommand{\tails}{\mbox{tails}}
34:
35: \newcommand{\s}[1]{s(#1)}
36: \newcommand{\f}[1]{f(#1)}
37: \newcommand{\sa}[2]{#1.#2}
38: \newcommand{\Hi}{H^{\infty}}
39:
40: \newcommand{\rst}{\mbox{\it rst\/}}
41: \newcommand{\me}{\mbox{\it me\/}}
42: \newcommand{\he}{\mbox{\it he\/}}
43: \newcommand{\chose}{\mbox{\it choose\/}}
44:
45: \newcommand{\jump}{\hspace*{1em}}
46:
47: \newenvironment{prot}{\tt\begin{tabbing}}{\end{tabbing}}
48: \newenvironment{prot3}{\tt\begin{tabbing}}{\end{tabbing}}
49: \newenvironment{prot4}{\tt\begin{tabbing}}{\end{tabbing}}
50: \newenvironment{prog}{\begin{verse}}{\end{verse}}
51: \newenvironment{hist}{\begin{verse}}{\end{verse}}
52:
53:
54:
55:
56: \begin{document}
57: \title{Randomized Two-Process Wait-Free Test-and-Set}
58:
59: %\epsfpreviewtrue
60:
61: \author{John Tromp and Paul Vitanyi\thanks{
62: J. Tromp is with the
63: Centrum voor Wiskunde en Informatica,
64: Kruislaan 413, 1098 SJ Amsterdam, The Netherlands. email: tromp@cwi.nl.
65: P.M.B. Vit\'anyi is with the Centrum voor Wiskunde en Informatica and
66: the University of Amsterdam, address: CWI,
67: Kruislaan 413, 1098 SJ Amsterdam, The Netherlands, email: paulv@cwi.nl.
68: Both authors were partially supported by the
69: EU fifth framework project QAIP, IST--1999--11234,
70: the NoE QUIPROCONE IST--1999--29064,
71: the ESF QiT Programmme, and the EU Fourth Framework BRA
72: NeuroCOLT II Working Group
73: EP 27150.
74: }
75: }
76:
77:
78:
79: \maketitle
80:
81: \begin{abstract}
82: We present the first explicit, and currently simplest,
83: randomized algorithm for
84: two-process wait-free test-and-set. It is implemented with two
85: 4-valued single writer single reader atomic variables.
86: A test-and-set takes at most 11 expected elementary steps, while
87: a reset takes exactly 1 elementary step.
88: Based on a finite-state analysis, the proofs of correctness
89: and expected length are compressed into one table.
90: \end{abstract}
91: \begin{keywords}
92: Test-and-set objects,
93: Symmetry breaking,
94: Asynchronous distributed protocols,
95: Fault-tolerance, Shared memory, Wait-free read/write registers,
96: Atomicity,
97: Randomized algorithms, Adaptive adversary.
98: \end{keywords}
99:
100:
101: \section{Introduction}
102: \label{sect.intro}
103: A test-and-set protocol concurrently executed by each process out of
104: a subset of $n$ processes
105: selects a {\em unique} process from among them.
106: In a distributed or concurrent system, the test-and-set operation is
107: useful and sometimes mandatory in a variety of situations including
108: mutual exclusion, resource allocation,
109: leader election and choice coordination. It is well-known
110: that in the wait-free setting,
111: \cite{La86}, a deterministic construction from atomic read/write
112: variables is impossible \cite{LA-A87}. Although widely assumed to
113: exist, and referred to,
114: an explicit randomized construction for wait-free
115: test-and-set has not appeared in print yet, apart from a deterministic
116: construction {\em assuming} two-process atomic test-and-set \cite{AGTV91}.
117: The latter, in the form of a randomized two-process wait-free test-and-set
118: has been circulated in draft form \cite{TV90} for
119: a decade. Here we finally present the construction.
120: Since such constructions are notoriously prone to hard-to-detect errors,
121: we prove it correct by an exhaustive finite-state proof, thus also
122: presenting a nontrivial application of this proof technique.
123:
124: {\bf Interprocess Communication:}
125: The model is interprocess communication through shared memory as
126: commonly used in the theory
127: of distributed algorithms
128: \cite{Ly96}.
129: We use atomic single writer single reader registers as primitives.
130: Such primitives
131: can be implemented wait-free
132: from single-reader single-writer ``safe''
133: bits
134: (mathematical versions of hardware ``flip-flops'')
135: \cite{La86}).
136: A concurrent object is {\em constructible\/}
137: if it can be implemented deterministically with boundedly many safe bits.
138: A deterministic protocol executed by $n$ processes is {\em wait-free}
139: if there is a finite function $f$ such that every non-faulty process terminates
140: its protocol executing a number of at most $f(n)$ of accesses
141: to the shared memory primitives, regardless of
142: the other processes execution speeds.
143: If the execution speed of a process drops to zero then
144: this is indistinguishable from the process having a crash failure.
145: As a consequence, a wait-free solution can tolerate up to
146: $n-1$ processes having crash failures
147: (a property called ``$(n-1)$-resiliency''), since the surviving
148: non-faulty process correctly executes and terminates its protocol.
149: Below, we also write ``shared variable'' for ``register.''
150:
151:
152: {\bf Randomization:}
153: The algorithms executed by each process are randomized by
154: having the process flip coins (access a random number generator).
155: In our randomized algorithms
156: the answers are always correct---a unique process gets selected---
157: but with small probability
158: the protocol takes a long time to finish.
159: We use the customary assumption
160: that the coin flip and subsequent
161: write to shared memory are separate atomic actions.
162: To express the computational complexity of our algorithm we use
163: the expected complexity, over all system executions and
164: with respect to the randomization by the processes and the worst-case
165: scheduling strategy of an adaptive adversary.
166: A {\em randomized} protocol is wait-free if $f(n)$
167: upper bounds the {\em expectation} of the number of elementary steps,
168: where the expectation is taken over all randomized system
169: executions against the worst-case adversary in the class
170: of adversaries considered (in our results the
171: adaptive adversaries).
172:
173: {\bf Complexity Measures:}
174: The computational complexity of distributed
175: deterministic algorithms using shared memory
176: is commonly expressed in number and type
177: of intercommunication primitives required and the maximum number of
178: sequential read/writes by
179: any single process in a system execution. Local computation is usually ignored,
180: including coin-flipping in a randomized algorithm.
181:
182:
183: {\bf Related Work:}
184: What concurrent wait-free object is
185: the most powerful constructible one?
186: It has been shown that wait-free atomic
187: multi-user variables, and atomic snapshot objects,
188: are constructible,
189: for example \cite{Pe83,La86,VA86,IL87,Sc88,LTV89,SinAG94,DS89,An90,AADGMS90,HV01}.
190: %used in \cite{BarD89,BorG93,HerS93}.
191: In contrast, the agreement problem in
192: the deterministic model of computation (shared memory or message passing) is
193: unsolvable in the presence of faults \cite{FisLP,He91a,LA-A87}.
194: Correspondingly, wait-free consensus---viewed as an object
195: on which each of $n$ processes can
196: execute just one operation---is not constructible \cite{CIL87,Ab88},
197: although randomized implementations are possible
198: \cite{CIL87,Ab88,As90,SSW90}.
199: Wait-free concurrent test-and-set can deterministically
200: implement two-process wait-free consensus, and therefore
201: is not deterministically constructible \cite{LA-A87,He91a}.
202: This raises the question of whether randomized algorithms for
203: test-and-set exist.
204:
205: In \cite{He91a} it is shown that repeated use of `consensus' on
206: {\em unbounded\/} hardware can implement `test-and-set'.
207: In \cite{Pl89,SSW90,He91} it is argued that a
208: bounded solution can be obtained by combining several intermediate
209: constructions, like so-called ``sticky bits'',
210: but no explicit construction is presented to back up this claim.
211: To quote \cite{Pl89}: ``randomized consensus algorithms of Chor,
212: Israeli, and Li \cite{CIL87}, Abrahamson \cite{Ab88},
213: Aspnes and Herlihy \cite{AH}, and Attiya, Dolev, and Shavit \cite{ADS},
214: together with our construction imply that polynomial number of safe bits is
215: sufficient to convert a safe implementation into a (randomized)
216: wait-free one.''
217: Any such a ``layered'' construction will require
218: orders of magnitude more primitive building blocks like
219: one-writer one-reader bits than the direct construction we present below.
220: Wait-free $n$-process test-and-set can be implemented
221: deterministically from wait-free two-process test-and-set, \cite{AGTV91},
222: showing that the impossibility of a deterministic algorithm
223: for $n$-process test-and-set is solely due to the two-process case.
224:
225: {\bf Present Results:}
226: Despite the frequent use of randomized wait-free test-and-set
227: in the literature, no explicit construction for the basic ingredient,
228: randomized wait-free two-process
229: test-and-set, has appeared in print. Our
230: construction, \cite{TV90}, has been subsumed and referred to long since,
231: for example in \cite{AGTV91,PTTV98,EHW98,BPSV00}, but other
232: interests prevented us publishing a final version earlier.
233: The construction is optimal or close to optimal.
234: The presented algorithm directly
235: implements wait-free test-and-set between two processes
236: from single-writer single-reader atomic shared registers.
237: Randomization means that the algorithm contains a
238: branch conditioned on the outcome of a fair coin flip (as in
239: \cite{Ra82}).
240: We use a finite-state based proof technique
241: for verifying correctness and worst-case expected execution length
242: in the spirit of \cite{CGP00}.
243: Our construction is very simple: it uses two 4-valued 1-writer
244: 1-reader atomic variables.
245: The worst-case expected number of elementary steps (called ``accesses''
246: in the remainder of the paper) in a test-and-set operation
247: is $11$, whereas a reset always takes 1 access.
248:
249:
250: \section{Preliminaries}
251: Processes are sequentially executed finite programs
252: with bounded local variables communicating through
253: single-writer, multi-reader bounded
254: wait-free atomic registers (shared variables).
255: The latter are a common model for interprocess
256: communication through shared memory as discussed briefly
257: in Section~\ref{sect.intro}.
258: For details see \cite{La86,LTV89} and for use and motivation
259: in distributed protocols see \cite{BarD89,BorG93,HerS93}.
260:
261: \subsection{Shared Registers, Atomicity}
262: The basic building blocks of our construction are
263: 4-valued 1-writer
264: 1-reader atomic registers.
265: Every read/write register is {\em owned} by one process.
266: Only the owner of a register can write it, while only one other
267: process can read it. In one {\em access} a process can
268: either:
269: \begin{itemize}
270: \item
271: Read the value of a register;
272: \item
273: Write a value to one of its own registers;
274: \item
275: Moreover, following the read/write of a register
276: the process possibly flips a local coin (invokes a random number generator
277: that returns a random bit), preceded or
278: followed by some local computation.
279: \end{itemize}
280:
281: We require the system to be {\em atomic}:
282: every access of a process can be thought to
283: take place in an indivisible instance
284: of time and in every indivisible time instance at most
285: one access by one process is executed. The atomicity requirement induces
286: in each actual system execution
287: total orders on the set of all of
288: the accesses by the different processes, on the set of accesses
289: of every individual process, and on the set of
290: read/write operations executed on each individual register.
291: The {\em state} of the system gives
292: for each process:
293: the contents of the program counter, the contents
294: of the local variables, and the contents of the owned shared registers.
295: Since processes execute sequential programs,
296: in each state every process has at most a single
297: access to be executed next. Such accesses are
298: {\em enabled} in that state.
299:
300: \subsection{Adversary}
301: There is an {\em adversarial} scheduling demon that in each state
302: decides which enabled access is executed next, and thus
303: determines the sequence of accesses of the system execution.
304: There are two main types of adversaries: the {\em oblivious}
305: adversary that uses a fixed schedule independent of the
306: system execution, and the much stronger {\em adaptive}
307: adversary that dynamically adapts the schedule based on
308: the past initial segment of the system execution. Our results
309: hold against the adaptive adversary---the strongest
310: adversary possible.
311:
312: \subsection{Complexity}
313: The computational complexity of a randomized distributed algorithm
314: in an adversarial setting and the corresponding notion of wait-freeness
315: require careful definitions.
316: For the rigorous
317: novel formulation of adversaries as restricted measures over the set
318: of system executions we refer to the Appendix of \cite{PTTV98}.
319: For the simple application in this paper we can assume that
320: the notions of global (system) execution, wait-freeness,
321: adaptive adversary, and expected complexity are familiar.
322: A randomized distributed algorithm is {\em wait-free}
323: if the expected number of read/writes to shared
324: memory by every participating process is bounded
325: by a finite function $f(n)$, where $n$ is the number of processes.
326: The expectation is taken over the probability measure
327: over all randomized global (system) executions against the worst-case
328: adaptive adversary.
329:
330: \section{Test-and-Set Implementation}
331: We first specify the semantics of the target object:
332:
333: \begin{definition}\label{def.targetsemantics}
334: An {\em atomic test-and-set object} $X$ is a {\em global variable},
335: associated with $n$ processes
336: $P_0 ,\ldots, P_{n-1}$, exhibiting the
337: following functionality:
338: \begin{itemize}
339: \item
340: The value of $X$ is 0 or 1;
341: \item
342: Every process $P_i$ has a {\em local binary
343: variable} $x_{i}$ which it alone can read or write;
344: \item
345: At any time exactly one
346: of $X, x_{0} ,\ldots, x_{n-1}$ has value 0, all others
347: have value 1 (we assume the global time model);
348: \item
349: A process $P_i$ with $x_{i} = 1$
350: can atomically execute a {\em test-and-set} operation $\tau$:
351: \begin{hist}
352: read $x_{i} := X$; write $X := 1$; return $x_{i}$.
353: \end{hist}
354: \item
355: A process~$P_i$ with $x_{i} = 0$ can atomically execute a {\em reset} operation
356: $\rho$:
357: \begin{hist}
358: $x_{i} := 1$; write $X := 0$.
359: \end{hist}
360: \end{itemize}
361: This specification naturally leads to
362: the definition of the {\em state\/} of the
363: test-and-set object as an element of
364: $\{\free, 0,\ldots,n-1\}$ corresponding to the unique local variable
365: out of $X, x_{0}, \ldots , x_{n-1}$ that has value 0. Here $\free$ is the state
366: that none of the $x_i$'s is 0.
367: Formally, the specification is given later as a finite automaton
368: in Definition~\ref{def.FA1}.
369: \end{definition}
370: Since ``atomicity'' means that the operation is executed
371: in a single indivisible time instant, and, moreover, in every such
372: time instant at most one operation execution takes place,
373: the effect of a test-and-set operation by process $P_i$ is that
374: $x_i :=0$ iff all $x_j \neq 0$ for all $j \neq i$, and $x_i =1$ otherwise.
375: The effect of a reset operation by $P_i$ is only defined for
376: initially $x_i = 0$ and $x_j \neq 0$ for all $j \neq i$, and results
377: in $x_i :=1$.
378: To synthesise the target object from more elementary objects,
379: we have to use a sequence of atomic accesses to these elementary objects.
380: By adversary scheduling these sequences may be interleaved arbitrarily.
381: Yet we would like to have the effect of an atomic execution
382: of the test-and-set operations and the reset operations by
383: each process. To achieve such a ``virtual'' atomic execution
384: we proceed
385: as follows:
386:
387: \begin{definition}
388: An {\em implementation} of a
389: {\em test-and-set} operation $\tau$ or a {\em reset} operation $\rho$
390: by a process $P$ is an algorithm executed by $P$ that results in
391: an ordered sequence
392: of accesses of that process to elements of a set
393: $\{R_{0}, \ldots ,R_{m-1}\}$ of atomic shared variables,
394: interspersed with local computation and/or local coin flips. The sequence
395: of accesses is determined by the,
396: possibly randomized, algorithm,
397: and the values returned by the ``read'' accesses to shared variables.
398: We denote an access by
399: $(P,R,A)$, meaning that process $P$
400: executes access $A$ (read or write a ``0'' or ``1'')
401: on shared variable $R$. The implementation must satisfy the
402: specification of the target test-and-set semantics of Definition
403: \ref{def.targetsemantics} restricted to process $P$.
404: Formally, the specification is given later as a finite automaton
405: in Definition~\ref{def.FA2}.
406: \end{definition}
407:
408: \begin{definition}
409: A {\em local execution} of a process $P$ consists of the (possibly
410: infinite) sequence
411: of test-and-set operations and reset operations it executes,
412: according to the implementation,
413: each such operation $a \in \{\tau, \rho \}$
414: provided with a {\em start} time $s(a)$
415: and a {\em finish} time $f(a)$---we assume a global time model.
416: Note that $s(a)$ coincides with the time of execution of the
417: first access in the ordered sequence consituting $a$,
418: and $f(a)$ coincides the time of execution of
419: the last access in the ordered sequence
420: constituting $a$.
421: By the atomicity of the individual accesses in the global time model,
422: all accesses are executed at different time instants.
423: In certain cases (which we show to have zero probability)
424: it is possible that $f(a)$ is not finite (because the algorithm
425: executes infinitely many loops with probability $\frac{1}{2}$ each).
426: \end{definition}
427:
428: \begin{definition}
429: Let the local execution of process $P_i$ consist of
430: the ordered sequence of operations
431: $a_1^i , a_2^i , \ldots$ ($0 \leq i \leq n-1$).
432: A {\em global execution} consists of the $({\cal A}, \rightarrow)$
433: where ${\cal A} = \{a_j^i : j=1,2, \ldots , \; 0 \leq i \leq n-1 \}$
434: and $\rightarrow$ is a partial order on the elements of ${\cal A}$
435: defined by $a \rightarrow b$ iff $f(a) < s(b)$ (the last access of $a$
436: precedes the first of $b$). We require that
437: the number of $b$ such that $b \rightarrow a$ is finite for each $a$.
438: \end{definition}
439:
440: A test-and-set operation
441: or reset operation by a particular process may consist
442: of more than one access, and therefore the
443: local executions by the different processes may happen concurrently
444: and asynchronously. This has the effect that
445: a {\em global execution} can correspond to many
446: different interleavings.
447:
448: \begin{definition}
449: Consider a global execution.
450: An {\em interleaving} of the accesses by the different processes associated
451: with the global execution is
452: a (possibly infinite) totally ordered
453: sequence $(P^1,R^1,A^1), (P^2,R^2,A^2) \ldots$,
454: where $(P^i,R^i,A^i)$ is the $i$th access,
455: respecting
456: \begin{itemize}
457: \item
458: The start times
459: and finish times determined by the local executions; and
460: \item
461: the order of the accesses in the local executions.
462: \end{itemize}
463: \end{definition}
464:
465: The implementation should guarantee that
466: the functionality of the implementation is ``equivalent'',
467: in an appropriate sense,
468: to the functionality of the target test-and-set object, and
469: in particular satisfies the ``linearizability requirement'' \cite{HW}
470: (also called ``atomicity'' in \cite{La86}).
471:
472: \begin{definition}
473: The system {\em implements} the target test-and-set object if
474: the system is initially in state $\free$, and
475: we can extend $\rightarrow$ on ${\cal A}$ to a total
476: order $\arp$ on ${\cal A}$ with an initial element, satisfying:
477: \begin{itemize}
478: \item From state $\free$, a successful test-and-set operation
479: $\tau$ executed by process $P_i$ (setting $x_i :=0$)
480: moves the system
481: to state $i$ at some time instant in the interval $[s(\tau), f(\tau)]$;
482: \item from state $i$, a reset operation $\rho$ executed by process
483: $P_i$ moves the system
484: to state $\free$ at some time instant in the interval $[s(\rho),f(\rho)]$;
485: \item From state $i$, every operation execution different from
486: a reset by process $P_i$ leaves the system
487: invariant in state $i$; and
488: \item No other state transitions than the above are allowed.
489: \end{itemize}
490: The implementation must satisfy the
491: specification of the target test-and-set semantics of Definition
492: \ref{def.targetsemantics}.
493: Formally, the specification is given later as a finite automaton
494: in Definitions~\ref{def.FA3} and \ref{def.FA4}.
495: \end{definition}
496:
497:
498: To prove that a protocol
499: executed by all processes is an implementation of the target test-and-set
500: object it suffices to show that every possible interleaving that can
501: be produced by the processes executing the protocol in every global
502: execution, starting from the $\free$ state, satisfies the above
503: requirements.
504:
505: \section{Algorithm}
506:
507: \begin{figure*}[htbp]
508:
509: \centerline{\epsfbox{prot.ps}}
510:
511: \caption{State Chart}
512: \label{prot2}
513: \end{figure*}
514:
515: %
516: %ref1: explain intuition behind me,he,choose,rst.
517: %
518: We give a test-and-set implementation between two processes,
519: process~$P_{0}$ and process~$P_{1}$.
520: The construction uses two 4-valued shared read/write variables
521: $R_{0}$ and $R_{1}$. The four values are
522: `me', `he', `choose', `rst'---chosen
523: as a mnemonic aid explained below.
524: Process~$P_i$ solely writes variable $R_{i}$, its own variable, and
525: solely reads $R_{1-i}$.
526: For this reason the reads and writes in the protocol
527: don't need to be qualified by the shared variables they access.
528: The protocol, for process~$P_i$ ($i=0,1$), is presented
529: as both a finite state chart, Figure~\ref{prot2} and as
530: the program below. The state chart representation will simplify
531: the analysis later.
532: The transitions in the state chart are labeled with reads $r(value)$
533: and writes $w(value)$ of the shared variables, where $value$
534: denotes the value read or written.
535: The 11 states of the state chart are split
536: into 4 groups enclosed by dotted lines. Each group is
537: an equivalence class consisting of
538: the set of states in which process $P_i$'s own shared variable $R_i$
539: has the same value.
540: That is, the states in a group are equivalent in the sense that
541: process~$P_{1-i}$ cannot distinguish between them by reading $R_{i}$.
542: Accordingly, the inter-group transitions are writes to $R_{i}$,
543: whereas the intra-group transitions are reads of $R_{1-i}$.
544: Each group is named after the corresponding value of the
545: %
546: %ref1: no group names in fig1!
547: % fig1 confusing. what is initial state? what are double circles?
548: %
549: own shared variable $R_i$. The state chart is deterministic, but for
550: a coin flip which is modeled by the two inter-group transitions in
551: the ``choose'' group, representing the two outcomes
552: of a fair coin flip.
553: Doubly circled states are ``idle'' states (no
554: operation execution is in progress), and singly circled states
555: are intermediate states in an operation execution that is in
556: progress.
557:
558: A program representation of the protocol,
559: for process~$P_i$, is given below.
560: An occurrence of $R_{i}$ not preceded by `write'
561: (similarly, $R_{1-i}$ not preceded by `read') as usual refers to the last value
562: written to it (resp. read from it).
563: The conditional `rnd(true,false)'
564: represents the boolean outcome `true' or `false' of a fair coin flip.
565: The system is initialized with value `rst' in shared variables $R_0,R_1$.
566: In our protocol, all assignments to local variables consist of
567: contents read from
568: shared variables. To simplify, we abbreviate statements like
569: ``$r_{1-i} := R_{1-i}$; while $r_{1-i}=r_i$ do \ldots $r_{1-i} := R_{1-i}$.''
570: to
571: ``while read $R_{1-i}=R_i$ do \ldots ''.
572: Here, $r_i$ is the local variable containing the value
573: last written to shared variable $R_i$ and $r_{1-i}$ is the local
574: variable storing the last read value of shared variable $R_{1-i}$,
575: for process $P_i$. This way, our (writing of the) protocol
576: can dispense with local variables
577: altogether.
578:
579: \begin{prot}
580: test\_and\_set: \\
581: \\
582: if $R_{i}=$ he AND read $R_{1-i}\neq$ rst \\
583: then return 1 \\
584: write $R_{i}:=$ me \\
585: while read $R_{1-i}=R_{i}$ do \\
586: \jump write $R_{i}:=$ choose \\
587: \jump if read $R_{1-i}=$ he OR \\
588: \jump \jump \jump ($R_{1-i}=$ choose AND rnd(true,false)) \\
589: \jump then write $R_{i}:=$ me \\
590: \jump else write $R_{i}:=$ he \\
591: if $R_{i}=$ me \\
592: then return 0 \\
593: else return 1 \\
594: \\
595: reset: \\
596: \\
597: write $R_{i}:=$ rst
598: \end{prot}
599:
600: It can be verified in the usual way that the state chart
601: represents the operation of the program.
602: The intuition is easily explained
603: using the state chart.
604: The default situation is where both processes are idle,
605: which corresponds to being in the `rst' state.
606: If process~$P_i$ starts a test-and-set
607: then it writes $R_{i} :=$ me (indicating its desire to take the 0),
608: and checks by reading $R_{1-i}$ whether process~$P_{1-i}$ agrees
609: (by {\em not\/} having $R_{1-i} =$ me).
610: If so, then $P_i$ has successfully completed a test-and-set by
611: obtaining the 0 and, implicitly, setting the global variable $X :=1$ .
612: In this case process~$P_{1-i}$
613: cannot get 0 until process~$P_i$ does a reset by writing $R_{i} :=$ rst.
614: While $R_{i}=$ me, process~$P_{1-i}$ can only move from state `me'
615: to state `notme' and on via states `choose', `tohe' and `he' to `tst1',
616: where it completes its test-and-set operation by failure to obtain the 0.
617:
618: The only complication arises if both processes
619: see each other's variable equal to `me'.
620: In this case they are said to {\em disagree\/} or to be {\em in conflict}.
621: They then proceed to the `choose' state from where they decide between
622: going for 0 or 1,
623: according to what the other process is seen to be doing.
624: (It is essential that this decision be made in a neutral state,
625: without a claim of preference for either 0 or 1.
626: If, for example, on seeing a conflict, a process would change preference
627: at random, then a process cannot know for sure whether the other one agrees
628: or is about to write a changed preference.)
629:
630: The deterministic choices, those made if the other's variable is read
631: to contain a value different
632: from `choose', can be seen to lead to a correct resolution
633: of the conflict. A process ending up in the `tst1' state makes sure
634: that its test-and-set resulting in obtaining the 1 is justified,
635: by remaining in that state
636: until it can be sure that the other process has taken the 0.
637: %
638: %ref1: not clear how this is reflected in code
639: %
640: Only if the other process is seen to be in the `rst' state it
641: resumes trying to take the 0 itself.
642:
643: Suppose now that process~$P_i$ has read $R_{1-i}=$ choose and
644: is about to flip a coin. Assume that process~$1-i$ has already
645: moved to one of the states `tome'/`tohe' (or else reason with the processes
646: interchanged). With 50 percent chance,
647: process~$P_i$ will move to the opposite state as did process~$P_{1-i}$,
648: and thus the conflict will be resolved.
649:
650: In the proof of Theorem~\ref{theo.scci} (below) we establish that
651: the probability of each loop
652: through the `choose' state is at most one half, and the expected number
653: of `choices' (transitions from state choose) is at most two.
654: This indicates that the worst case expected test-and-set length is 11.
655: Namely, starting from the `tst1' state,
656: it takes 4 accesses to get to state `choose', another 4 accesses to loop back
657: to `choose' and 3 more accesses to reach `tst0'/`tst1'.
658: The reset operation always takes 1 access.
659:
660: \section{Proof of Correctness}
661: The proof idea is as follows: We give a specification of a correct
662: implementation of two-process test-and-set in the form of a
663: finite automaton (Figure~\ref{hybrid}). We then show that
664: all initial segments of
665: every possible interleaving of accesses by two processes
666: $P_0$ and $P_1$, both executing the algorithm of the state chart
667: (Figure~\ref{prot2}), are accepted by the finite automaton.
668: Moreover, the sequence of states of the finite automaton
669: in the acceptance process induces a linear order on the
670: operation execution of the implemented processes that extends
671: the partial order induced by the start and finish times of the
672: individual operation executions. Thus, the implementation is
673: both correct and atomic. Essentially, the proof is given
674: by Figure~\ref{tabletje}, which gives the state of the specification finite
675: automaton for every reachable combination of states which
676: processes $P_0$ and $P_1$ can attain in their respective copies
677: of the state chart
678: (Figure~\ref{prot2}). By analysis of the state chart,
679: or Figure~\ref{tabletje}, we upper bound the expectation of the number
680: of accesses of every operation execution of the implementation by
681: a small constant.
682: Hence the implementation is wait-free.
683:
684: Let $h$ be an interleaving corresponding to a
685: global execution $({\cal A},\ar)$ of two processes running the protocol
686: starting from the initial state.
687: Let $\{s(a),f(a): a \in {\cal A} \}$
688: be the set of time instants that start or finish an operation execution,
689: each such time instant corresponding to an access $(P,R,A)$.
690: Let $B$ denote the set these accesses.
691: Recall that if $a$ is a reset, then we have $s(a)=f(a)$ and there is
692: but a single access executing this operation.
693:
694: By definition, $h|B$, the restriction of $h$ to the accesses in $B$,
695: completely determines the partial order $\ar$. If, for
696: every $a \in A$ we can choose a single access $(P,R,A)_a$ in the sequence
697: of accesses constituting the operation execution of $a$, such that
698: if $a \rightarrow b$ then $(P,R,A)_a$ precedes $(P,R,A)_b$ in $h$,
699: then we are done. Namely, we can imagine an operation $a$
700: as executing atomically at the time instant of atomic access $(P,R,A)_a$,
701: and the total order $\arp$ defined by $a \arp b$ iff $(P,R,A)_a$
702: precedes $(P,R,A)_b$ in $h$, extends the partial order $\ar$.
703: Denote the set $\{(P,R,A)_a : a \in {\cal A}\}$ by $C$.
704: We have to show that for every $h$ as defined above such a $C$ can be found.
705:
706:
707: \begin{definition}{\em Specification of two-process atomic test-and-set:}
708: \label{def.FA1}
709: The definition of the target atomic test-and-set for two processes, process $P_0$
710: and process $P_1$, is captured by
711: finite automaton FA1 in Figure~\ref{atomic}, which accepts all possible
712: sequences of atomic test-and-set and reset operations (all states final).
713: The states are labeled with the owner of the 0-bit.
714: The arcs representing actions of process $P_1$ are labeled,
715: whereas the non-labeled arcs represent the
716: corresponding actions of process $P_0$:
717: resulting in setting $x_1 := 1$.
718:
719: \begin{figure}[htbp]
720:
721: \centerline{\epsfbox{tasbit2.ps}}
722:
723: \caption{FA1: Specification of two-process atomic test-and-set object}
724: \label{atomic}
725: \end{figure}
726: \end{definition}
727:
728: \begin{definition}{\em Specification
729: of wait-free atomic test-and-set restricted to a single process:}
730: \label{def.FA2}
731: Figure \ref{semantics} shows the semantics required of a
732: correct implementation
733: of a wait-free test-and-set object as a finite automaton FA2,
734: that accepts all sequences of accesses by a single process $P_i$
735: ($i=0,1$) executing a correct wait-free atomic test-and-set protocol:
736: (all states final):
737: \begin{itemize}
738: \item the access starting a test-and-set operation execution, denoted s(tas),
739: \item the atomic occurrence of a test-and-set operation execution
740: returning 0, denoted tas0,
741: \item the atomic occurrence of a test-and-set operation execution
742: returning 1, denoted tas1,
743: \item the access finishing a test-and-set operation execution
744: returning 0, denoted f(tas0),
745: \item the access finishing a test-and-set operation execution
746: returning 1, denoted f(tas1),
747: \item the single access corresponding to a complete reset
748: operation execution, denoted rst.
749: \end{itemize}
750: These are the events in $B \cup C$ restricted to a process $P_i$.
751: The reason for not splitting a reset operation execution
752: into start, atomic occurrence,
753: and finish is that it is implemented in our protocol as a single
754: atomic write where the above three transitions coincide.
755: As before, doubly circled states are ``idle'' states (no
756: operation execution is in progress), and singly circled states
757: are intermediate states in an operation execution that is in
758: progress.
759:
760: \begin{figure}[htbp]
761:
762: \centerline{\epsfbox{pcs.ps}}
763:
764: \caption{FA2: Specification of 1-process wait-free implementation
765: of atomic test-and-set}
766: \label{semantics}
767: \end{figure}
768: \end{definition}
769:
770: \begin{definition}{\em Specification
771: of two-process wait-free atomic test-and-set:}
772: \label{def.FA3}
773: The proof that our implementation is correct consists in
774: demonstrating that it satisfies the specification in the form
775: of the finite automaton FA3
776: in Figure~\ref{hybrid} below (again all states are final).
777:
778: \begin{figure}[htbp]
779:
780: \centerline{\epsfbox{hybrid.ps}}
781:
782: \caption{FA3/FA4: Specification of two-process wait-free atomic test-and-set}
783: \label{hybrid}
784: \end{figure}
785:
786: Formally \cite{LT87}, FA3 is the composition of FA1 with two copies of
787: FA2, in the I/O Automata framework, as follows:
788: It is drawn as a cartesian product of the two component
789: processes---transitions of process~$P_0$ are drawn vertically and
790: those of process~$P_1$ horizontally. For clarity, the transition names
791: are only given once: only for process~$P_1$.
792: Identifying the starts and finishes of test-and-set operation executions $a$
793: with their atomic occurrence $(P,R,A)_a$ by
794: collapsing the $\s$ and $\f$ arcs,
795: FA3 reduces to the atomic test-and-set diagram FA1.
796: Identifying all nodes in the same column (row) reduces FA3
797: to FA2 of process~{$P_0$} (process~{$P_1$}).
798:
799: In the states labeled `a' through `h', neither process owns the $0$;
800: the system is in state $\free$.
801: In the states labeled `i' through `n', process~$1$ owns the $0$;
802: the system is in state $1$.
803: In the states labeled `o' through `t', process~$0$ owns the $0$;
804: and the system is in state $0$.
805: \end{definition}
806:
807: The broken transitions of
808: Figure~\ref{hybrid} correspond to the access
809: $(P,R,A)_a \in C$, required for a correct implementation,
810: where the atomic execution of operation $a$
811: can be virtually situated. Recall that this is only relevant
812: for $a$ is a test-and-set operation, since the reset operation
813: is implemented in the protocol already in a single atomic access
814: of a shared primitive variable.
815:
816: \begin{definition}\label{def.FA4}
817: Let FA4 be the (nondeterministic) finite automaton
818: obtained from FA3 by turning the broken transitions of
819: Figure~\ref{hybrid}, which correspond to the unknown but
820: existing access $(P,R,A)_a \in C$ where the execution of $a$
821: can be virtually situated,
822: into $\epsilon$-moves.
823: \end{definition}
824:
825: \begin{lemma}\label{lem.1}
826: Acceptance of $h|B$ by FA4 implies that $({\cal A},\ar)$ is linearizable:
827: partial order $\ar$ can be extended to a total order $\arp$ such
828: that the sequence of operation executions in ${\cal A}$ ordered
829: by $\arp$ satisfy the test-and-set semantics specification of
830: Definition~\ref{def.FA1}.
831: \end{lemma}
832:
833: \begin{proof}
834: If FA4 accepts $h|B$, then, corresponding to the $\epsilon$
835: moves, we can augment the sequence $h|B$ with an access $(P,R,A)_a$ in
836: the interval $[s(a),f(a)]$ of each operation
837: execution $a \in {\cal A}$---or select the single access involved
838: if $s(a)=f(a)$ as in the case of a reset operation execution---
839: to obtain a new sequence $h'$ that is accepted by FA3.
840: By the way FA1 composes FA3, it accepts $h'|C$, the subsequence of atomic
841: accesses $(P,R,A)_a$ with $a \in {\cal A}$ contained in $h'$.
842: Furthermore, letting $t(a)$ denote the time of access $(P,R,A)_a$,
843: we have $a \ar b$ iff
844: $t(a) \leq f(a) \leq s(b) \leq t(b)$. Defining
845: $a \arp b$ if $t(a) < t(b)$, the total order of accesses in $h'|C$,
846: then $\arp$ is a total order that extends the partial order $\ar$.
847: That is, the sequence of operation executions of ${\cal A}$,
848: linear ordered by $\arp$, is accepted by FA1.
849: \end{proof}
850:
851: \begin{figure*}[htbp]
852:
853: \begin{center}
854: \footnotesize
855: \begin{tabular}{|c|ccccccccccc|}
856: \hline
857: & rst & tst0 & notme & me & tome & choose & tohe & he & nothe & tst1 & free
858: \\ \hline
859: rst & d{\bf 10} & l{\bf 10} & cek{\bf 10} & ek{\bf 10} & ek{\bf 10} & c{\bf 10} & c{\bf 10} & c{\bf 10} & c{\bf 10} & d{\bf 10} & ek{\bf 10}
860: \\
861: tst0 & s{\bf 1} & * & rt{\bf 1} & rt{\bf 1} & rt{\bf 1} & r{\bf 1} & r{\bf 1} & r{\bf 1} & r{\bf 1} & s{\bf 1} & rt{\bf 1}
862: \\
863: notme & agp{\bf 8} & jn{\bf 8} & imoq{\bf 8} & imoq{\bf 8} & * & imoq{\bf 8} & imoq{\bf 8} & o{\bf 4} & * & p{\bf 4} & *
864: \\
865: me & gp{\bf 9} & jn{\bf 9} & imoq{\bf 9} & imoq{\bf 9} & imoq{\bf 9} & o{\bf 1} & o{\bf 1} & o{\bf 1} & o{\bf 1} & p{\bf 1} & imoq{\bf 9}
866: \\
867: tome & gp{\bf 10} & jn{\bf 10} & * & imoq{\bf 10} & imoq{\bf 10} & imoq{\bf 6} & o{\bf 2} & o{\bf 2} & imoq{\bf 6} & p{\bf 2} & *
868: \\
869: choose & a{\bf 3} & j{\bf 3} & imoq{\bf 7} & i{\bf 3} & imoq{\bf 7} & imoq{\bf 7} & imoq{\bf 7} & o{\bf 3} & imoq{\bf 7} & p{\bf 3} & *
870: \\
871: tohe & a{\bf 2} & j{\bf 2} & imoq{\bf 6} & i{\bf 2} & i{\bf 2} & imoq{\bf 6} & imoq{\bf 10} & imoq{\bf 10} & * & p{\bf 6} & *
872: \\
873: he & a{\bf 1} & j{\bf 1} & i{\bf 1} & i{\bf 1} & i{\bf 1} & i{\bf 1} & imoq{\bf 9} & imoq{\bf 9} & imoq{\bf 9} & p{\bf 5} & *
874: \\
875: nothe & a{\bf 4} & j{\bf 4} & * & i{\bf 4} & imoq{\bf 8} & imoq{\bf 8} & * & imoq{\bf 8} & imoq{\bf 8} & p{\bf 4} & *
876: \\
877: tst1 & d{\bf 11} & l{\bf 11} & k{\bf 11} & k{\bf 11} & k{\bf 11} & k{\bf 11} & k{\bf 11} & k{\bf 11} & k{\bf 11} & * & *
878: \\
879: free & gp{\bf 10} & jn{\bf 10} & * & imoq{\bf 10} & * & * & * & * & * & * & *
880: \\ \hline
881: \end{tabular}
882: \end{center}
883: \caption{Table verification of correctness and wait-freedom}
884: \label{tabletje}
885:
886: \end{figure*}
887:
888: Recall that Figure~\ref{prot2} is the state chart
889: of the execution of the implementation
890: of an operation by a single process. Each process can be in a particular
891: state of the state chart. Let $(s_0,s_1)$ denote the state
892: of the system with process $P_i$ in state $s_i$ ($i\in \{0,1\}$).
893:
894: \begin{definition}
895: The {\em initial} system state is $(rst,rst)$.
896: A system state $(s_0,s_1)$ is {\em reachable} from the initial system
897: state $(rst,rst)$ if there is a sequence $h$ arising from the execution
898: of our test-and-set implementation, represented by the state chart
899: of Figure~\ref{prot2}, starting from the initial state
900: and ending in state $(s_0,s_1)$.
901: \end{definition}
902:
903: \begin{example}\label{ex.reach1}
904: \rm
905: In the initial state both processes are in state
906: `rst'.
907: Process~$P_0$
908: can start a test-and-set by executing $w(me)$ and entering
909: state $me$.
910: Suppose process~$P_1$
911: now starts a test-and-set: it executes $w(me)$ and moves to state
912: $me$.
913: Hence, system states $(me,rst)$ and $(me,me)$ are reachable states.
914: \end{example}
915:
916: \begin{definition}
917: The {\em representative set} of a
918: reachable system state $(s_{0},s_{1})$ is
919: a nonempty set $S_{s_{0},s_{1}}$ of FA3/FA4 states,
920: as in Figure~\ref{hybrid}, such that:
921: For every sequence of accesses $h$ starting in the
922: initial state and ending in state $(s_{0},s_{1})$,
923: the set $S_{s_{0},s_{1}}$ is
924: the set of states in which FA4 can be after processing $h|B$,
925: excluding those states that have outgoing moves that are $\epsilon$-moves only.
926: \end{definition}
927:
928: \begin{example}\label{ex.reach2}
929: \rm
930: We elaborate Example~\ref{ex.reach1}.
931: In the initial state both processes are in state
932: `rst'.
933: The corresponding start state $d$ of FA4 gives the associated
934: (in this case singleton) representative set $\{d\}$.
935: When process~$P_0$
936: executes $w(me)$ and enters
937: state $me$, the resulting system state is $(me,rst)$
938: with the associated representative set $\{g,p\}$ of FA4 states.
939: That is, the system is now either in state $g$,
940: meaning that process~$P_0$ has executed $s(tas)$, or in state $p$
941: meaning that process~$P_0$ has executed $s(tas)$ and also
942: $tas0$ atomically.
943: In the scenario of Example~\ref{ex.reach1}, process~$P_1$
944: now executes $w(me)$ and moves to state
945: $me$, resulting in the system state $(me,me)$.
946: The corresponding representative set of FA4 states is $\{i,m,o,q\}$.
947: State $m$ says process~$P_1$ has executed
948: $s(tas)$ and $tas0$ atomically, while process~$P_0$
949: has only executed $s(tas)$---hence the system was previously in state $g$
950: and not in state $p$. State $i$ says process~$P_1$ has executed
951: $s(tas)$ and $tas0$ atomically, while process~$P_0$
952: has executed $s(tas)$ and $tas1$
953: atomically---and hence the system was previously in state $g$
954: and not state $p$. States $o$ and $q$ imply the same state
955: of affairs with the roles of process~$P_0$ and process~$P_1$
956: interchanged, and the previous system state is
957: either $p$ or $g$.
958: (The correspondence between reachable states and their representative
959: sets is exhaustively established in Claim~\ref{claim.1} below.)
960: \end{example}
961:
962: \begin{lemma}\label{lem.2}
963: Let $h$ be a sequence of accesses arising from the execution
964: of our test-and-set implementation, represented by the state chart
965: of Figure~\ref{prot2}, starting from the initial state
966: (both processes in state `rst'). Then, every initial segment of
967: $h|B$ is accepted by FA4 starting from initial state `d'.
968: \end{lemma}
969:
970: \begin{proof}
971: We show that the set of letters in an entry in the table
972: of Figure~\ref{tabletje}
973: is a representative set
974: for the state of process $P_0$, indexing the row, and the
975: state of process $P_1$, indexing the column.
976: The entries were chosen excluding all states from the representative
977: sets with all outgoing moves consisting of $\epsilon$-moves
978: (but the representative sets contain the
979: states the outgoing $\epsilon$-moves of the excluded states point to).
980: This gives the most insight
981: into the workings of the protocol by considering only the result
982: of executing $\epsilon$-moves from a state
983: if its only outgoing moves are $\epsilon$-moves.
984: A $*$-entry indicates an unreachable state pair.
985: (The number ending an entry gives
986: the expected number of accesses to finish the current
987: operation execution of process~$P_0$---and by symmetry, that for
988: an equivalent state pair with respect to $P_1$. We will use this later.)
989: Thus, every state $(s_0,s_1)$ of the implementation execution
990: corresponds with a set of states $S_{s_0,s_1}$ of FA4.
991:
992: \begin{claim}\label{claim.1}
993: The representative sets are given by the entries of Figure~\ref{tabletje}.
994: \end{claim}
995: \begin{proof}
996: The proof of the claim is contained
997: in the combination of Figures~\ref{prot2}, \ref{hybrid}, \ref{tabletje}.
998: Below we give the inductive argument. The mechanical verification
999: of the subcases has been done by hand, and again by machine.
1000: The setting up of the exhaustive list subcases and subsequent verification
1001: by a computer program is the essennce of a finite-state proof. In
1002: this particular case, exceptionally, the finite state machines involved (and
1003: the table of representative sets) have been minimized so that
1004: ``mechanical'' verification by hand by the reader is still feasible.
1005: Induction is on the length of the sequence of accesses:
1006: \begin{description}
1007: \item
1008: {\em Base Case:}
1009: Initially, after an empty sequence of accesses, FA4 is in
1010: the state
1011: $\{d\} = S_{rst,rst}$.
1012: \item
1013: {\em Induction:}
1014: Every non-reachable state has a $*$-entry in the table of Figure \ref{tabletje}.
1015: Consider an arbitrary atomic transition from a reachable state $(s_{0},s_{1})$
1016: to a state $(t_{0},t_{1})$, that is, using a single arc in the state chart in
1017: Figure~\ref{prot2} for either process $P_0$ or $P_1$.
1018: This way, either $t_0 = s_0$ or
1019: $t_1 = s_1$ but not both. Then, for every FA4 state $y \in S_{t_{0},t_{1}}$,
1020: Figure~\ref{hybrid},
1021: according to the table of Figure~\ref{tabletje},
1022: there is an FA4 state $x \in S_{s_{0},s_{1}}$ according to
1023: Figure~\ref{hybrid}, such that
1024: FA4 can move from $x$ to $y$ by executing: either the access corresponding
1025: to the transition in the state chart in Figure~\ref{prot2},
1026: if that access belongs to $B$,
1027: or no access otherwise (there is
1028: a sequence of $\epsilon$-moves from $x$ to $y$).
1029: \end{description}
1030:
1031:
1032: \end{proof}
1033: Since every reachable state of the system $(s_0,s_1)$, with $s_i$
1034: ($i \in \{0,1\})$ a state of the state chart of Figure~\ref{prot2},
1035: has a representative set in FA4, Figure~\ref{hybrid}, and every state of
1036: of FA4 is an accepting state, the lemma follows from Claim~\ref{claim.1}.
1037: \end{proof}
1038:
1039: \begin{theorem}
1040: The algorithm represented by state chart
1041: of Figure~\ref{prot2}
1042: correctly implements an atomic test-and-set object.
1043: \end{theorem}
1044: \begin{proof}
1045: By Lemma \ref{lem.2} the implementation by the state chart in Figure~\ref{prot2}
1046: correctly implements the specification of two-process test-and-set
1047: given by Figure~\ref{hybrid}. The implementation is linearizable
1048: (atomic) by Lemma~\ref{lem.2}. The system makes progress (every
1049: operation execution is executed completely except for possibly
1050: the last one of each process) since $h|B$ contains only the start
1051: and finish accesses of each operation execution performed by
1052: the implementation.
1053: \end{proof}
1054:
1055: \begin{theorem}
1056: \label{theo.scci}
1057: The algorithm represented by state chart
1058: of Figure~\ref{prot2}
1059: is wait-free: the expected number of accesses to shared variables
1060: never exceeds 11 during execution of an operation.
1061: \end{theorem}
1062: \begin{proof}
1063: In Figure~\ref{prot2} every arc is an access. Double circled
1064: states are idle states (in between completing an operation execution
1065: and starting a new one). Consider process $P_0$ (the case
1066: for process $P_1$ is symmetrical). The longest path without
1067: completing an operation and without cycling is from state `tst1':
1068: tst1, free, me, notme, choose, tohe, he, tst1. This takes 7 accesses.
1069: Four of these accesses are parts of a potential cycle of length 4.
1070: The remainder is 3 accesses outside the potential cycle.
1071: In state `choose',
1072: the outgoing arrow is a random choice only
1073: when process $P_1$ is also in the CHOOSE
1074: group. If it is, then with $\frac{1}{2}$ probability $P_1$
1075: makes (or has already made) a choice which will cause process
1076: $P_0$ to loop back to the `choose' state again.
1077: This can happen
1078: again and again.
1079: The expected number
1080: of iterations of loops is $\sum_{i=1}^{\infty}
1081: i \left( \frac{1}{2} \right)^{i} = \frac{1}{2} (1- \frac{1}{2})^{-2} = 2$.
1082: Since a loop has length 4, this gives a total of expected accesses of 8
1083: for the loops. Together with 3 non-loop accesses
1084: the total is at most $11$ accesses.
1085: Such a computation holds for every state
1086: in the state chart of Figure~\ref{prot2}, the only loop being
1087: the one discussed but the longest possible path is the one starting from
1088: `tst1'. For definiteness,
1089: we have in fact computed the expected number
1090: of accesses for every accessible state $(s_0,s_1)$ according to
1091: the state chart of Figure~\ref{prot2}, and added that number
1092: to the representative set concerned in the table of Figure~\ref{tabletje}.
1093: Since the expected number of accesses is
1094: between 1 and 11 for all operation executions,
1095: the algorithm given by the state chart of Figure~\ref{prot2} is wait-free.
1096: \end{proof}
1097:
1098: To aid intuition, we give an example of checking a few transitions below,
1099: as well as giving the interpretation.
1100:
1101: \begin{example}
1102: We elaborate and continue Examples~\ref{ex.reach1}, \ref{ex.reach2}.
1103: In the initial state both processes are in state
1104: `rst'.
1105: In Figure~\ref{hybrid},
1106: the table entry $d10$ gives the corresponding start state $d$ of FA4.
1107: The worst-case expected number
1108: of accesses for a test-and-set by process~$0$ is 10. Process~$P_0$
1109: can start a test-and-set by executing $w(me)$ and entering
1110: state $me$. The corresponding table entry $gp9$
1111: indicates in Figure~\ref{hybrid}
1112: that the system is now either in state $g$
1113: meaning that process~$P_0$ has executed $s(tas)$, or in state $p$
1114: meaning that process~$P_0$ has executed $s(tas)$ and also
1115: $tas0$ atomically.
1116: The expected number of accesses is now $9 \leq 10-1$. Suppose process~$P_1$
1117: now starts a test-and-set: it executes $w(me)$ and moves to state
1118: $me$. The corresponding table entry $imoq9$
1119: gives the system state as one
1120: possibility in $\{i,m,o,q\}$ in Figure~\ref{hybrid}
1121: and the expected number of accesses for execution of test-and-set by
1122: process~$P_0$ is still 9. State $m$ says process~$P_1$ has executed
1123: $s(tas)$ and $tas0$ atomically, while process~$P_0$
1124: has only executed $s(tas)$---hence the system was previously in state $g$
1125: and not in state $p$. State $i$ says process~$P_1$ has executed
1126: $s(tas)$ and $tas0$ atomically, while process~$P_0$
1127: has executed $s(tas)$ and $tas1$
1128: atomically---and hence the system was previously in state $g$
1129: and not state $p$. States $o$ and $q$ imply the same state
1130: of affairs with the roles of process~$P_0$ and process~$P_1$
1131: interchanged, and the previous system state is
1132: either $p$ or $g$.
1133:
1134: Note that at this point the system can also be in state
1135: $h$ of FA4---both processes having executed $s(tas)$
1136: but no process having executed $tas0$ or $tas1$. However, from $h$
1137: there are two $\epsilon$-moves possible, and no other moves,
1138: leading to $q$ and $m$. This corresponds to the fact that if both
1139: processes have executed $s(tas)$, one of them must return 0 and
1140: the other one must return 1.
1141: We have optimized the table
1142: entries by eliminating such spurious intermediate states $h$ with
1143: outgoing moves that are $\epsilon$-moves only.
1144:
1145: Process~$P_0$ might now read $R_{1} = me$, and move via state `notme'
1146: (table entry $imoq8$) by writing $R_{0} := choose$,
1147: to state `choose'. Process~$P_1$ is idle in the meantime.
1148: The table entry is now $i3$. This says that
1149: process~$P_1$ has atomically executed $tst0$, and process~$P_0$
1150: has atomically executed $tst1$. Namely, all subsequent schedules
1151: lead in 3 accesses of process~$P_0$ to state `tst1'---hence the expectation 3.
1152:
1153: The expected number of remaining accesses of process~$P_0$'s test-and-set
1154: has dropped from 8 to 3 by the last access since 8 was the worst-case
1155: which could be forced by the adversary. Namely, from the system
1156: in state $(notme, me)$, the adversary can schedule process~$P_1$
1157: to move to $(notme, notme)$
1158: with table entry $imoq8$, followed by a move of process~$P_1$ to
1159: state $(notme, choose)$ with table entry $imoq8$,
1160: followed by a move of process~$P_0$ to state $(choose,choose)$
1161: with table entry $imoq7$. Suppose the adversary now schedules
1162: process~$P_0$. It now flips a fair coin to obtain the conditional
1163: boolean $rnd(true,false)$. If the outcome is $true$, then
1164: the system moves to state $(tome, choose)$ with entry $imoq6$.
1165: If the outcome is $false$, then the system moves to state
1166: $(tohe, choose)$ with table entry $imoq6$. Given a fair coin,
1167: this access of process~$P_0$ correctly decrements the expected number
1168: of accesses. Suppose the adversary schedules process~$P_1$ in state
1169: $(choose, choose)$. Process~$P_1$ flips a fair coin.
1170: If the outcome is $true$ the system moves to state
1171: $(choose, tome)$ with table entry $imoq7$; if the outcome is $false$
1172: then the system moves to state $(choose, tohe)$ with
1173: table entry $imoq7$.
1174: \end{example}
1175:
1176: \section{Remark on Multi-Process Test-And-Set}
1177:
1178: The obvious way to extend the given solution to more than two processes
1179: would be to arrange them at the leaves of a binary tree.
1180: Then, a process wishing to execute an $n$-process test-and-set,
1181: would enter a tournament, as in \cite{PF77},
1182: by executing a separate two-process test-and-set for each node
1183: on the path up to the root.
1184: When one of these fails, it would again descend,
1185: resetting all the tas-bits on which it succeeded, and return 1.
1186: When it succeeds ascending up to the root, it would return 0
1187: and leave the resetting descend to its $n$-process reset.
1188:
1189: The intuition behind this tree approach is that if a process $i$ fails
1190: the test-and-set at some node $N$, then another process $j$ will get
1191: to the root successfully and thus justify the value 1 returned by the former.
1192:
1193: The worst case expected length of the $n$-process operations is only
1194: $\log n$ (binary logarithm) times more than that of the two-process case.
1195:
1196: Unfortunately, this straightforward extension does not work.
1197: The problem is that the other process $j$ need not be the
1198: one responsible for the failure at node $N$, and might have started
1199: its $n$-process test-and-set only after process $i$ completes its own.
1200: Clearly, the resulting history cannot be linearized.
1201:
1202: Nonetheless, it turns out that with a somewhat more
1203: complicated construction we can {\em deterministically}
1204: implement $n$-process test-and-set using
1205: two-process test-and-set as primitives \cite{AGTV91}.
1206: This shows that the impossibility of deterministic
1207: wait-free atomic $n$-process test-and-set is completely
1208: due to the impossibility of deterministic wait-free atomic two-process
1209: test-and-set. This latter problem we have just solved by a
1210: simple direct randomized algorithm.
1211:
1212: \begin{thebibliography}{9}
1213:
1214: \bibitem{Ab88} K. Abrahamson, On achieving consensus using shared memory,
1215: {\em Proc. 7th ACM Symp. Principles of Distributed Computing}, 1988,
1216: 291--302.
1217:
1218: \bibitem{AADGMS90} Y. Afek, H. Attiya, D. Dolev, E. Gafni, M. Merritt,
1219: N. Shavit, Atomic snapshots of shared memory,
1220: {\em Journal of the ACM}, 40:4(1993), 873-890.
1221:
1222: \bibitem{AGTV91}
1223: Y. Afek, E. Gafni, J. Tromp, P.M.B. Vit\'anyi, Wait-free test-and-set,
1224: pp. 85-94 in: {\em Proc. 6th Workshop on Distributed Algorithms (WDAG-6)},
1225: Lecture Notes in Computer Science, vol. 647, Springer Verlag,
1226: Berlin, 1992.
1227:
1228: \bibitem{ADS}
1229: H. Attiya, D. Dolev, N. Shavit,
1230: Bounded Polynomial Randomized Consensus,
1231: {\em Proc.8th ACM
1232: Symp. Principles of Distributed Computing}, 1989, 281--293.
1233:
1234: \bibitem{An90} J.H. Anderson, Multiwriter composite registers,
1235: {\em Distributed Computing}, 7:4(1994), 175-195.
1236:
1237: \bibitem{As90} J. Aspnes, Time- and space-efficient randomized
1238: consensus,
1239: {\em Journal of Algorithms}, 14:3(1993), 414-431.
1240:
1241: \bibitem{AH}
1242: J. Aspnes, M. Herlihy,
1243: Fast randomized consensus using shared memory,
1244: {\em Journal of Algorithms}, 11:3(1990), 441-461,
1245:
1246: \bibitem{BarD89}
1247: A. Bar-Noy and D. Dolev,
1248: A partial equivalence between shared-memory
1249: and message-passing in an asynchronous fail-stop distributed
1250: environment, {\em Mathematical Systems Theory}, 26(1993), 21--39.
1251: %Shared Memory vs. Message-passing in an Asynchronous Distributed
1252: %Environment.
1253: %In {\em Proc. 8th ACM Symposium on Principles of Distributed
1254: %Computing}, 1989, 307--318.
1255:
1256: \bibitem{BorG93}
1257: E. Borowsky and E. Gafni,
1258: Immediate Atomic Snapshots and Fast Renaming,
1259: {\em Proc. 11th ACM Symp. on Principles of Distributed
1260: Computing}, 1992, pp.~41--52.
1261:
1262: \bibitem{BPSV00}
1263: H. Buhrman, A. Panconesi, R. Silvestri, and P. Vitanyi
1264: On the importance of having an identity or, is consensus really
1265: Universal?, {\em Distributed Computing Conference (DISC'00)},
1266: Lecture Notes in Computer Science, Vol. 1914,
1267: Springer-Verlag, Berlin, 2000, 134--148.
1268:
1269: \bibitem{BJLFP82}
1270: J.E Burns, P.Jackson, N.A. Lynch, M.J. Fischer, G.L. Peterson,
1271: Data Requirements for Implementation of N-process Mutual Exclusion
1272: Using a Single Shared Variable, {\em J. Assoc. Comput. Mach.},
1273: 29(1982),183--205.
1274:
1275:
1276: \bibitem{CIL87} B. Chor, A. Israeli, M. Li,
1277: Wait--Free Consensus Using Asynchronous Hardware,
1278: {\em SIAM J. Comput.}, 23:4(1994), 701--712.
1279:
1280: \bibitem{CGP00}
1281: E. M. Clarke, O. Grumberg, and D. Peled, {\em Model Checking}, MIT Press, 2000.
1282:
1283: \bibitem{DS89} D. Dolev and N. Shavit,
1284: Bounded concurrent time-stamp systems are constructible,
1285: {\em Siam J. Comput.}, 26(2):418-455, 1997.
1286:
1287: \bibitem{EHW98} W. Eberly, L. Higham, J. Warpechowska-Gruca,
1288: Long-lived, fast, waitfree renaming with optimal name space and high throughput,
1289: {\em Proc. 12th Intn'l Distributed Computing Conference (DISC'98)},
1290: Lecture Notes in Computer Science, 1499,
1291: Springer-Verlag, Berlin, 1998.
1292:
1293: \bibitem{HV01}
1294: S. Haldar, P.M.B. Vitanyi,
1295: Bounded concurrent timestamp systems using vector clocks,
1296: {\em J. Assoc. Comput. Mach.}, 49:1(2002).
1297:
1298:
1299: \bibitem{He91a}
1300: M. Herlihy,
1301: Wait-free synchronization.
1302: {\em ACM Trans. Progr. Lang. Syst.}, 13:1(1991),
1303: 124--149.
1304:
1305: \bibitem{He91} M.P. Herlihy,
1306: Randomized Wait-Free Concurrent Objects,
1307: {\em Proc. 10th ACM Symp. Principles of Distributed Computing}, 1991, 11--21.
1308:
1309:
1310: \bibitem{HerS93}
1311: M. Herlihy and N. Shavit,
1312: The topological structure of asynchronous computability,
1313: {\em J. Assoc. Comp. Mach.}, 46:6(1999), 858-923.
1314:
1315: \bibitem{HW}
1316: M. Herlihy, J. Wing,
1317: Linearizability: A correctness condition for concurrent
1318: objects, {\em ACM Trans. Program. Languages and Systems},
1319: 12(1990), 463--492.
1320:
1321:
1322: \bibitem{FisLP}
1323: M.J. Fischer, N.A. Lynch, and M.S. Paterson,
1324: Impossibility of Distributed Consensus with One Faulty Processor.
1325: {\em J. Assoc. Comput. Mach.} 32:2(1985), 374--382.
1326:
1327:
1328:
1329: \bibitem{IL87} A. Israeli and M. Li, Bounded Time-Stamps,
1330: {\em Distributed Computing} 6(1993), 205--209.
1331:
1332: \bibitem{La86} L. Lamport, On Interprocess Communication Parts I and II,
1333: {\em Distributed Computing} 1(1986), 77--101.
1334:
1335: \bibitem{LA-A87} M. Loui, H.H. Abu-Amara, Memory requirements for
1336: agreement among unreliable asynchronous processes, pp. 163--183 in:
1337: {\em Advances in Computing Research}, Vol. 4, JAI Press, 1987.
1338:
1339: \bibitem{LTV89} M. Li, J. Tromp, P.M.B. Vit\'{a}nyi,
1340: How to share concurrent
1341: wait-free variables,
1342: {\em J. Assoc. Comp. Mach.}, 43 (1996), 723-746.
1343:
1344: \bibitem{Ly96}
1345: N.A. Lynch, {\em Distributed Algorithms},
1346: Morgan Kaufmann, 1996.
1347:
1348:
1349: \bibitem{LT87} N.A. Lynch and M. Tuttle,
1350: An Introduction to Input/Output automata,
1351: {\em CWI-Quarterly}, 2:3(1989), 219--246.
1352:
1353:
1354: \bibitem{PTTV98}
1355: A. Panconesi, M. Papatrintafilou, P. Tsigas, P. Vitanyi,
1356: Randomized Naming Using Wait-Free Shared Variables,
1357: {\em Distributed Computing}, 11(1998), 113--124.
1358:
1359:
1360: \bibitem{PF77} G.L. Peterson, M. Fischer, Economical
1361: solutions for the critical section problem in a distributed
1362: system, {\em Proc. 9th ACM Symp. Theory of Computing}, 1977, 91--97.
1363:
1364: \bibitem{Pe83} G.L. Peterson, Concurrent reading while writing,
1365: {\em ACM Trans. Programming Languages and Systems},
1366: 5:1(1983), 46--55.
1367:
1368: \bibitem{Pl89} S. Plotkin, Sticky bits and universality of consensus,
1369: {\em Proc. 8th ACM Symp. Principles of Distributed Computing},
1370: 1989, 159--175.
1371:
1372: \bibitem{SinAG94}
1373: A.K. Singh, J.H. Anderson, and M.G. Gouda,
1374: The Elusive Atomic Register Revisited,
1375: {\em J. Assoc. Comput. Mach.}, 41:2(1994), 311--339.
1376:
1377:
1378: \bibitem{Sc88} R. Schaffer, {\em On the correctness of atomic multi-writer
1379: registers}, Technical Report MIT/LCS/TM-364, MIT lab. for
1380: Computer Science, June 1988.
1381:
1382: \bibitem{SSW90}
1383: M. Saks, N. Shavit, and H. Woll.
1384: Optimal time randomized consensus -- making resilient algorithms fast
1385: in practice,
1386: {\em 2nd ACM Symp. On Discrete Algorithms}, 1991, 351--362.
1387:
1388: \bibitem{Ra82} M.O. Rabin, The choice coordination problem.
1389: {\em Acta Informatica}, 17(1982), 121--134.
1390:
1391: \bibitem{TV90}
1392: J.~Tromp and P.~M.~B. Vitanyi,
1393: Randomized wait-free test-and-set,
1394: Manuscript, November 1990.
1395:
1396: \bibitem{VA86} P.M.B. Vitanyi, B. Awerbuch,
1397: Atomic Shared Register Access by Asynchronous Hardware, {\em Proc. 27th
1398: IEEE Symp. Foundations of Computer Science}, 1986, 233--243.
1399: (Errata, Ibid.,1987)
1400:
1401: \end{thebibliography}
1402:
1403: \end{document}
1404: