# Constant RMR Recoverable Mutex under System-wide Crashes

Prasad Jayanti111Dartmouth College<EMAIL_ADDRESS>Siddhartha V.
Jayanti222Google Research and MIT<EMAIL_ADDRESS><EMAIL_ADDRESS>Anup Joshi333Yahoo<EMAIL_ADDRESS>
(January 17, 2023)

###### Abstract

We design two Recoverable Mutual Exclusion (RME) locks for the system-wide
crash model. Our first algorithm requires only $O(1)$ space per process, and
achieves $O(1)$ worst-case RMR complexity in the CC model. Our second
algorithm enhances the first algorithm to achieve (the same) $O(1)$ space per
process and $O(1)$ worst-case RMR complexity in both the CC and DSM models.
Furthermore, both algorithms allow dynamically created threads of arbitrary
names to join the protocol and access the locks. To our knowledge, these are
the only RME locks to achieve worst-case $O(1)$ RMR complexity assuming
nothing more than standard hardware support. In light of Chan and Woelfel’s
$\Omega(\log n/\log\log n)$ worst-case RMR lower bound for RME in the
individual crash model, our results show a separation between the system-wide
crash and individual crash models in worst-case RMR complexity in both the CC
and DSM models.

##  1 Introduction

The emergence and widespread commercial availability of non-volatile memory
(NVM), which retains its state despite system-wide crashes caused by power
outages [29, 30, 31] has ushered in the era of recoverable (a.k.a. durable)
algorithms. Such algorithms allow processes that crash, and lose the contents
of their process registers due to a system-wide power outage, to smoothly
recover upon restart and resume computing from the time of the crash [17, 2,
12, 13, 16, 14, 15, 16, 19, 20, 21, 22, 5, 6]. Due to the centrality of mutual
exclusion (mutex) locks in concurrent computing [11], the recoverable mutual
exclusion (RME) lock has received a lot of attention [16, 14, 15, 16, 19, 20,
21, 22, 5, 6]. The principal goal of RME lock research has been to design
algorithms that have low “RMR” complexity for both “cache-coherent” (CC) and
“distributed shared memory” (DSM) systems, in the face of crashes. In this
paper, we design RME locks that tolerate system-wide crashes for both CC and
DSM systems. Our locks have just constant worst-case RMR complexity, allow
access to dynamically created threads, and require only constant space per
accessing thread. Our algorithm uses only the read, write, compare-and-swap
(CAS) and fetch-and-store (FAS) instructions, which are commonly supported on
modern machines.

In the rest of this section, we review the background, state our
contributions, and compare them to the state of the art.

###  1.1 Failure models

In practice, crashes are generally caused by power-failures, which cause all
processes in the system to crash simultaneously [17]. Recoverable algorithms
for such system-wide crashes, have been widely studied in both the systems and
theory communities [17, 15, 12, 13, 27, 9, 7, 8, 24]. A lot of theory
literature, particularly related to RME, has also studied the individual crash
model [14, 16, 19, 20, 21, 22, 5, 6, 4, 3] in which individual processes can
crash and restart even as other processes run unaffected. Algorithms designed
for this individual crash model work for system-wide crashes, because a
sequence of individual crashes can simulate a system-wide crash. Algorithms
designed directly for system-wide crashes however, can exploit the structure
in the simultaneous failure to potentially achieve better efficiency
guarantees. The main result of this paper—a constant worst-case RMR algorithm
for RME tolerating system-wide crashes—displays such an efficiency boost in
light of Chan and Woelfel’s $\Omega(\log n/\log\log n)$ worst-case RMR lower
bound for RME in the individual crash model; here $n$ is the number of
processes participating in the algorithm.

###  1.2 RME Lock: Problem Statement

A standard mutex lock $\ell$ consists of two methods —$\ell.\mbox{\em
try}_{p}()$ and $\ell.\mbox{\em exit}_{p}()$ for each process $p$—and a
recoverable mutex (RME) lock consists of one additional method, called
$\ell.\mbox{\em recover}_{p}()$. Initially each process is in the remainder
section and in a correct state. From the remainder section, when in a correct
state, a process $p$ may invoke and execute $\ell.\mbox{\em try}_{p}()$. When
$\ell.\mbox{\em try}_{p}()$ returns, $p$ is said to be in the critical section
(CS). From the CS, $p$ next invokes and executes $\ell.\mbox{\em exit}_{p}()$.
When this method completes, $p$ is back in the remainder section and in a
correct state.

At any time, a process may execute a normal step or a system-wide crash may
occur. In a normal step of a process $p$, $p$ executes the instruction pointed
to by its program counter $PC_{p}$. When a system-wide crash occurs, for each
process $p$, $p$ enters a crashed state, $PC_{p}$ is set to $p$’s remainder
section, and all $p$’s other registers and local variables that are not in the
NVM are set to arbitrary values. When $p$ subsequently restarts, it is
required to invoke $\ell.\mbox{\em recover}_{p}()$. When this method
completes, it returns either IN_REM or IN_CS and $p$ is said to move back from
the crashed to the correct state. A return value of IN_REM by $\ell.\mbox{\em
recover}_{p}()$ puts $p$ in the remainder section and a return value of IN_CS
puts $p$ in the CS.

Two fundamental properties of an RME lock are:

  * •

Mutual Exclusion: At most one process is in the CS at any time.

  * •

Critical Section Reentry (CSR) [16]: If a process $p$ crashes while in the CS,
no other process may enter the CS before $p$ reenters the CS. In other words,
if $p$ crashes in the CS, the subsequent execution of $\ell.\mbox{\em
recover}_{p}()$ that returns, must put $p$ back in the CS.

The CSR property is required because $p$ could be manipulating some shared
data structure in the CS at the time of the crash, in which case the crash
could leave the data structure in an inconsistent state. The CSR property
ensures that $p$ gets the opportunity to enter the CS before anyone else and
clean up its act. (We assume, as is standard in the RME literature, that the
CS is idempotent.)

An RME lock must also ensure progress in fair runs—runs where no process stays
in the CS forever and no process permanently stops taking steps, unless it is
in the Remainder in a correct state. Our algorithm satisfies the following
liveness property:

  * •

Starvation Freedom: In every fair run, if a process $p$ executes
$\ell.\mbox{\em try}_{p}()$ and no crash occurs during this execution of the
try method, then the method will eventually complete, leading to $p$ entering
the CS.

Two other important properties are [21]:

  * •

Bounded Recovery: If a process $p$ executes $\ell.\mbox{\em recover}_{p}()$
without crashing, $p$ returns from the method in a constant number of its own
steps.

  * •

Bounded Exit: If a process $p$ executes $\ell.\mbox{\em exit}_{p}()$ without
crashing, $p$ returns from the method in a constant number of its own steps.

Bounded Recovery ensures that if $p$ crashes while in the CS, once it
restarts, it will be able to walk back into the CS without being obstructed by
others [21]. Bounded Exit stipulates that there should be no hindrances when
all that a process wants to do is to give up the lock.

###  1.3 Dynamic Joining and Adaptive Space

Previous RME locks were designed for a fixed set of $N$ processes labeled
$1,\ldots,N$, and have required pre-allocated shared-arrays of length $O(N)$
or $O(N^{2})$ for communication. We design RME locks that allow dynamic
joining, i.e., processes that are created on-the-fly (a.k.a. threads) of
arbitrary names can access our locks. Thus, there is no pre-defined limit $N$
on the number of processes that may access our locks. To achieve this
property, we design all communication structures in our protocol to be
pointer-based, so we can eliminate the need for pre-allocated fixed-length
arrays.

Our space usage is adaptive, i.e., the space grows with the actual number of
processes $n$ that use our lock (in contrast to space being a function of a
pre-defined maximum number of processes $N$ for which the lock is designed).

###  1.4 RMR Complexity

The complexity of mutual exclusion algorithms is commonly studied in two
multiprocessor models: cache-coherent (CC) and distributed shared memory
(DSM).

In the CC model, each process has a cache. A read operation by a process $p$
on a shared variable $X$ fetches a copy of $X$ from shared memory to $p$’s
cache, if a copy is not already present in the cache. Any non-read operation
on $X$ by any process invalidates copies of $X$ at all caches. An operation on
$X$ by $p$ counts as a remote memory reference (RMR) if either the operation
is not a read or $X$’s copy is not already present in $p$’s cache. When a
process crashes, its cache contents are lost.

In the DSM model, shared memory is partitioned between the processes. Each
shared variable $X$ resides in exactly one of the parts. Any operation on $X$
by a process $p$ counts as an RMR if and only if $X$ is not in $p$’s part of
shared memory.

A passage of a process $p$ in a run starts from the time it leaves the
remainder (in the correct or the crashed state) to the earliest subsequent
time when $p$ returns to the remainder (in the correct or the crashed state).

The passage complexity or the RMR complexity of an RME algorithm is the worst-
case number of RMRs that a process incurs in a passage.

###  1.5 Our Contribution

We design two RME algorithms that tolerate system-wide crashes. Our first
algorithm has $O(1)$ worst-case RMR complexity for CC systems. Our second
algorithm enhances the first, and has $O(1)$ worst-case RMR complexity for
both CC and DSM systems. Both algorithms require only $O(1)$ space per
process, allow dynamic joining, and satisfy all of the properties stated in
Section 1.2—Mutual Exclusion, CSR, Starvation Freedom, Bounded Recovery, and
Bounded Exit. Both algorithms use just the standard fetch-and-store (FAS) and
compare-and-swap (CAS) instructions for synchronization.444The operation
$r\leftarrow\mbox{\bf FAS}(X,v)$ has the following semantics: if $X$’s value
is $u$ immediately before the instruction, it writes $u$ in the CPU register
$r$ and updates $X$’s value to $v$. The operation $r\leftarrow\mbox{\bf
CAS}(X,u,v)$ has the following semantics: if $X$’s value is $u$, the operation
changes $X$’s value to $v$ and writes true in the CPU register $r$; otherwise,
$X$ remains unchanged and the operation writes false in $r$.

###  1.6 Comparison to the state of the art

Four previous works explore the possibility of constant RMR solutions for RME
locks [14, 19, 15, 5]. Two of these works require hardware support for
instructions that atomically manipulate two unrelated words of shared-
memory—the fetch-and-store-and-store (FASAS) instruction and the double-word-
compare-and-swap (DCAS) instruction—to achieve $O(1)$ worst-case RMR
complexity in the individual process crash model [14, 19]. To our knowledge,
no current systems support these instructions.

Chan and Woelfel designed an RME algorithm for the independent crash model,
which achieves amortized $O(1)$ RMR complexity and requires unbounded space
[5]. A lower bound by the same authors shows that $O(1)$ worst-case RMR
complexity cannot be achieved in the individual crash model [6], and confirms
that the worst-case $\Theta(\log n/\log\log n)$ RMR algorithms of Golab and
Hendler [14] and Jayanti et al. [20] are the best possible for CC and DSM in
that model of computation, where $n$ is number of processes accessing the
lock.

Golab and Hendler (GH) designed a pair of RME algorithms for the system-wide
crash model, which assume that “processes receive additional information from
the environment regarding the occurrence of the failure,” to achieve $O(1)$
worst-case RMR [15]. Specifically, the GH algorithms assume that processes
have access to a shared failure-counter, which an out-of-band environmental
mechanism must increase after each crash event. Their CC algorithm can be
implemented to allow dynamic joining and uses only constant space per process,
like ours. Their DSM algorithm however, does not allow dynamic joining,
requires a knowledge of the maximum number of processes $N$ that might access
the lock, and uses $O(N)$ space per process, i.e., a total of $O(N^{2})$
space. Both our CC and DSM algorithms allow dynamic joining and use only
$O(1)$ space per process, i.e., a total of $O(n)$ space, where $n$ is the
actual number of processes that access the lock in the run (hence, $n$ can be
much smaller than $N$).

The GH algorithms do not satisfy the Bounded Recovery and Bounded Exit
properties, but satisfy a stronger version of Starvation Freedom, which states
that in an infinite run with infinitely many super passages, every process
that executes the try section eventually reaches the critical section.

To our knowledge, our algorithms are the only RME locks to achieve worst-case
$O(1)$ RMR complexity assuming nothing more than standard hardware support.
They are also the first to achieve the Bounded Recovery and Bounded Exit
properties, alongside $O(1)$ RMR complexity, and the first to achieve $O(1)$
space per process in the DSM model. Furthermore, in light of Chan and
Woelfel’s $\Omega(\log n/\log\log n)$ worst-case RMR lower bound for RME in
the individual crash model, our results show a separation between the system-
wide crash and individual crash models in worst-case RMR complexity in both
the CC and DSM models (without assuming a failure detector).

###  1.7 Related research on RME

Golab and Ramaraju formalized the RME problem and designed several algorithms
by adapting traditional mutual exclusion algorithms [16]. Ramaraju [28],
Jayanti and Joshi [21], and Jayanti, Jayanti, and Joshi [19] designed RME
algorithms that support the First-Come-First-Served property [25]. Golab and
Hendler [14] and Jayanti, Jayanti, and Joshi [20] presented RME algorithms
that have sub-logarithmic RMR complexity. Dhoked and Mittal gave a lock with
sub-logarithmic RMR complexity that is additionally adaptive [10]. A recent
lower bound by Chan and Woelfel [6] matches the upper bounds of Jayanti,
Jayanti, and Joshi [20] and Golab and Hendler [14] to pin down the worst-case
RMR complexity of RME in the individual crash model as $\Theta(\log n/\log\log
n)$ for both the CC and DSM models. Interestingly, Chan and Woelfel’s previous
work shows that, given unbounded space, $O(1)$ RMR complexity can be achieved
in the amortized sense. RME locks that are abortable have also been designed:
the first by Jayanti and Joshi uses CAS and has logarithmic RMR complexity
[22], and a subsequent one by Katzan and Morrison achieves sublogarithmic RMR
complexity using CAS and Fetch&Add [23]. All these results apply to the
individual crash model of failure. As discussed above, Golab and Hendler [15]
presented an algorithm that has $O(1)$ RMR complexity in the system-wide crash
model, assuming a failure detector.

###  1.8 Organization

In Section 2, we present an algorithm for an RME lock that has $O(1)$ RMR
complexity for only the CC model. In Section 4, we adapt this algorithm to
achieve $O(1)$ RMR complexity for both CC and DSM. We conclude in Section 5.

##  2 RME lock for CC

In this section, we present an algorithm for implementing an RME lock
${\mathcal{L}}$ for the system-wide crash model. This algorithm has $O(1)$ RMR
complexity on CC machines, and is displayed in Figure 1. We explain the ideas
underlying its design in Section 2.1, and provide a line-by-line commentary in
Section 2.2. We then provide an invariant based proof of correctness in
Section 3.

###  2.1 High level ideas

The algorithm uses the following persistent (NVM) variables. Some are shared
and the others, subscripted with $p$, are local to process $p$.

  * •

Seq and $\mbox{\sc S}_{p}$: Seq stores a sequence number that grows
monotonically, and the local variable $\mbox{\sc S}_{p}$ holds what process
$p$ believes to be the current sequence number. If $p$ crashes and
subsequently restarts, it increases Seq to $\mbox{\sc S}_{p}+1$.

  * •

$\mbox{\sc Lock}[0]$, $\mbox{\sc Lock}[1]$, $\mbox{\sc Lock}[2]$: These are
three instances of a standard (non-recoverable) mutex lock. Since our RME
lock’s properties will depend on the properties of these underlying “base
locks”, we instantiate these to be Lee’s queue locks [26], which we have
presented in Figure 6 in Appendix A, along with its properties.

To compete with other processes in order to obtain the ownership of the CS,
$p$ uses the lock numbered $\mbox{\sc S}_{p}\%3$.

  * •

$\mbox{\sc Stop}[0]$, $\mbox{\sc Stop}[1]$, $\mbox{\sc Stop}[2]$: These are
boolean variables and the variable $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]$
denotes whether $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ is in good condition or
not. That is to say that, if a crash occurred while a process was actively
using the lock $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ and the lock was not
subsequently reset, then the lock is not in good condition and hence should
not be used to gain access to the CS.

  * •

CSowner: This variable stores the name of the process in the CS of the
implemented recoverable lock ${\mathcal{L}}$ (i.e., the real CS and not that
of any of the three base lock). Its value is $\bot$ if no process is in the CS
of ${\mathcal{L}}$.

  * •

$\mbox{Active}_{p}$: This boolean local variable holds true while $p$ executes
the algorithm. Therefore, if $p$ jumps to the Remainder section because it
crashed while executing the algorithm, $\mbox{Active}_{p}$ has $true$. On the
other hand, if $p$ completes the algorithm normally (e.g., without crashing),
$\mbox{Active}_{p}$ has $false$ when $p$ reaches the Remainder section.

The idea is that, in order to compete for the recoverable lock
${\mathcal{L}}$, each process $p$ reads into $\mbox{\sc S}_{p}$ the sequence
in Seq and attempts to acquire the base lock $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3]$ (by executing $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3].\texttt{try}_{p}()$). For example, if processes $p$ and $q$ compete
for ${\mathcal{L}}$ when the sequence number is 10, they try to acquire
$\mbox{\sc Lock}[10\%3]$ (or $\mbox{\sc Lock}[1]$). If there are no crashes,
then each process acquires $\mbox{\sc Lock}[1]$, enters the CS of
${\mathcal{L}}$, and then releases $\mbox{\sc Lock}[1]$. Thus, $p$ and $q$
enter the CS of ${\mathcal{L}}$ one after the other and return to the
Remainder section.

For a more complex scenario, suppose that the system crashes while $p$ and $q$
are competing for $\mbox{\sc Lock}[1]$. The crash wipes out these process’ CPU
registers, thereby rendering $\mbox{\sc Lock}[1]$ unusable in the future. When
one of these processes, say $p$, subsequently restarts and enters
$\texttt{recover}_{p}()$ of ${\mathcal{L}}$, it infers from the value of
$true$ in $\mbox{Active}_{p}$ that it must have crashed while executing the
algorithm. So, $p$ advances Seq by writing 11 and goes on to acquire
$\mbox{\sc Lock}[11\%3]$, or $\mbox{\sc Lock}[2]$, if necessary. However,
suppose that a third process $r$ executes the algorithm before $p$ changes Seq
to 11. Since $r$ has no previous context, when it reads 10 in Seq, it simply
writes 10 in $\mbox{\sc S}_{r}$ and competes for $\mbox{\sc Lock}[10\%3]$
(i.e., in $\mbox{\sc Lock}[1]$), which could be stuck, but then $r$ doesn’t
know that. If $p$ now takes steps, it writes 11 in Seq and proceeds to compete
for $\mbox{\sc Lock}[11\%3]$ (i.e., $\mbox{\sc Lock}[2]$). Thus, at this
point, there are processes waiting at two different locks, namely, $\mbox{\sc
Lock}[1]$ and $\mbox{\sc Lock}[2]$. To prevent $r$ from being stuck forever at
$\mbox{\sc Lock}[10\%3]$, we require that while waiting in the
$\texttt{try}_{r}()$ procedure of $\mbox{\sc Lock}[10\%3]$, $r$ parallely also
checks whether $\mbox{\sc Stop}[10\%3]$ changes to $true$. On noticing a
change in $\mbox{\sc Stop}[10\%3]$, $r$ can promptly switch to $\mbox{\sc
Lock}[11\%3]$.

Could there be a scenario where processes could be waiting at three locks? The
answer is no. To see this, suppose that a system-wide crash occurs when Seq
has some value $v$. Processes that have not witnessed the value $v$ in Seq in
the past (such as process $r$ in the previous scenario) as well as processes
that saw $v$ in Seq but exited the algorithm normally will proceed to
$\mbox{\sc Lock}[v\%3]$, while those that had seen $v$ in Seq and experienced
the crash write $v+1$ in Seq and wait at $\mbox{\sc Lock}[(v+1)\%3]$. Thus,
there is no possibility of any process flocking to a third lock. In
particular, of the three base locks employed in the algorithm, we can be
certain that no process waits at $\mbox{\sc Lock}[(v-1)\%3]$. Since this lock
could be stuck from prior crashes, now is the ripe time to reset and keep it
ready for future use; so, $p$ resets $\mbox{\sc Lock}[(v-1)\%3]$ as it changes
Seq from $v$ to $v+1$. This observation that three base locks suffice and that
$\mbox{\sc Lock}[(v-1)\%3]$ should be reset when changing Seq from $v$ to
$v+1$ is a crucial insight in our algorithm.

|  |  |
---|---|---|---
Shared variables (stored in NVM)
|  |  $\mbox{\sc Seq}\in\mathbb{N}$, initially $1$.
|  |  $\mbox{\sc Lock}[0\cdots 2]$ is an array of base mutual exclusion locks, as implemented in Figure 6.
|  |  $\mbox{\sc Stop}[0\cdots 2]$ is an array of booleans, each initially false.
|  |  CSowner stores a process identifier or $\perp$, initially $\perp$.
|  Persistent variables local to process $p$ (stored in NVM)
|  |  $\mbox{Active}_{p}$ is a boolean, initially false.
|  |  $\mbox{\sc S}_{p}\in\mathbb{N}$, initially $1$.

|  |  |  |
---|---|---|---|---
|  1. |  Remainder Section
|  | procedure $\texttt{try}_{p}()$
| 2. |  $\mbox{Active}_{p}\leftarrow true$
|  3. |  $\mbox{\sc S}_{p}\leftarrow\mbox{\sc Seq}$
|  4. |  $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$ $\parallel$ wait till $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=true$
|  5. |  if $\mbox{\sc Seq}\neq\mbox{\sc S}_{p}$: go to Line 1
|  6. |  wait till $\mbox{\sc CSowner}=\perp$ $\parallel$ wait till $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=true$
|  go to Line 1
|  7. |  if $\mbox{\bf CAS}(\mbox{\sc CSowner},\perp,p)$: return IN_CS
|  8. |  if $\mbox{\sc Seq}\neq\mbox{\sc S}_{p}$:
|  9. |  |  $\mbox{\sc S}_{p}\leftarrow\mbox{\sc S}_{p}+1$
|  10. |  |  $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$
|  11. |  |  wait till $\mbox{\sc CSowner}=\perp$
|  12. |  |  if $\mbox{\bf CAS}(\mbox{\sc CSowner},\perp,p)$: return IN_CS
|  13. |  wait till $\mbox{\sc CSowner}=\perp$
|  14. |  $\mbox{\sc CSowner}\leftarrow p$
|  15. |  return IN_CS
|  16. |  Critical Section
|  | procedure $\texttt{exit}_{p}()$
|  17. |  if $\mbox{\sc S}_{p}=\mbox{\sc Seq}$:
|  18. |  |  $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$
|  19. |  $\mbox{\sc CSowner}\leftarrow\perp$
|  20. |  $\mbox{Active}_{p}\leftarrow\mbox{\it false}$
|  | procedure $\texttt{recover}_{p}()$
|  21. |  if $\mbox{Active}_{p}\wedge\mbox{\sc Seq}=\mbox{\sc S}_{p}$:
|  22. |  |  $\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\texttt{reset}_{p}()$
|  23. |  |  $\mbox{\sc Stop}[(\mbox{\sc S}_{p}-1)\%3]\leftarrow\mbox{\it false}$
|  24. |  |  $\mbox{\sc Seq}\leftarrow\mbox{\sc S}_{p}+1$
|  25. |  |  $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]\leftarrow true$
|  26. |  if $\mbox{\sc CSowner}=p$: return IN_CS
|  27. |  $\mbox{Active}_{p}\leftarrow\mbox{\it false}$
|  28. |  return IN_REM

Figure 1: Algorithm for an RME lock ${\mathcal{L}}$ for an arbitrary number of
processes of arbitrary names, for CC machines. Code shown for a process $p$.

###  2.2 Line-by-line commentary

In this section we informally describe the working of our algorithm presented
in Figure 1. We first describe how a process $p$ would execute the algorithm
in the absence of a crash, and then proceed to explain the working of the
algorithm in presence of a crash.

#### Crash-free attempt.

A process $p$ starts an attempt to enter the CS from the Remainder Section by
invoking the $\texttt{try}_{p}()$ procedure. At Line 1, $p$ sets
$\mbox{Active}_{p}$ to $true$ making a note to itself that it has started an
attempt. Subsequently, $p$ reads the current sequence number Seq into its
local variable $\mbox{\sc S}_{p}$ at Line 1, and proceeds by trying to acquire
the corresponding lock $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ at Line 1. While
executing $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$, $p$
simultaneously monitors the value of the corresponding stop flag, $\mbox{\sc
Stop}[\mbox{\sc S}_{p}\%3]$, by interleaving its steps between the try method
and the wait till at Line 1. If $\mbox{\sc S}_{p}\%3$ is indeed the current
lock, then $p$’s try attempt will eventually succeed. Otherwise, if another
process $q$ that previously crashed while active in the lock with sequence
number $\mbox{\sc S}_{p}$ restarts, it will increment Seq and set the flag
$\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]$ to true. When $p$ finishes Line 4, it
could have been because it successfully obtained the lock or because the stop
flag was raised. Thus, it checks whether the sequence number Seq was
incremented at Line 5, if so it abandons the $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3]$ and proceeds to update its sequence number at Line 9 and proceeds
to try to obtain the newly installed lock (as we explain later). Otherwise, if
$\mbox{\sc S}_{p}$ is still current (i.e. it still equals Seq), then $p$ waits
for the CS to become freed by spinning on CSowner at Line 6. Once again, $p$
is aware that the sequence number could be updated, so it simultaneously
monitors $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]$ and (just as before) proceeds
to Line 9 if the stop flag gets raised. If $p$ eventually finds the CS vacated
(i.e. $\mbox{\sc CSowner}=\perp$ at Line 1), it tries to establish ownership
of the CS by CASing its name into the CSowner field at Line 1. If $p$ succeeds
in the CAS, then it moves to the CS. Otherwise, as we explain in the
following, there could be two reasons that $p$ failed in the CAS after having
read that the CS is empty at Line 1. In the first case, the lock used by $p$
must have been an older lock that was part of a crash before $p$ enqueued
itself into it, and subsequently a new lock was installed that allowed another
process to enter the CS (all of this not noticed by $p$). In the second case
$p$ itself was enqueued in the latest lock, however, it lost to another
process $q$ that had enqueued itself into a older lock (just like $p$ in the
first case above). To find out which of the above two cases caused this CAS
failure, $p$ compares Seq with $\mbox{\sc S}_{p}$ at Line 1. If the two are
the same, $p$ knows it is in the right lock, hence, it goes to Line 1 to wait
for its turn to occupy the CS. Otherwise, $p$ tries for the latest active base
lock next, hence, it goes to Line 1.

From the above description, we see that $p$ could reach Line 1 in three
different ways: from Line 5, Line 6, or Line 8. In all the cases, $p$ knows
that the sequence number increased after its execution of Line 3. Since, $p$
knows that the sequence number could go up only once between two crashes (an
invariant maintained by our algorithm), it increments $\mbox{\sc S}_{p}$ by 1
(Line 1) to the current value of Seq. This time, when $p$ tries for the lock
$\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ at Line 10, it is guaranteed to
eventually succeed (if there is no system-wide crash), and thus does not need
to simultaneously monitor a stop flag. At Line 1 $p$ waits to ensure that the
CS is empty. It needs to ensure this for one of two reasons: either a process
acquired the CS before the crash and still continues to do so, or a process
succeeded in the CAS at Line 1 by coming through a lock before it was replaced
by the current lock that $p$ came from. Once $p$ is past Line 1, it attempts
to CAS its own name into CSowner if the CS is still empty. If $p$ succeeds in
the CAS, then it moves to the CS. Otherwise $p$ failed only because some other
process must have succeeded in the CAS at Line 1 as described above. $p$ waits
one more time at Line 1 to ensure that the CS is empty. Once $p$ reaches Line
1 it is sure that it reached the line by enqueuing into the latest active lock
and there could not be any more competition to it. Hence it writes its own
name into CSowner and moves to CS (Line 1).

In the $\texttt{exit}_{p}()$ procedure, $p$ first checks if the base lock that
it queued up and entered the CS from is still the active lock (Line 1). If it
is indeed still the active lock, $p$ executes the $\texttt{exit}_{p}()$
procedure of that lock at Line 1. Otherwise, $p$ knows that it is no longer in
the queue of the lock it used and hence doesn’t execute the
$\texttt{exit}_{p}()$ method of that lock. At Line 1 $p$ informs other
processes that it is giving up the CS by writing $\perp$ to CSowner. Finally,
at Line 1 $p$ sets $\mbox{Active}_{p}$ to $false$ to complete its attempt.

#### Recovery from a crash.

We now discuss what happens when $p$ crashes while executing an attempt. The
idea behind our algorithm is to keep an active instance of the base lock and
the number in Seq determines which of the three instances is active.
Therefore, in any configuration, $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ is the
active base lock. This idea guides a process on whether after a crash it needs
to setup a new lock or not. Thus, at Line 1, $p$ determines if it took any
meaningful steps prior to the crash, and if so, whether it might have
attempted to queue up in the currently active base lock. If
$\mbox{Active}_{p}=false$, $p$ is sure that it didn’t take any meaningful
steps before the crash and hence continues to Line 1 of the procedure (from
there it is sure to find $\mbox{\sc CSowner}\neq p$ and thus will return to
the Remainder completing the attempt). If $\mbox{Active}_{p}=true$ but
$\mbox{\sc S}_{p}\neq\mbox{\sc Seq}$, then $p$ knows that it no longer needs
to setup a new lock because either a new lock was already setup or the
currently active lock is not the one that $p$ queued itself into. Thus, $p$
would continue to Line 1. In the case where $\mbox{Active}_{p}=true$ and
$\mbox{\sc S}_{p}=\mbox{\sc Seq}$, $p$ might have enqueued itself into
$\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ at either of Lines 1 or 1. Hence,
assuming that $p$ itself has broken the queue structure of $\mbox{\sc
Lock}[\mbox{\sc Seq}\%3]$, it moves to setup a new lock at Lines 1-1. Our
algorithm maintains the invariant that $\mbox{\sc Lock}[(\mbox{\sc
Seq}+1)\%3]$ is always initialized, i.e., the next instance of Lock is always
kept ready to use. Therefore, before installing the next lock in sequence, $p$
readies the lock after the next lock in sequence to maintain the invariant. To
this purpose, at Line 1, $p$ first resets the lock $\mbox{\sc Lock}[(\mbox{\sc
S}_{p}-1)\%3]$, which is the lock coming up after the next lock in sequence
(i.e., lock numbered $(\mbox{\sc Seq}+2)\%3$ or $(\mbox{\sc Seq}-1)\%3$ is the
lock coming up after the next lock in sequence). $p$ then resets the Stop flag
associated with lock $\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3]$ at Line 1.
Next $p$ moves to signal that $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ should no
longer be used, therefore, it increments Seq by $1$ at Line 1. It then sets
$\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]$ to $true$ (at Line 1) so that any
processes that queued up at lock $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ in the
time between the previous crash and now know that they should move to the next
lock in sequence, i.e., $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$. An invariant our
algorithm maintains is that between two consecutive crashes, the value of Seq
is incremented at most once. To see how that is achieved consider the
following example. Suppose $p$, $q$, and $r$ committed to the value 10 by
reading Seq at Line 1 and noting into their respective variables $\mbox{\sc
S}_{p}$, $\mbox{\sc S}_{q}$, and $\mbox{\sc S}_{r}$. Assume that a crash
occurs after that and $p$ and $q$ restart immediately actively taking steps.
$p$ and $q$ both read $\mbox{\sc Seq}=\mbox{\sc S}_{p}$ and $\mbox{\sc
Seq}=\mbox{\sc S}_{q}$ and thus execute Lines 1-1 one after another. After
that $q$ executes Line 1 first to set Seq to 11 for the first time. Following
this, $p$ will execute Line 1 at most once before the next crash, and that
step wouldn’t change the value of Seq because $p$ would attempt to set it to
11, a value Seq already holds. Also, following the step by $q$, no matter when
$r$ starts taking steps, it will always find $\mbox{\sc Seq}=11$ which is not
the same as what $\mbox{\sc S}_{r}$ held prior to the crash. Hence, $r$ would
never change the value of Seq. Thus, with the execution of Line 1, $p$
completes the repair and moves to execute Line 1.

At Line 1 $p$ checks if it acquired access to the CS prior to the crash by
checking if $\mbox{\sc CSowner}=p$. If so, $p$ moves to the CS by returning
IN_CS from $\texttt{recover}_{p}()$. Otherwise, $p$ is sure that it has
repaired any issues that might have caused due to the crash and it can’t go in
the CS any more in the current attempt. Thus it sets the $\mbox{Active}_{p}$
flag to $false$ (Line 1) to signal the end of the attempt and returns IN_REM
(Line 1) to go back to the Remainder.

In the above, Line 1 may put $p$ into the CS, hence satisfying the CSR
property. Thus, in the $\texttt{exit}_{p}()$ procedure $p$ checks if it
entered the CS normally or due to the CSR property as mentioned above. If $p$
finds that $\mbox{\sc Seq}=\mbox{\sc S}_{p}$ at Line 1, it infers that it
entered the CS normally, and hence executes the $\texttt{exit}_{p}()$
procedure of $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3]$ at Line 1. Otherwise, $p$
knows that it is no longer in the queue of the lock it used and hence doesn’t
execute $\texttt{exit}_{p}()$. At Line 1 $p$ informs other processes that it
is giving up the CS by writing $\perp$ to CSowner. Finally, at Line 1 $p$ sets
$\mbox{Active}_{p}$ to $false$ to complete its attempt.

##  3 Correctness of the algorithm

The proof of correctness is based on the inductive invariant of the algorithm,
which we present in Figure 2. For analysis purposes, we introduce an abstract
variable $status_{p}$ for each process $p$ (only for the proof). $status_{p}$
reflects what section of the protocol $p$ last crashed in (if at all).
Specifically, if $p$ crashes in the try section, CS, or exit section,
$status_{p}$ is set to recover-from-try, recover-from-CS, or recover-from-exit
respectively. When $p$ subsequently executes the recover method to completion,
it attains $good$ status again. When in $good$ status, if $p$ calls the
recover method, $status_{p}$ is set to recover-from-rem.

In Appendix B, we prove this invariant by induction and use it to prove the
the main result for CC machines. Appendix B is composed of several
subsections:

  * •

In Section B.2, we prove the lemmas that establish that the three base locks
are used correctly, i.e., respecting the use pattern.

  * •

In Section B.3, we use the invariant to prove the properties of the algorithm,
i.e., Mutual Exclusion, Starvation Freedom, CSR, Bounded Recovery, and Bounded
Exit.

  * •

In Section B.4, we argue that the RMR complexity of the algorithm is $O(1)$.

  * •

In Appendix C, we provide the full inductive proof of the invariant.

To give a flavor of how we prove the properties using the invariant, we
reproduce the proofs of Mutual Exclusion and Starvation Freedom below. These
proofs of course rely on other lemmas in the appendix, which are appropriately
referenced. Finally, we end the section with the statement of the main theorem
that summarizes the results about the CC algorithm.

Lemma 15 (Mutual Exclusion). At most one process is in the CS in any
configuration of any run.

###### Proof.

Assume for a contradiction that there are two processes $p$ and $q$ in the CS
in the same configuration. Therefore,
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:cs:1}}$ and
$\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:cs:1}}$ in the same configuration. By
Condition 9 we have $\mbox{\sc CSowner}=p$ as well as $\mbox{\sc CSowner}=q$
in the same configuration. Thus CSowner has two different values in the same
configuration, a contradiction. ∎

Lemma 17 (Starvation Freedom). At most one process is in the CS in any
configuration of any run. In every fair run, if a process $p$ executes the try
method and no crash occurs during this execution of the try method, then the
method will eventually complete, leading to $p$ entering the CS.

###### Proof.

Since there are only finitely many crash steps in the run, for the purpose of
the argument take a run and pick the earliest time $\tau$ in the run such that
all the crashes have occurred by $\tau$. We need to show that if a process $p$
invokes $\texttt{try}_{p}()$ at a time $t>\tau$, it is in the CS at some time
$t^{\prime}>t$. From an inspection of the algorithm we note that when the
method $\texttt{try}_{p}()$ returns, it puts $p$ in the CS because every
return statement returns the value IN_CS. Thus, we need to show that process
$p$ doesn’t forever get stuck at Lines 1, 1-1, 1, 1, or 1, which will ensure
that $p$ does return from $\texttt{try}_{p}()$. By Lemmas B.5, B.6, and B.7 we
know that $p$ eventually gets past the Lines 1-1, 1, and 1 respectively. When
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:3}}$, by Condition 11, $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$. If $\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$, by Condition 12, $\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]=true\vee(\exists
q,\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}\wedge\mbox{\sc
S}_{q}=\mbox{\sc S}_{p})$. In either case, $\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]=true$ eventually, which $p$ notices at the wait loop of Line 1 and
goes past the line. Hence, we assume that whenever $p$ executes Lines 1 or 1,
$\mbox{\sc S}_{p}=\mbox{\sc Seq}$, because that is the only other possibility
by Condition 11. Therefore, we will argue next that the starvation freedom
property of $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ is satisfied, which will
imply that $p$ gets past Lines 1 or 1. We know from an inspection of the
algorithm that any process that were to execute the $\texttt{reset}()$ at Line
1, would do so for $\mbox{\sc Lock}[\mbox{\sc Seq}-1]$ or $\mbox{\sc
Lock}[\mbox{\sc Seq}-2]$, because by Condition 11 $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$ for any process $p$ with
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$. It follows that from the last
crash onwards, no process will execute $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{reset}()$, meeting the first condition for starvation freedom
on the base lock. It is straightforward that the second condition for
starvation freedom on the base lock is met. Lemmas B.5, B.6, and B.7 ensure
that the last condition for starvation freedom on the base lock is also met.
Hence we know that $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ satisfies starvation
freedom. Therefore, a process $p$ gets past Lines 1 or 1 by the starvation
freedom property of the base lock. It follows that the claim holds. ∎

|  |  |
---|---|---|---
Definitions :
| $\bullet$ |  $\forall i\in[0,2],\mbox{\sc Lock}[i].\mbox{\sc State}=(\mbox{\sc Lock}[i].\mbox{\sc TrySet},\mbox{\sc Lock}[i].\mbox{\sc CSSet},\mbox{\sc Lock}[i].\mbox{\sc ExitSet})$.
| $\bullet$ |  $\forall i\in[0,2],\mbox{\sc Lock}[i].\mbox{\sc Set}=\mbox{\sc Lock}[i].\mbox{\sc TrySet}\cup\mbox{\sc Lock}[i].\mbox{\sc CSSet}\cup\mbox{\sc Lock}[i].\mbox{\sc ExitSet}$.
Conditions :

  1. 1.

$1\leq\mbox{\sc S}_{p}\leq\mbox{\sc Seq}$

  2. 2.

$\mbox{\sc Lock}[(\mbox{\sc Seq}+1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$
$\wedge$
$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rec:3}},{\bf\ref{ln:fullcrash:rec:4}}\\}$
$\Rightarrow$ $\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\mbox{\sc
State}=(\phi,\phi,\phi))$

  3. 3.

$\mbox{\sc Stop}[\mbox{\sc Seq}\%3]=false$ $\wedge$ $\mbox{\sc
Stop}[(\mbox{\sc Seq}+1)\%3]=false$ $\wedge$
$(\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}\Rightarrow\mbox{\sc
Stop}[(\mbox{\sc S}_{p}-1)\%3]=false)$

  4. 4.

$((\mbox{Active}_{p}=false\vee\mbox{\sc S}_{p}<\mbox{\sc
Seq}\vee\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\})$
$\Rightarrow$ $p\notin\mbox{\sc Lock}[\mbox{\sc Seq}\%3].\mbox{\sc Set})$
$\wedge$ $(\mbox{\sc S}_{p}<\mbox{\sc Seq}-1\Rightarrow p\notin\mbox{\sc
Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc Set})$

  5. 5.

$\forall i\in[0,2]$, $p$ is in at most one of $\mbox{\sc Lock}[i].\mbox{\sc
TrySet}$, $\mbox{\sc Lock}[i].\mbox{\sc CSSet}$, or $\mbox{\sc
Lock}[i].\mbox{\sc ExitSet}$.

  6. 6.

$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:9}}\\}$
$\Rightarrow$ $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc TrySet}$

  7. 7.

$((\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:4}}\wedge\mbox{\sc
Stop}[\mbox{\sc
S}_{p}\%3]=false)\vee\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:5}}\texttt{-}{\bf\ref{ln:fullcrash:try:7}},{\bf\ref{ln:fullcrash:try:10}}\texttt{-}{\bf\ref{ln:fullcrash:try:14}}\\}$
$\vee$
$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:cs:1}},{\bf\ref{ln:fullcrash:exit:1}}\\}\wedge\mbox{\sc
S}_{p}=\mbox{\sc Seq}))$
$\Rightarrow$ $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$

  8. 8.

$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:exit:2}}$ $\Rightarrow$ $p\in\mbox{\sc
Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc ExitSet}$

  9. 9.

$((\mbox{Active}_{p}=false\vee\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:1}}\texttt{-}{\bf\ref{ln:fullcrash:try:12}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:7}}\\})\Rightarrow\mbox{\sc
CSowner}\neq p)$ $\wedge$
$(\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:13}}\Rightarrow\mbox{\sc
CSowner}=\perp)$
$\wedge$
$((\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:14}}\texttt{-}{\bf\ref{ln:fullcrash:exit:3}}\\}\vee\mbox{\em
status}_{p}=\mbox{\em recover-from-cs})\Rightarrow\mbox{\sc CSowner}=p)$

  10. 10.

$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}}\texttt{-}{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:2}}\texttt{-}{\bf\ref{ln:fullcrash:rec:5}}\\}\Rightarrow\mbox{Active}_{p}=true)$
$\wedge$
$(((\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rem:1}},{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:7}}\\}\wedge\mbox{\em
status}_{p}\in\\{\mbox{\em good},\mbox{\em recover-from-
rem}\\})\vee\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:1}},{\bf\ref{ln:fullcrash:rec:8}}\\})\Rightarrow\mbox{Active}_{p}=false)$

  11. 11.

$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:3}}\texttt{-}{\bf\ref{ln:fullcrash:try:7}},{\bf\ref{ln:fullcrash:exit:2}},{\bf\ref{ln:fullcrash:rec:2}}\texttt{-}{\bf\ref{ln:fullcrash:rec:4}}\\}\Rightarrow\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\})$ $\wedge$
$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:8}},{\bf\ref{ln:fullcrash:rec:5}}\\}\Rightarrow\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1)$
$\wedge$
$(\mbox{$PC_{p}$}\in[{\bf\ref{ln:fullcrash:try:9}},{\bf\ref{ln:fullcrash:try:14}}]\Rightarrow\mbox{\sc
S}_{p}=\mbox{\sc Seq})$ $\wedge$
$((\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:6}}\wedge\mbox{\sc
CSowner}=p)\Rightarrow\mbox{\sc S}_{p}<\mbox{\sc Seq})$

  12. 12.

This condition says that if Seq is already incremented, then $\mbox{\sc
Stop}[(\mbox{\sc Seq}-1)\%3]$ is already $true$ or some process is poised to
set it to $true$.
$(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:3}}\texttt{-}{\bf\ref{ln:fullcrash:try:5}}\\}\wedge\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1)$ $\Rightarrow$ $(\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]=true\vee(\exists
q,\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}\wedge\mbox{\sc
S}_{q}=\mbox{\sc S}_{p}))$

  13. 13.

This condition is useful in proving that once Seq is incremented, it will not
be incremented again prior to the next crash. The argument follows from the
fact that once a process is in one of certain states in the run that can only
occur after Seq is incremented, there will be no other process that will
eventually increment Seq once more prior to the next crash.

$((\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:3}}\texttt{-}{\bf\ref{ln:fullcrash:try:6}},{\bf\ref{ln:fullcrash:exit:2}},{\bf\ref{ln:fullcrash:rec:2}}\texttt{-}{\bf\ref{ln:fullcrash:rec:5}}\\}\wedge\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1)$ $\vee$
$(\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:6}}\wedge\mbox{\sc
CSowner}\neq\perp)$ $\vee$
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:7}}\texttt{-}{\bf\ref{ln:fullcrash:try:14}}\\})$
$\Rightarrow$ $\forall
q,(\neg(\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:rem:1}},{\bf\ref{ln:fullcrash:rec:1}}\\}$
$\wedge$ $\mbox{Active}_{q}=true$ $\wedge$ $\mbox{\sc S}_{q}=\mbox{\sc
Seq})\wedge(\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:rec:2}}\texttt{-}{\bf\ref{ln:fullcrash:rec:5}}\\}\Rightarrow\mbox{\sc
S}_{q}=\mbox{\sc Seq}-1))$

  14. 14.

This condition essentially means that there can be at most two working queues
coming out of the three base locks. Moreover, once a process $q$ from an older
queue goes past Line 1, that queue freezes for the remaining run upto the next
crash.

$(\forall
q,(\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:6}},{\bf\ref{ln:fullcrash:try:7}},{\bf\ref{ln:fullcrash:try:12}}\\}\wedge\mbox{\sc
S}_{p}=\mbox{\sc Seq}\wedge\mbox{\sc CSowner}=q)$
$\Rightarrow$ $(\mbox{\sc S}_{q}=\mbox{\sc Seq}-1\wedge q\in\mbox{\sc
Lock}[\mbox{\sc S}_{q}\%3].\mbox{\sc CSSet}$
$\wedge$ $\forall r,(q\neq r\wedge\mbox{\sc S}_{r}=\mbox{\sc S}_{q})$
$\Rightarrow$
$(\mbox{$PC_{r}$}\in\\{{\bf\ref{ln:fullcrash:rem:1}}\texttt{-}{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:8}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:8}}\\}$
$\vee$ $(\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:try:4}}\Rightarrow\mbox{\sc
Stop}[\mbox{\sc S}_{r}\%3]=true)))$
$\wedge$
$(((\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:7}},{\bf\ref{ln:fullcrash:try:12}}\\}\wedge\mbox{\sc
S}_{p}=\mbox{\sc Seq}\wedge\mbox{\sc
CSowner}=\perp)\vee\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:13}},{\bf\ref{ln:fullcrash:try:14}}\\})$
$\Rightarrow$ $(\forall r,(\mbox{\sc S}_{r}\neq\mbox{\sc
Seq}-1\vee\mbox{$PC_{r}$}\in\\{{\bf\ref{ln:fullcrash:rem:1}}\texttt{-}{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:8}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:8}}\\}$
$\vee$ $(\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:try:4}}\Rightarrow\mbox{\sc
Stop}[\mbox{\sc S}_{r}\%3]=true))$
$\wedge$ $\exists q,q\in\mbox{\sc Lock}[(\mbox{\sc Seq}-1)\%3].\mbox{\sc
CSSet}))$

Figure 2: Invariant for the RME algorithm presented in Figure 1. The algorithm
satisfies the conjunction of all the conditions given above in every
configuration of every run.

######  Theorem 3.1.

The algorithm in Figure 1 solves the recoverable mutual exclusion problem on
CC machines for an arbitrary number of processes of arbitrary names. It
satisfies mutual exclusion, starvation freedom, critical section re-entry,
bounded recovery, and bounded exit. The space complexity of the algorithm is
$O(1)$ per process, and the RMR complexity of the algorithm on CC machines is
$O(1)$ per passage.

##  4 Enhancing the algorithm for DSM

The CC algorithm just presented has an unbounded RMR complexity in the DSM
model. In this section, we enhance it to obtain a new algorithm that has
$O(1)$ RMR complexity in both the DSM and CC models. The enhanced algorithm so
closely mirrors the CC algorithm that its correctness follows from that of the
CC algorithm. Below, we describe the main ideas behind how we transform the CC
algorithm into an efficient DSM algorithm (Section 4.1), and then present the
technical details (Sections 4.2 and 4.3).

|  |  |
---|---|---|---
Shared variables (stored in NVM)
|  |  $\mbox{\sc Seq}\in\mathbb{N}$, initially $1$.
|  |  $\mbox{\sc Lock}[0\cdots 2]$ is an array of base mutual exclusion locks, as implemented in Figure 7.
|  |  $\mbox{\sc Stop}[0\cdots 2]$ is an array of boolean signal objects, as implemented in Figure 5, each initially false.
|  |  CSowner is a capturable object, as implemented in Figure 4, initially $\perp$.
|  Persistent variables local to process $p$ (stored in NVM)
|  |  $\mbox{Active}_{p}$ is a boolean, initially false.
|  |  $\mbox{\sc S}_{p}\in\mathbb{N}$, initially $1$.

|  |  |  |
---|---|---|---|---
|  1. |  Remainder Section
|  | procedure $\texttt{try}_{p}()$
| 2. |  $\mbox{Active}_{p}\leftarrow true$
|  3. |  $\mbox{\sc S}_{p}\leftarrow\mbox{\sc Seq}$
|  4. |  $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$
|  5. |  if $\mbox{\sc Seq}\neq\mbox{\sc S}_{p}$: then go to Line 3
|  6. |  $\mbox{\sc CSowner}.\texttt{wait}_{p}(\mbox{\sc S}_{p}\%3)$ $\parallel$ $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3].\texttt{wait}_{p}()$
|  |  $\mbox{\sc CSowner}.\texttt{wait}_{p}(\mbox{\sc S}_{p}\%3)$ $\parallel$ go to Line 3
|  7. |  if $\mbox{\sc CSowner}.\texttt{capture}_{p}()$ then return IN_CS
|  8. |  if $\mbox{\sc Seq}\neq\mbox{\sc S}_{p}$ then
|  9. |  |  $\mbox{\sc S}_{p}\leftarrow\mbox{\sc S}_{p}+1$
|  3.1. |  |  $\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\texttt{exit}_{p}()$
|  10. |  |  $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$
|  11. |  |  $\mbox{\sc CSowner}.\texttt{wait}_{p}(\mbox{\sc S}_{p}\%3)$
|  12. |  |  if $\mbox{\sc CSowner}.\texttt{capture}_{p}()$ then return IN_CS
|  13. |  $\mbox{\sc CSowner}.\texttt{wait}_{p}(\mbox{\sc S}_{p}\%3)$
|  14. |  $\mbox{\sc CSowner}.\texttt{write}_{p}()$
|  15. |  return IN_CS
|  16. |  Critical Section
|  | procedure $\texttt{exit}_{p}()$
|  17. |  $x_{p}\leftarrow\mbox{\sc Seq}$
|  18. |  if $\mbox{\sc S}_{p}=x_{p}$ then $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$
|  3.1. |  if $\mbox{\sc S}_{p}=x_{p}-1$ then $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$
|  19. |  $\mbox{\sc CSowner}.\texttt{release}_{p}()$
|  20. |  $\mbox{Active}_{p}\leftarrow\mbox{\it false}$
|  | procedure $\texttt{recover}_{p}()$
|  21. |  if $\mbox{Active}_{p}\wedge\mbox{\sc Seq}=\mbox{\sc S}_{p}$:
|  22. |  |  $\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\texttt{reset}_{p}()$
|  23. |  |  $\mbox{\sc Stop}[(\mbox{\sc S}_{p}-1)\%3].\texttt{reset}_{p}()$
|  24. |  |  $\mbox{\sc Seq}\leftarrow\mbox{\sc S}_{p}+1$
|  25. |  |  $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3].\texttt{set}_{p}()$
|  3.1. |  if $\mbox{\sc S}_{p}=\mbox{\sc Seq}-1$: then $\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$
|  26. |  if $\mbox{\sc CSowner}.\texttt{read}_{p}()=p$ then return IN_CS
|  27. |  $\mbox{Active}_{p}\leftarrow\mbox{\it false}$
|  28. |  return IN_REM

Figure 3:  Algorithm for an RME lock ${\mathcal{L}}$ for an arbitrary number
of processes of arbitrary names, for DSM machines. Code shown for a process
$p$.

###  4.1 Ideas underlying the DSM algorithm

To achieve $O(1)$ RMR complexity for our RME algorithm in the DSM model, we
need base mutex locks—$\mbox{\sc Lock}[i]$ for $i\in[0,2]$—that have $O(1)$
RMR complexity in the DSM model. We obtain these by using Lee’s second
algorithm in Figure 7, instead of his first algorithm. Beyond this simple
change, we must address the issue that an unbounded number of RMRs are
incurred at each line of the algorithm where a process busy-waits. In the
following, we explain that there are three sources of busy-wait in the
algorithm, and for each source, explain how we propose to bring the RMRs down
to $O(1)$.

  * •

The busy-waiting on CSowner at Lines 6, 11, and 13 of the earlier algorithm
incurs unbounded RMRs on a DSM machine since the variable CSowner must reside
in a memory partition that is remote to all but one process. To overcome this
difficulty, we introduce a new object, which we call a capturable object, that
supports a method for each operation the algorithm performs on CSowner, and
implement each method so that it incurs only $O(1)$ RMRs. More specifically,
the shared variable CSowner of the CC algorithm is replaced by a capturable
object CSowner in our DSM algorithm and the steps “wait till $\mbox{\sc
CSowner}=\perp$” (at Lines 6, 11, and 13), “$\mbox{\sc
CSowner}\leftarrow\perp$” (at Line 19), “read CSowner” (at Line 26),
“$\mbox{\sc CSowner}\leftarrow p$” (at Line 14), and “CAS$(\mbox{\sc
CSowner},\bot,p)$” (at Lines 7 and 12) of the earlier algorithm are replaced,
respectively, by the constant-RMR methods $\mbox{\tt
CSowner}.\texttt{wait}_{p}($), $\mbox{\tt CSowner}.\texttt{release}_{p}($),
$\mbox{\tt CSowner}.\texttt{read}_{p}($), $\mbox{\tt
CSowner}.\texttt{write}_{p}($), and $\mbox{\tt
CSowner}.\texttt{capture}_{p}($), as presented in Figure 3.

  * •

The statement “wait till $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=true$” which
appears at both Line 4 and Line 6, is a source of unbounded RMRs in the DSM
model. Although the wait statement at Line 4 is identical to the wait
statement at Line 6, there is a significant difference between the two. At
Line 6, there can be at most one process busy waiting on $\mbox{\sc
Stop}[\mbox{\sc S}_{p}\%3]$—the winner of $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3]$. In contrast, many processes can be busy waiting at Line 4. We
devise different solutions to reduce the the unbounded RMRs incurred at these
two lines to $O(1)$.

To handle Line 6, we implement a new object, which we call a boolean signal
object, that supports a method for each operation the algorithm performs on
$\mbox{\sc Stop}[i]$, and implement each method so that it incurs only $O(1)$
RMRs. More specifically, the shared variable $\mbox{\sc Stop}[i]$ of the CC
algorithm is replaced by a boolean signal object object $\mbox{\tt Stop}[i]$
in our DSM algorithm and the steps “wait till $\mbox{\sc Stop}[i]=true$” (Line
6), “$\mbox{\sc Stop}[i]\leftarrow true$” (Line 25), and “$\mbox{\sc
Stop}[i]\leftarrow\mbox{\it false}$ (Line 23) of the earlier algorithm are
replaced, respectively, by the constant-RMR methods $\mbox{\tt
Stop}[i].\texttt{wait}_{p}($), $\mbox{\tt Stop}[i].\texttt{set}_{p}($), and
$\mbox{\tt Stop}[i].\texttt{reset}_{p}($), as can be seen by comparing Lines
6, 23, and 25 of Figures 1 and 3.

  * •

At Line 4 of the CC algorithm, $p$ repeatedly reads the $\mbox{\sc
Stop}[S_{p}\%3]$ variable while performing in parallel the Try method on
$\mbox{\sc Lock}[S_{p}\%3]$. This repeated reading is done because, if a
process $q$ installs $\mbox{\sc Lock}[(S_{p}+1)\%3]$ while $p$ is executing
the Try method of $\mbox{\sc Lock}[S_{p}\%3]$, the algorithm needs $p$ to
detect this development and migrate to the newly installed lock. Such a
scenario manifests if events occur in the following order: a crash occurs
while $q$ is in the try method of $\mbox{\sc Lock}[S_{p}\%3]$; when processes
subsequently restart after this crash, $p$ starts executing the algorithm,
reads $S_{p}$ from Seq, and (clueless about the prior crash) executes the try
method of the base lock $\mbox{\sc Lock}[S_{p}\%3]$ (Line 4); $q$ restarts,
executes the recover method, and increments Seq to $S_{p}+1$.

In the above scenario, since the newer base lock, namely $\mbox{\sc
Lock}[(S_{p}+1)\%3]$, has been installed, $p$ and any more such processes that
are stuck at the try section of $\mbox{\sc Lock}[S_{p}\%3]$ should release
themselves and migrate to the try section of $\mbox{\sc Lock}[(S_{p}+1)\%3]$.
To meet this need while expending only $O(1)$ RMRs, we exploit the “Release
Property” of Lee’s lock, which guarantees that no process ever gets stuck in
$\mbox{\sc Lock}[S_{p}\%3]$ so long as all processes—including those that
crash while using the $\mbox{\sc Lock}[S_{p}\%3]$—eventually execute the exit
section of that lock (Theorem A.2 in Appendix A states the Release property
and the paragraph preceding the theorem informally describes the property).
This insight eliminates the need for the “wait until” statement at Line 4
(compare Line 4 of Figure 1 with Line 4 of Figure 3), and adds three lines
(Lines 9.1, 18.1, and 25.1), where a process executes the exit method on an
old lock as it installs or migrates to a new lock.

The above ideas give rise to the DSM algorithm in Figure 3, which has three
additional lines where $\texttt{exit}_{p}$ is called, as just explained, and
every other line corresponds to the same numbered line of the earlier CC
algorithm.

In the next two subsections, we present the specification and the
implementation of the capturable and boolean signal objects, which completes
the description of our DSM algorithm.

###  4.2 Capturable object: Spec and Implementation

A capturable object $\mathcal{C}$ is specified as follows:
$\mathcal{C}.\mbox{\em state}$ is a pid or $\bot$, and $\mathcal{C}$ supports
the following operations.

  * •

$\mathcal{C}.\texttt{read}_{p}($): returns $\mathcal{C}.\mbox{\em state}$.

  * •

$\mathcal{C}.\texttt{write}_{p}($): changes $\mathcal{C}.\mbox{\em state}$ to
$p$.

  * •

$\mathcal{C}.\texttt{release}_{p}($): changes $\mathcal{C}.\mbox{\em state}$
to $\bot$.

  * •

$\mathcal{C}.\texttt{capture}_{p}($): If $\mathcal{C}.\mbox{\em state}=\bot$,
it changes $\mathcal{C}.\mbox{\em state}$ to $p$ and returns true; otherwise,
it returns false, and leaves $\mathcal{C}.\mbox{\em state}$ unchanged.

  * •

$\mathcal{C}.\texttt{wait}_{p}(i\in\\{0,1,2\\})$: this method returns only if
$\mathcal{C}.\mbox{\em state}=\bot$ at some point during the execution of the
method. Thus, it is equivalent to the statement “wait till
$\mathcal{C}.\mbox{\em state}=\bot$”

(The argument $i$ to the wait operation is irrelevant to the semantics of the
operation, but we have introduced it for implementational convenience, as
explained below.)

In the algorithm in Figure 3, there are three lines where a process waits on
CSowner (Lines 6, 11, 13). In all of these lines together, for any
$i\in\\{0,1,2\\}$, at most one process $p$ executes $\mbox{\sc
CSowner}.\texttt{wait}_{p}(i)$ at any given time. So, for our purpose, it
suffices to implement a capturable object that supports one waiting process at
each $i$ (and an arbitrary number of processes that might execute the other
operations).

The simple algorithm in Figure 4 efficiently implements such an object, as
summarized by the following theorem.

|  |
---|---|---
Shared variables (stored in NVM):
|  $X$ holds a process id or $\bot$; initialized to $\bot$.
|  $\text{\sc Go}_{p}$ holds a pair $(\text{\sc Go}_{p}.seq,\text{\sc
Go}_{p}.flag)$, where $\text{\sc Go}_{p}.seq$ is an integer and
|  $\text{\sc Go}_{p}.flag$ is a boolean; $\text{\sc Go}_{p}$ is initialized
arbitrarily.
|  $\text{\sc Go}_{p}$ resides in process $p$’s partition of shared memory.
|  $W[0\cdots 2]$ is an array of pointers. Each pointer is initially $\bot$.

|  |  |  |  |
---|---|---|---|---|---
|  | procedure $\mathcal{C}.\texttt{read}_{p}()$
| 1. |  return $X$
|  | procedure $\mathcal{C}.\texttt{write}_{p}()$
| 2. |  $X\leftarrow p$
|  | procedure $\mathcal{C}.\texttt{capture}_{p}()$
| 3. |  return $\mbox{\bf CAS}(X,\bot,p)$
|  | procedure $\mathcal{C}.\texttt{wait}_{p}(i_{p}\in\\{0,1,2\\})$
| 4. |  $x_{p}\leftarrow\text{\sc Go}_{p}.seq$
| 5. |  $\text{\sc Go}_{p}\leftarrow(x_{p}+1,\mbox{\it false})$
| 6. |  $W[i_{p}]\leftarrow\&\text{\sc Go}_{p}$
| 7. |  if $X=\bot$ return
| 8. |  wait till $\text{\sc Go}_{p}.flag$
|  | procedure $\mathcal{C}.\texttt{release}_{p}()$
| 9. |  $X\leftarrow\bot$
| 10. |  for $i_{p}\in\\{0,1,2\\}$
| 11. |  |  $ptr_{p}\leftarrow W[i_{p}]$
| 12. |  |  if $ptr_{p}\neq\bot$ then
| 13. |  |  |  $(x_{p},b_{p})\leftarrow*ptr_{p}$
| 14. |  |  |  if $\neg b_{p}\wedge(X=\bot)$ then
| 15. |  |  |  |  $\mbox{\bf CAS}(*ptr_{p},(x_{p},\mbox{\it false}),(x_{p},true))$

Figure 4:  Strictly-Linearizable implementation of a capturable object
$\mathcal{C}$ that supports a single process waiting at each
$i\in\\{0,1,2\\}$. Code for process $p$.

######  Theorem 4.1.

For the algorithm in Figure 4, if for each $i\in\\{0,1,2\\}$, no two processes
execute $\mathcal{C}.\texttt{wait}(i)$ concurrently, then:

  * •

$\mathcal{C}$ is strictly linearizable [1], i.e., (1) $\mathcal{C}$ is
linearizable, and (2) if a crash occurs before the operation completes, then
either the operation takes effect before the crash or it will never take
effect.

  * •

The operations $\texttt{read}_{p}($), $\texttt{write}_{p}($),
$\texttt{release}_{p}($), and $\texttt{capture}_{p}($) are wait-free.

  * •

Suppose that no crash occurs since the time a process $p$ invokes
$\mathcal{C}.\texttt{wait}_{p}(i_{p})$, and suppose that
$\mathcal{C}.\mbox{\em state}=\bot$ forever, starting from some arbitrary
point in time. Then, in a fair run, $p$ eventually returns from
$\mathcal{C}.\texttt{wait}_{p}(i_{p})$.

  * •

A process incurs $O(1)$ RMRs to invoke and complete any of the five operations
in both DSM and CC machines.

Proof sketch: The algorithm maintains the key invariant that
$\mathcal{C}.\mbox{\em state}=X$, and linearizes the read, write, capture, and
release operations at Lines 1, 2, 3, and 9, respectively. We linearize a wait
operation only if it returns from the wait method; we observe that if a wait
operation returns, then there is a point in time during the execution of the
wait operation when $X=\bot$, and we linearize the operation at any such time.
Hence, we have Part (1) of the lemma. The other parts follow easily from an
inspection of the code. $\blacksquare$

###  4.3 Signal Object: Spec and Implementation

A boolean signal object $\mathcal{S}$ is specified as follows:
$\mathcal{S}.\mbox{\em state}$ is Boolean, and $\mathcal{S}$ supports the
following three operations.

  * •

$\mathcal{S}.\texttt{set}_{p}($): changes $\mathcal{S}.\mbox{\em state}$ to
true.

  * •

$\mathcal{S}.\texttt{reset}_{p}($): changes $\mathcal{S}.\mbox{\em state}$ to
false

  * •

$\mathcal{S}.\texttt{wait}_{p}($): this method returns only if
$\mathcal{S}.\mbox{\em state}=\mbox{\em true}$ at some point during the
execution of the method. Thus, it is identical to the statement “wait till
$\mathcal{S}.\mbox{\em state}=\mbox{\em true}$”

In the algorithm in Figure 3, for any $i\in\\{0,1,2\\}$, at most one process
$p$ waits on $\mbox{\sc Stop}[i]$ (at Line 6) at any given time. So, for our
purpose, it suffices to implement a boolean signal object that supports only
one waiting process (and an arbitrary number of setting and resetting
processes). The simple algorithm in Figure 5 efficiently implements such an
object, as summarized below:

|  |
---|---|---
Shared variables (stored in NVM):
|  $X$ is a boolean; initialized to false.
|  $\text{\sc Go}_{p}$ holds a boolean; initialized arbitrarily. $\text{\sc
Go}_{p}$ resides in $p$’s partition of memory.
|  $W$ is a pointer; initialized to $\bot$.

|  |  |  |
---|---|---|---|---
|  | procedure $\mathcal{S}.\texttt{wait}_{p}()$
| 1. |  $\text{\sc Go}_{p}\leftarrow\mbox{\it false}$
| 2. |  $W\leftarrow\&\text{\sc Go}_{p}$
| 3. |  if $X$ then return
| 4. |  wait till $\text{\sc Go}_{p}$
|  | procedure $\mathcal{S}.\texttt{set}_{p}()$
| 5. |  $X\leftarrow true$
| 6. |  $ptr_{p}\leftarrow W$
| 7. |  if $ptr_{p}\neq\bot$ then
| 8. |  |  $*ptr_{p}\leftarrow true$
|  | procedure $\mathcal{S}.\texttt{reset}_{p}()$
| 9. |  $X\leftarrow\mbox{\it false}$

Figure 5:  Strictly-Linearizable implementation of a boolean signal object
$\mathcal{S}$ that supports a single waiting process. Code for process $p$.

######  Theorem 4.2.

For the algorithm in Figure 5, if no two processes execute
$\mathcal{S}.\texttt{wait}()$ concurrently, then:

  * •

$\mathcal{S}$ is strictly linearizable.

  * •

The operations $\texttt{set}_{p}($) and $\texttt{reset}_{p}()$ are wait-free.

  * •

Suppose that no crash occurs since the time a process $p$ invokes
$\mathcal{S}.\texttt{wait}_{p}($), and suppose that $\mathcal{S}.\mbox{\em
state}=true$ forever, starting from some arbitrary point in time. Then, in a
fair run, $p$ eventually returns from $\mathcal{S}.\texttt{wait}_{p}($).

  * •

A process incurs $O(1)$ RMRs to invoke and complete any of the three
operations in both DSM and CC machines.

Proof sketch: The algorithm maintains the key invariant that
$\mathcal{S}.\mbox{\em state}=X$, and linearizes the set and reset operations
at Lines 5 and 9, respectively. We linearize a wait operation only if it
returns from the wait method; we observe that if a wait operation returns,
then there is a point in time during the execution of the wait operation when
$X=true$, and we linearize the operation at any such time. Hence, we have Part
(1) of the lemma. The other parts follow easily from an inspection of the
code. $\blacksquare$

###  4.4 The final result

The theorem below summarizes the results of this paper.

######  Theorem 4.3.

The algorithm in Figure 3 solves the recoverable mutual exclusion problem on
DSM and CC machines for an arbitrary number of processes of arbitrary names.
It satisfies mutual exclusion, bounded exit, bounded critical section reentry,
and starvation freedom. The space complexity of the algorithm is $O(1)$ per
process, and the RMR complexity of the algorithm on DSM and CC machines is
$O(1)$ per passage.

Proof: Since the algorithm in Figure 3 has the same invariant as that in
Figure 1, the proofs of the properties are accordingly the same. $\square$

##  5 Conclusion

For the system-wide crashes, we have designed the first RME algorithm with
$O(1)$ worst-case RMR complexity for both the CC and DSM models. Our algorithm
allows access to threads created dynamically, on-the-fly, and requires only
$O(1)$ space per thread.

For the RME problem, the worst-case RMR complexity in the individual crash
model for both CC and DSM machines (using realistic primitives) was settled to
be $\Theta(\log n/\log\log n)$ by the upper bounds due to Jayanti et al. and
Golab and Hendler [20, 14] and the matching lower bounds due to Chan and
Woelfel [6]. This paper resolves the worst-case RMR complexity in the system-
wide crash model to be $\Theta(1)$, thereby formalizing our intuition that
individual crashes can be more expensive to cope with than system-wide
crashes.

We close with two open problems:

  1. 1.

The algorithms in this paper use an unbounded sequence number. This is not a
practical concern on modern 64-bit architectures, since it would take 500,000
years for the counter to overflow even at a rate of a million system-wide
crashes per second. Nevertheless, from a theoretical stand point, it would be
interesting to investigate whether we can do away with such variables.

  2. 2.

Our algorithms do not satisfy the first-come-first-served (FCFS) property, but
they satisfy the following weaker property: if an infinite run has only a
finite number of crashes, then FCFS will hold for an infinite suffix of the
run. Designing an FCFS algorithm without sacrificing on the other metrics is a
tantalizing open problem.

## References

  * [1] Aguilera, M. K., and Frølund, S. Strict linearizability and the power of aborting.  Tech. Rep. HPL-2003-241, Hewlett-Packard Labs, 2003.
  * [2] Attiya, H., Ben-Baruch, O., and Hendler, D. Nesting-safe recoverable linearizability: Modular constructions for non-volatile memory.  In PODC (2018), C. Newport and I. Keidar, Eds., ACM, pp. 7–16.
  * [3] Attiya, H., Ben-Baruch, O., and Hendler, D. Nesting-safe recoverable linearizability: Modular constructions for non-volatile memory.  In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2018), PODC ’18, Association for Computing Machinery, p. 7–16.
  * [4] Ben-David, N., Blelloch, G. E., Friedman, M., and Wei, Y. Delay-free concurrency on faulty persistent memory.  In The 31st ACM Symposium on Parallelism in Algorithms and Architectures (New York, NY, USA, 2019), SPAA ’19, Association for Computing Machinery, p. 253–264.
  * [5] Chan, D. Y. C., and Woelfel, P. Recoverable mutual exclusion with constant amortized RMR complexity from standard primitives.  In PODC ’20: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, August 3-7, 2020 (2020), Y. Emek and C. Cachin, Eds., ACM, pp. 181–190.
  * [6] Chan, D. Y. C., and Woelfel, P. Tight lower bound for the RMR complexity of recoverable mutual exclusion.  533–543.
  * [7] Coburn, J., Caulfield, A. M., Akel, A., Grupp, L. M., Gupta, R. K., Jhala, R., and Swanson, S. Nv-heaps: Making persistent objects fast and safe with next-generation, non-volatile memories.  Association for Computing Machinery.
  * [8] Coburn, J., Caulfield, A. M., Akel, A., Grupp, L. M., Gupta, R. K., Jhala, R., and Swanson, S. Nv-heaps: Making persistent objects fast and safe with next-generation, non-volatile memories.  SIGARCH Comput. Archit. News 39, 1 (mar 2011), 105–118.
  * [9] Condit, J., Nightingale, E. B., Frost, C., Ipek, E., Lee, B. C., Burger, D., and Coetzee, D. Better I/O through byte-addressable, persistent memory.  In Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009 (2009), J. N. Matthews and T. E. Anderson, Eds., ACM, pp. 133–146.
  * [10] Dhoked, S., and Mittal, N. An adaptive approach to recoverable mutual exclusion.  In PODC ’20: ACM Symposium on Principles of Distributed Computing, Virtual Event, Italy, August 3-7, 2020 (2020), Y. Emek and C. Cachin, Eds., ACM, pp. 1–10.
  * [11] Dijkstra, E. W. Solution of a Problem in Concurrent Programming Control.  Commun. ACM 8, 9 (Sept. 1965), 569–.
  * [12] Friedman, M., Herlihy, M., Marathe, V. J., and Petrank, E. A persistent lock-free queue for non-volatile memory.  In Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2018, Vienna, Austria, February 24-28, 2018 (2018), A. Krall and T. R. Gross, Eds., ACM, pp. 28–40.
  * [13] Friedman, M., Petrank, E., and Ramalhete, P. Mirror: Making Lock-Free Data Structures Persistent.  Association for Computing Machinery, New York, NY, USA, 2021, p. 1218–1232.
  * [14] Golab, W., and Hendler, D. Recoverable mutual exclusion in sub-logarithmic time.  In Proceedings of the ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2017), PODC ’17, ACM, pp. 211–220.
  * [15] Golab, W., and Hendler, D. Recoverable Mutual Exclusion Under System-Wide Failures.  In Proceedings of the 2018 ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2018), PODC ’18, ACM, pp. 17–26.
  * [16] Golab, W., and Ramaraju, A. Recoverable Mutual Exclusion: [Extended Abstract].  In Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2016), PODC ’16, ACM, pp. 65–74.
  * [17] Izraelevitz, J., Mendes, H., and Scott, M. L. Linearizability of persistent memory objects under a full-system-crash failure model.  In Distributed Computing - 30th International Symposium, DISC 2016, Paris, France, September 27-29, 2016. Proceedings (2016), C. Gavoille and D. Ilcinkas, Eds., vol. 9888 of Lecture Notes in Computer Science, Springer, pp. 313–327.
  * [18] Jayanti, P., and Jayanti, S. Deterministic constant-amortized-rmr abortable mutex for CC and DSM.  ACM Trans. Parallel Comput. 8, 4 (2021), 22:1–22:26.
  * [19] Jayanti, P., Jayanti, S., and Joshi, A. Optimal Recoverable Mutual Exclusion using only FASAS.  In The 6th Edition of The International Conference on Networked Systems (2018), NETYS 2018, Springer, Cham.
  * [20] Jayanti, P., Jayanti, S., and Joshi, A. A recoverable mutex algorithm with sub-logarithmic rmr on both cc and dsm.  In Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2019), PODC ’19, Association for Computing Machinery, p. 177–186.
  * [21] Jayanti, P., and Joshi, A. Recoverable FCFS mutual exclusion with wait-free recovery.  In 31st International Symposium on Distributed Computing (2017), DISC 2017, pp. 30:1–30:15.
  * [22] Jayanti, P., and Joshi, A. Recoverable mutual exclusion with abortability.  In Networked Systems (Cham, 2019), M. F. Atig and A. A. Schwarzmann, Eds., Springer International Publishing, pp. 217–232.
  * [23] Katzan, D., and Morrison, A. Recoverable, abortable, and adaptive mutual exclusion with sublogarithmic RMR complexity.  In 24th International Conference on Principles of Distributed Systems, OPODIS 2020, December 14-16, 2020, Strasbourg, France (Virtual Conference) (2020), Q. Bramas, R. Oshman, and P. Romano, Eds., vol. 184 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 15:1–15:16.
  * [24] Kolli, A., Pelley, S., Saidi, A., Chen, P. M., and Wenisch, T. F. High-performance transactions for persistent memories.  In Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems (New York, NY, USA, 2016), ASPLOS ’16, Association for Computing Machinery, p. 399–411.
  * [25] Lamport, L. A New Solution of Dijkstra’s Concurrent Programming Problem.  Commun. ACM 17, 8 (Aug. 1974), 453–455.
  * [26] Lee, H. Local-spin mutual exclusion algorithms on the DSM model using fetch-&-store objects.  Master’s thesis, University of Toronto, 2003.
  * [27] Li, N., and Golab, W. Brief announcement: Detectable sequential specifications for recoverable shared objects.  In Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing (New York, NY, USA, 2021), PODC’21, Association for Computing Machinery, p. 557–560.
  * [28] Ramaraju, A. RGLock: Recoverable mutual exclusion for non-volatile main memory systems.  Master’s thesis, University of Waterloo, 2015.
  * [29] Raoux, S., Burr, G. W., Breitwisch, M. J., Rettner, C. T., Chen, Y.-C., Shelby, R. M., Salinga, M., Krebs, D., Chen, S.-H., Lung, H.-L., et al. Phase-change random access memory: A scalable technology.  IBM Journal of Research and Development 52, 4/5 (2008), 465.
  * [30] Strukov, D. B., Snider, G. S., Stewart, D. R., and Williams, R. S. The missing memristor found.  nature 453, 7191 (2008), 80.
  * [31] Tehrani, S., Slaughter, J. M., Deherrera, M., Engel, B. N., Rizzo, N. D., Salter, J., Durlam, M., Dave, R. W., Janesky, J., Butcher, B., et al. Magnetoresistive random access memory using magnetic tunnel junctions.  Proceedings of the IEEE 91, 5 (2003), 703–714.

##  Appendix A Lee’s Standard (Non-Recoverable) Mutual Exclusion Locks with
Atomic Reset

We present two well known, standard (non-recoverable) queue locks due to Lee
[26] with an atomic reset method. The first lock, presented in Figure 6, has
$O(1)$ RMR complexity in the CC model, and is used for the three base locks of
our RME lock of Section 2. The second one, in Figure 7, has $O(1)$ RMR
complexity in both CC and DSM models, and is used for the three base locks of
our RME lock of Section 4.

We capture the status of a lock $\ell$ by four sets—$\ell.\mbox{\sc TrySet}$,
$\ell.\mbox{\sc CSSet}$, $\ell.\mbox{\sc ExitSet}$, and $\ell.\mbox{\sc
CrashSet}$. The first three are the set of processes in $\ell$’s try section,
CS, and exit section, respectively. When a system-wide crash occurs, the
processes in these sets are moved to $\ell.\mbox{\sc CrashSet}$ (and the other
three sets become empty). Thus, $\ell.\mbox{\sc CrashSet}$ consists of those
processes that were using the lock when a crash occurred. When atomic reset is
performed on $\ell$, all four sets are set to $\emptyset$, reflecting that
$\ell$ is once more ready for use as a fresh mutex lock; furthermore, reset
can be performed at any time.

The use-pattern states the obvious: a process $p$ may enter $\ell.\mbox{\sc
TrySet}$ only when it is not in any of the four sets; when $p$ leaves
$\ell.\mbox{\sc TrySet}$ (upon completing the try section), it gets into
$\ell.\mbox{\sc CSSet}$; when $p$ leaves $\ell.\mbox{\sc CSSet}$, it gets into
$\ell.\mbox{\sc ExitSet}$; and when $p$ leaves $\ell.\mbox{\sc ExitSet}$, it
is out of all sets. Furthermore, $p$ may execute a step of the try, CS, or
exit section only if it is in $\ell.\mbox{\sc TrySet}$, $\ell.\mbox{\sc
CSSet}$, or $\ell.\mbox{\sc ExitSet}$, respectively.

The properties of Lee’s locks are summarized as follows.

######  Theorem A.1.

Lee’s locks in Figures 6 and 7 satisfy the following properties, assuming that
processes respect the use-pattern stated above:

  * •

Mutual Exclusion: $|\ell.\mbox{\sc CSSet}|\leq 1$

  * •

Starvation Freedom: In every fair run, if a process $p$ executes
$\ell.\mbox{\em try}_{p}()$ and $\ell.\mbox{\sc CrashSet}$ is empty during the
entire interval of this execution of the try method, then the method will
eventually complete, leading to $p$ entering the CS.

  * •

Bounded Exit: If a process $p$ executes $\ell.\mbox{\em exit}_{p}()$ without
crashing, $p$ returns from the method in a constant number of its own steps..

  * •

Atomic Reset: $\ell.\mbox{\sc Reset}_{p}()$ is atomic and returns $\ell$ to
its initial state.

  * •

RMR and space complexity: The lock in Figure 6 has $O(1)$ RMR complexity in
the CC model, the lock in Figure 7 has $O(1)$ RMR complexity in both CC and
DSM models, and both locks have $O(1)$ space complexity per process.

Lee’s algorithms have an additional property [18], which is explained as
follows. Suppose that a set $A$ of processes were using a lock $\ell$ when a
system-wide crash occurred. When processes subsequently restart, suppose that
a set $B$ of processes (with $B$ disjoint from $A$) invoke the try method.
Because processes in $B$ queue up behind those in $A$ that lost their state
(due to the earlier crash), processes in $B$ could get stuck in the try
section forever. However, if all processes in $A$, when they restart, execute
the exit section, some process in $B$ (informally, the first in the queue
among the ones in $B$) will complete and return from its try section;
furthermore, if each process in $B$, upon returning from the try section,
executes the exit section, then all processes in $A$, one after the other,
return from the try section. The crashed processes in $A$, by executing the
exit section while in $\ell.\mbox{\sc CrashSet}$, violate the use-pattern.
Hence, Mutual Exclusion can be potentially violated, but the feature that none
in $B$ gets stuck is useful when designing our RME algorithm for the DSM
model. The following theorem summarizes the property explained so far.

######  Theorem A.2 (Release Property).

Let $\ell$ be a Lee’s lock from Figure 6 or 7. Suppose that $\ell.\mbox{\sc
CrashSet}=A\neq\emptyset$ and $\ell.\mbox{\sc TrySet}\neq\emptyset$. If each
process in $A$ executes the exit section and each process in $\ell.\mbox{\sc
TrySet}$, if and when it leaves $\ell.\mbox{\sc TrySet}$, executes the exit
section, then every process in $\ell.\mbox{\sc TrySet}$ eventually leaves
$\ell.\mbox{\sc TrySet}$.

|  |  |
---|---|---|---
Shared variable (stored in NVM):
|  |  Tail is a pointer to a location that contains a boolean or $\bot$; Tail is initialized to $\bot$.
|  Persistent Variables local to process $p$ (stored in NVM):
|  |  $\mbox{Node}_{p}[0],\mbox{Node}_{p}[1]$ are pointers to booleans which are initialized arbitrarily.
|  |  $\text{Face}_{p}\in\\{0,1\\}$, initialized arbitrarily.

|  |  |
---|---|---|---
|  | procedure $\ell.\texttt{try}_{p}()$
|  10. |  $\text{Face}_{p}=1-\text{Face}_{p}$
|  11. |  $*\mbox{Node}_{p}[\text{Face}_{p}]\leftarrow\mbox{\it false}$
|  12. |  $prev_{p}\leftarrow\mbox{\bf FAS}(\mbox{\sc Tail},\mbox{Node}_{p}[\text{Face}_{p}])$
|  13. |  if $prev_{p}\neq\bot$ then wait till $*prev_{p}=true$
|  | procedure $\ell.\texttt{exit}_{p}()$
|  14. |  $*\mbox{Node}_{p}[\text{Face}_{p}]\leftarrow true$
|  | procedure $\ell.\texttt{reset}_{p}()$
|  15. |  $\mbox{\sc Tail}\leftarrow\bot$

Figure 6:  Lee’s lock for CC machines [26], with a line added for Reset. Code
shown for a process $p$.

|  |  |
---|---|---|---
Shared variable (stored in NVM):
|  |  Tail is a pointer to a location that contains a pointer or $\bot$; Tail is initialized to $\bot$.
|  Persistent Variables local to process $p$ (stored in NVM):
|  |  $\mbox{Node}_{p}[0],\mbox{Node}_{p}[1]$ are pointers to memory-words which are initialized arbitrarily.
|  |  $\text{Face}_{p}\in\\{0,1\\}$, initialized arbitrarily.

|  |  |  |
---|---|---|---|---
|  | procedure $\ell.\texttt{try}_{p}()$
|  1. |  $\text{Face}_{p}=1-\text{Face}_{p}$
|  2. |  $*\mbox{Node}_{p}[\text{Face}_{p}]\leftarrow\bot$
|  3. |  $prev_{p}\leftarrow\mbox{\bf FAS}(\mbox{\sc Tail},\mbox{Node}_{p}[\text{Face}_{p}])$
|  4. |  if $prev_{p}\neq\bot$ then
|  5. |  |  $\text{\sc Go}_{p}\leftarrow\mbox{\it false}$
|  6. |  |  if $\mbox{\bf FAS}(*prev_{p},\&\text{\sc Go}_{p})=\texttt{token}$ then return
|  7. |  |  wait till $\text{\sc Go}_{p}$
|  | procedure $\ell.\texttt{exit}_{p}()$
|  8. |  $ptr_{p}\leftarrow\mbox{\bf FAS}(*\mbox{Node}_{p}[\text{Face}_{p}],\texttt{token})$
|  9. |  if $ptr_{p}\neq\bot$ then $*ptr_{p}\leftarrow true$
|  | procedure $\ell.\texttt{reset}_{p}()$
|  10. |  $\mbox{\sc Tail}\leftarrow\bot$

Figure 7:  Lee’s queue lock for CC and DSM machines [26], with a line added
for Reset. Code shown for a process $p$.

##  Appendix B Correctness of the algorithm

We prove the correctness of the algorithm by first presenting the invariant
satisfied by the algorithm in Section B.1 and then use the invariant to prove
correctness the correctness of the algorithm in Section B.3.

###  B.1 Invariant of the algorithm

The invariant of the algorithm appears in Figure 2.

###  B.2 Proofs required by the base lock

In this section we prove certain lemmas that prove that our RME algorithm
invokes the base lock as it is required by the lock. This ensures that the
base locks behave in the way they are expected to. Lemmas B.1-B.2 argue that
the main algorithm follows the rules of transition as expected by the base
lock. Lemmas B.5-B.7 are important to argue that the pre-condition for
starvation freedom on the base lock holds. That is, no process stays in the CS
forever: if any process $q$ is in ${\ell}.\mbox{\sc CSSet}$ at any time
$t^{\prime}>t$, $q$ is in ${\ell}.\mbox{\sc ExitSet}$ after $t^{\prime}$. To
see that, we observe from the algorithm that a process could loop only at
certain places throughout the run. When a process $p$ is at Line 1 or 1, we
know that $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc TrySet}$.
However, it could be the case that $p\in\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3].\mbox{\sc CSSet}$ when
$\mbox{$PC_{p}$}\in[{\bf\ref{ln:fullcrash:try:4}},{\bf\ref{ln:fullcrash:try:5}}]$,
or certainly that $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$
when
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:10}},{\bf\ref{ln:fullcrash:try:12}}\\}$.
While a process is resetting a lock $\ell$, no other process performs a step
of the $\ell.\texttt{try}()$ or $\ell.\texttt{exit}()$ methods of that lock.
More precisely, for each lock $\ell$ and each process $q$, if, for a process
$p$, $PC_{p}$ points to a step of ${\ell}.\texttt{reset}_{p}()$, then $PC_{q}$
does not point to a step in ${\ell}.\texttt{try}_{q}()$ or
${\ell}.\texttt{exit}_{q}()$. This is exactly what Lemma B.8 argues about.
Lemma B.8 below essentially implies that once a process $p$ finishes the
execution of $\ell.\texttt{reset}_{p}()$, for any base lock $\ell$, any
process $q$, whether $q=p$ or not, goes back to the pattern of executing the
$\ell.\texttt{try}_{q}()$, CS, and $\ell.\texttt{exit}_{q}()$ methods,
beginning with the invocation of $\ell.\texttt{try}_{q}()$. This follows from
the fact that $\ell.\texttt{reset}_{p}()$ will reset the lock changing
$\ell.\mbox{\sc TrySet}$, $\ell.\mbox{\sc CSSet}$, and $\ell.\mbox{\sc
ExitSet}$ to empty sets, and By Lemmas B.1-B.2 we know that the main algorithm
honors the transitions required by the base lock.

######  Lemma B.1.

A process $p$ may invoke $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{try}_{p}()$ only if $p$ is not in any of the three sets.

###### Proof.

A process $p$ may invoke $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{try}_{p}()$ either from Line 1 or 1. By Condition 4, when
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:2}}$, $p\notin\mbox{\sc
Lock}[\mbox{\sc Seq}\%3].\mbox{\sc Set}$, and we have the claim. When
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:8}}$, by Condition 11, $\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$, and thus, by Condition 4 again we have the claim. ∎

######  Lemma B.2.

A process $p$ may invoke $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{exit}_{p}()$ only if $p$ is in $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\mbox{\sc CSSet}$.

###### Proof.

A process $p$ may invoke $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{exit}_{p}()$ at Line 1. This could happen only if $\mbox{\sc
S}_{p}=\mbox{\sc Seq}$ when $p$ takes a step at Line 1. In that case, by
Condition 7, $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$,
which implies that the claim holds when $p$ invokes $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{exit}_{p}()$. ∎

######  Lemma B.3.

There is a constant $c$ such that, if a crash occurs while a process $p$ is in
the CS (i.e., when $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:cs:1}}$), then $p$
reenters the CS before it executes $c$ of its steps that have no intervening
crash steps.

###### Proof.

If a crash occurs while a process $p$ is in the CS, in the configuration
immediately after the crash, $\mbox{\em status}_{p}=\mbox{\em recover-from-
cs}$ and $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rem:1}}$. It also holds that
$\mbox{\sc CSowner}=p$ in the configuration after the crash since it had that
value prior to the crash by Condition 9 and the crash doesn’t change the value
of CSowner. We know from the description of the control flow that
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:1}}$ eventually. We note that once
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:1}}$, $PC_{p}$ changes to 1 in a
constant number of $p$’s own normal steps, this follows from an inspection of
the algorithm and since there are no loops between the execution path from
Line 1 to Line 1.

We now argue by contradiction that CSowner retains the value $p$ from the
configuration immediately after $p$’s crash in CS upto the configuration prior
to $p$ executing Line 1. Thus, assume for a contradiction that CSowner is
changed from $p$ to some other value after $p$’s crash in the CS but before
$p$ ever executes Line 1. Let process $r$ be the earliest such process in the
run to change the value of CSowner from $p$ to some other value. The value of
CSowner is changed only in the $\texttt{try}()$ and $\texttt{exit}()$ method
and since $p$ is either at Line 1 or the $\texttt{recover}_{p}()$ method,
$p\neq r$. We note that if $r$ changed it due to the CAS operation at Lines 1
or 1, $\mbox{\sc CSowner}=\perp$ in the configuration prior to $r$’s step, and
hence $r$ is not the earliest process to change the value of CSowner from $p$
to some other value. Similarly, if $r$ were to execute Line 1, by Condition 9,
$\mbox{\sc CSowner}=\perp$ when
$\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:try:13}}$, and hence $r$ is not the
earliest process to change the value of CSowner from $p$ to some other value.
Thus, by an inspection of the algorithm we see that CSowner could change only
to $\perp$ due to execution of Line 1 by $r$. Let $C$ be the configuration
when $\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:exit:3}}$. We know that in $C$
$\mbox{\sc CSowner}=p$. Since $\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:exit:3}}$
in $C$, it follows from Condition 9 that $\mbox{\sc CSowner}=r$ in $C$.
Therefore, CSowner has two different values in $C$, a contradiction. It
follows from the above that CSowner retains the value $p$ from the
configuration immediately after $p$’s crash in CS upto the configuration prior
to $p$ executing Line 1.

From the above it follows that if a crash occurs while a process $p$ is in the
CS (i.e., when $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:cs:1}}$), then $p$
reenters the CS before it executes $c$ of its steps that have no intervening
crash steps ∎

######  Lemma B.4.

Assume a fair run in which $\mbox{\sc CSowner}=p$ at time $t$, $\mbox{\sc
CSowner}=\perp$ at time $t^{\prime}>t$ in that run.

###### Proof.

Suppose we have a fair run in which $\mbox{\sc CSowner}=p$ at time $t$. By
Condition 9, $\mbox{Active}_{p}=true$ and
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:14}}\texttt{-}{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:6}}\\}$
or, together with Condition 9 and 10,
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rem:1}}$ and $\mbox{\em
status}_{p}\notin\\{\mbox{\em good},\mbox{\em recover-from-rem}\\}$. If
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rem:1}}$ and $\mbox{\em
status}_{p}\notin\\{\mbox{\em good},\mbox{\em recover-from-rem}\\}$, we know
from the description of the control flow that
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:1}}$ eventually. From an inspection
of the algorithm, it follows that $p$ eventually executes Line 1 in either of
the cases when $\mbox{Active}_{p}=true$ and
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:6}}\\}$,
or $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rem:1}}$ and $\mbox{\em
status}_{p}\notin\\{\mbox{\em good},\mbox{\em recover-from-rem}\\}$. By the
argument similar to one given for Lemma B.3, it follows that CSowner retains
the value $p$ upto the point where it executes Line 1 and re-enters the CS and
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:cs:1}}$ eventually. Once
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:14}}\texttt{-}{\bf\ref{ln:fullcrash:exit:3}}\\}$
it is straightforward to see that $p$ sets CSowner to $\perp$ at Line 1 at a
later point in time, satisfying the claim. ∎

######  Lemma B.5.

If $p$ is at Lines 1-1 at time $t$, $p$ is at a different line at some time
$t^{\prime}>t$.

###### Proof.

Suppose $p$ is at Lines 1-1. By Condition 11, $\mbox{\sc S}_{p}\in\\{\mbox{\sc
Seq}-1,\mbox{\sc Seq}\\}$. We argue each of the cases as follows:

  * Case 1

Suppose $\mbox{\sc S}_{p}=\mbox{\sc Seq}-1$. By Condition 12, $\mbox{\sc
Stop}[\mbox{\sc S}_{p}\%3]=true\vee(\exists
q,\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}\wedge\mbox{\sc
S}_{q}=\mbox{\sc S}_{p})$ If $\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=true$, $p$
notices that the next time it executes Line 1 and comes out of the loop.
Otherwise, we have $\exists
q,\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}\wedge\mbox{\sc
S}_{q}=\mbox{\sc S}_{p}$. At Line 1 $q$ sets $\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]$ to $true$, which $p$ notices the next time it executes Line 1 and
hence comes out of the loop.

  * Case 2

Suppose $\mbox{\sc S}_{p}=\mbox{\sc Seq}$. Let’s assume for the sake of the
argument that there is no crash in the run after
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:4}}$ for the first time in the
current passage and $\mbox{\sc Seq}=\mbox{\sc S}_{p}$ forever, because
otherwise $p$ is at a different line due to one of the above cases and the
claim holds trivially. We note that by Condition 3 $\mbox{\sc Stop}[\mbox{\sc
Seq}\%3]$ will remain $false$ forever, which prevents $p$ from getting out of
the loop at Line 1.

If $\mbox{\sc CSowner}=\perp$ and $p$ notices that the next time it executes
Line 1, $p$ comes out of the loop. Otherwise, assume $\mbox{\sc CSowner}=q$.
By the contrapositive of the first part of Condition 9 it follows that $q\neq
p$. By Lemma B.4 CSowner changes to $\perp$ at a later point. If $p$ notices
that $\mbox{\sc CSowner}=\perp$ at Line 1, we have the claim. Otherwise, we
argue as follows that CSowner could assume the value $r\neq\perp$ at most once
after changing to $\perp$ as above, and then would become $\perp$ again when
$p$ finally notices it. Thus, assume that CSowner changes to the value
$r\neq\perp$ right after becoming $\perp$ as above but before $p$ notices it
at Line 1. We note that this value of $r$ could only be written into CSowner
by $r$ itself at Lines 1, 1, or 1. Thus, $r\neq p$, otherwise $p$ already left
the loop and we have the claim. We first note that the change to CSowner could
not happen at Lines 1 or 1. This is because, by Condition 7 and 11, at Lines 1
and 1 $\mbox{\sc S}_{r}=\mbox{\sc Seq}$ and $r\in\mbox{\sc Lock}[\mbox{\sc
S}_{r}\%3].\mbox{\sc CSSet}$. Because
$\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:4}}\texttt{-}{\bf\ref{ln:fullcrash:try:5}}\\}$
and $\mbox{\sc S}_{p}=\mbox{\sc Seq}$ (which implies $\mbox{\sc
Stop}[\mbox{\sc S}_{p}\%3]=false$ by Condition 3) we already have
$p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$ from Condition 7.
Hence, the mutual exclusion property of $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$
implies that $r$ cannot be in $\mbox{\sc Lock}[\mbox{\sc S}_{r}\%3].\mbox{\sc
CSSet}$ at the same time with $\mbox{\sc S}_{r}=\mbox{\sc Seq}$. It follows
that the value $r$ is written into CSowner at Line 1 only. By Condition 11 and
the same argument as above, it follows that $\mbox{\sc S}_{r}=\mbox{\sc
Seq}-1$, and by Condition 7, $r\in\mbox{\sc Lock}[\mbox{\sc
S}_{r}\%3].\mbox{\sc CSSet}$ when $r$ writes its own name into CSowner at Line
1. Once $r$ CASes the value $r$ into CSowner at Line 1, it moves to the CS,
completes the CS operation and invokes $\texttt{exit}_{r}()$. At Line 1 $r$
finds that $\mbox{\sc S}_{r}=\mbox{\sc Seq}-1\neq\mbox{\sc Seq}$ and hence it
doesn’t invoke $\mbox{\sc Lock}[\mbox{\sc S}_{r}\%3].\texttt{exit}_{r}()$ at
Line 1 ever. Thereby, $r$ remains in $\mbox{\sc Lock}[\mbox{\sc
S}_{r}\%3].\mbox{\sc CSSet}$ forever and by the mutual exclusion property of
the base lock $\mbox{\sc Lock}[\mbox{\sc S}_{r}\%3]$, no other process comes
to execute Line 1 later. Thus, once $r$ writes $\perp$ into CSowner at Line 1,
there is no other process to write its own name into CSowner at Lines 1, 1, or
1. Thus, $p$ notices at Line 1 that $\mbox{\sc CSowner}=\perp$ and comes out
of the loop.

We note that from the above two cases, the claim holds. ∎

######  Lemma B.6.

If $p$ is at Line 1 at time $t$, $p$ is at a different line at some time
$t^{\prime}>t$.

###### Proof.

We first note that $\mbox{\sc S}_{p}=\mbox{\sc Seq}$ when
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:10}}$ by Condition 11. The claim
holds by the same argument as given in Case 2 of the proof of Lemma B.5 above.
∎

######  Lemma B.7.

If $p$ is at Line 1 at time $t$, $p$ is at a different line at some time
$t^{\prime}>t$.

###### Proof.

Suppose $p$ is at Line 1 at time $t$. We note that $\mbox{\sc S}_{p}=\mbox{\sc
Seq}$ when $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:12}}$ by Condition 11.
If $\mbox{\sc CSowner}=q\neq\perp$, by Condition 9, $q\neq p$. By Lemma B.4 we
have that $\mbox{\sc CSowner}=\perp$ at a later time $t^{\prime}$. Thus,
assume $\mbox{\sc CSowner}=\perp$, by Condition 14, we get $\forall
r,(\mbox{\sc S}_{r}\neq\mbox{\sc
Seq}-1\vee\mbox{$PC_{r}$}\in\\{{\bf\ref{ln:fullcrash:rem:1}}\texttt{-}{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:8}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:1}}\texttt{-}{\bf\ref{ln:fullcrash:rec:8}}\\}$
$\vee$ $(\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:try:4}}\Rightarrow\mbox{\sc
Stop}[\mbox{\sc S}_{r}\%3]=true))$. This implies that there is no process $r$
with $\mbox{\sc S}_{r}=\mbox{\sc Seq}-1$ and
$\mbox{$PC_{r}$}={\bf\ref{ln:fullcrash:try:6}}$ once $\mbox{\sc
CSowner}=\perp$. Since $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:12}}$, by
Condition 7, $p\in\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$.
Since $\mbox{\sc S}_{p}=\mbox{\sc Seq}$, by Condition 7 again, there is no
process $q$ with $\mbox{\sc S}_{q}=\mbox{\sc Seq}$ and $PC_{q}$ to be 1, 1, or
1. Thus CSowner doesn’t change from $\perp$ to some other value once $p$ is at
Line 1 and so long as $p$ doesn’t notice CSowner to be $\perp$. It follows
that $p$ comes out of the loop at Line 1 to move to Line 1. ∎

######  Lemma B.8.

For each lock $\ell$ and each process $q$, if, for a process $p$, $PC_{p}$
points to a step of ${\ell}.\texttt{reset}_{p}()$ at time $t$, then $PC_{q}$
does not point to a step in ${\ell}.\texttt{try}_{q}()$ or
${\ell}.\texttt{exit}_{q}()$ at $t$.

###### Proof.

Suppose $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$ with $\mbox{\sc
S}_{p}=\mbox{\sc Seq}$ at time $t$. Assume for a contradiction that at $t$
there is a process $q$ such that
$\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:try:3}}$ with $\mbox{\sc
S}_{q}=\mbox{\sc Seq}-1$. By Condition 13 it follows that for each process
$r$, if
$\mbox{$PC_{r}$}\in\\{{\bf\ref{ln:fullcrash:rec:2}}\texttt{-}{\bf\ref{ln:fullcrash:rec:5}}\\}$
then $\mbox{\sc S}_{r}=\mbox{\sc Seq}-1$, which is a contradiction to our
original assumption that $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$ with
$\mbox{\sc S}_{p}=\mbox{\sc Seq}$. Thus there is no process $q$ such that
$\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:try:3}}$ with $\mbox{\sc
S}_{q}=\mbox{\sc Seq}-1$ at $t$. By the same argument we conclude that there
is no process $q$ such that $\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:exit:2}}$
with $\mbox{\sc S}_{q}=\mbox{\sc Seq}-1$. By Condition 11 we know that if for
a process $q$ if $\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:try:9}}$, $\mbox{\sc
S}_{q}=\mbox{\sc Seq}$. Thus, when $p$ is pointing to a step of $\mbox{\sc
Lock}[(\mbox{\sc Seq}-1)\%3].\texttt{reset}_{p}()$ at time $t$, there is no
process $q$ that points to a step in $\mbox{\sc Lock}[(\mbox{\sc
Seq}-1)\%3].\texttt{try}_{q}()$ or $\mbox{\sc Lock}[(\mbox{\sc
Seq}-1)\%3].\texttt{exit}_{q}()$ at $t$.

Suppose $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$ with $\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$ at time $t$. By Condition 11, for any process $q$, if
$\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:9}},{\bf\ref{ln:fullcrash:exit:2}}\\}$,
then $\mbox{\sc S}_{q}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$. It follows
that when $p$ is pointing to a step of $\mbox{\sc Lock}[(\mbox{\sc
Seq}-2)\%3].\texttt{reset}_{p}()$ (or equivalently $\mbox{\sc Lock}[(\mbox{\sc
Seq}+1)\%3].\texttt{reset}_{p}()$) at time $t$, there is no process $q$ that
points to a step in $\mbox{\sc Lock}[(\mbox{\sc
Seq}-2)\%3].\texttt{try}_{q}()$ or $\mbox{\sc Lock}[(\mbox{\sc
Seq}-2)\%3].\texttt{exit}_{q}()$ at $t$.

The claim thus follows from the above. ∎

###  B.3 Proof of properties

######  Lemma B.9 (Mutual Exclusion).

At most one process is in the CS in any configuration of any run.

###### Proof.

Assume for a contradiction that there are two processes $p$ and $q$ in the CS
in the same configuration. Therefore,
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:cs:1}}$ and
$\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:cs:1}}$ in the same configuration. By
Condition 9 we have $\mbox{\sc CSowner}=p$ as well as $\mbox{\sc CSowner}=q$
in the same configuration. Thus CSowner has two different values in the same
configuration, a contradiction. ∎

######  Lemma B.10 (Bounded Exit).

There is an integer $b$ such that if in any run any process $p$ invokes and
executes $\texttt{exit}_{p}()$ without crashing, the method completes in at
most $b$ steps of $p$.

###### Proof.

We note that the base algorithm satisfies the bounded exit property. From an
inspection of the algorithm we note that the $\texttt{exit}_{p}()$ procedure
from Figure 1 has a bounded number of steps and no loops. The claim thus
holds. ∎

######  Lemma B.11 (Starvation Freedom).

In every fair run, if a process $p$ executes the try method and no crash
occurs during this execution of the try method, then the method will
eventually complete, leading to $p$ entering the CS.

###### Proof.

Since there are only finitely many crash steps in the run, for the purpose of
the argument take a run and pick the earliest configuration from the run such
that all the crashes have already occurred. We need to show that if a process
$p$ is in $\texttt{try}_{p}()$ at a time $t$, it is in the CS at a different
time $t^{\prime}>t$. From an inspection of the algorithm we note that when the
method $\texttt{try}_{p}()$ returns, it puts $p$ in the CS because every
return statement returns the value IN_CS. Thus, we need to show that process
$p$ doesn’t forever get stuck at Lines 1, 1-1, 1, 1, or 1, which will ensure
that $p$ does return from $\texttt{try}_{p}()$. By Lemmas B.5, B.6, and B.7 we
know that $p$ eventually gets past the Lines 1-1, 1, and 1 respectively. When
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:3}}$, by Condition 11, $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$. If $\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$, by Condition 12, $\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]=true\vee(\exists
q,\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}\wedge\mbox{\sc
S}_{q}=\mbox{\sc S}_{p})$. In either case, $\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]=true$ eventually, which $p$ notices at the wait loop of Line 1 and
goes past the line. Hence, we assume that whenever $p$ executes Lines 1 or 1,
$\mbox{\sc S}_{p}=\mbox{\sc Seq}$, because that is the only other possibility
by Condition 11. Therefore, we will argue next that the starvation freedom
property of $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ is satisfied, which will
imply that $p$ gets past Lines 1 or 1. We know from an inspection of the
algorithm that any process that were to execute the $\texttt{reset}()$ at Line
1, would do so for $\mbox{\sc Lock}[\mbox{\sc Seq}-1]$ or $\mbox{\sc
Lock}[\mbox{\sc Seq}-2]$, because by Condition 11 $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$ for any process $p$ with
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$. It follows that from the last
crash onwards, no process will execute $\mbox{\sc Lock}[\mbox{\sc
Seq}\%3].\texttt{reset}()$, meeting the first condition for starvation freedom
on the base lock. It is straightforward that the second condition for
starvation freedom on the base lock is met. Lemmas B.5, B.6, and B.7 ensure
that the last condition for starvation freedom on the base lock is also met.
Hence we know that $\mbox{\sc Lock}[\mbox{\sc Seq}\%3]$ satisfies starvation
freedom. Therefore, a process $p$ gets past Lines 1 or 1 by the starvation
freedom property of the base lock. It follows that the claim holds. ∎

######  Lemma B.12 (Critical Section Reentry).

In any run, if a process $p$ crashes while in the CS, no other process enters
the CS until $p$ subsequently reenters the CS.

###### Proof.

The claim is immediate from Lemmas B.3 and B.9. ∎

######  Lemma B.13 (Bounded Recovery to CS/Exit).

There is an integer $b$ such that if in any run any process $p$ executes
$\texttt{recover}_{p}()$ without crashing and with $\mbox{\em
status}_{p}\in\\{\mbox{\em recover-from-cs},\mbox{\em recover-from-exit}\\}$,
the method completes in at most $b$ steps of $p$.

###### Proof.

An inspection of the $\texttt{recover}_{p}()$ method reveals that the method
completes within a constant number of steps, when a process $p$ executes
$\texttt{recover}_{p}()$ without crashing. ∎

######  Lemma B.14 (Fast Recovery to Remainder).

There is a constant $b$ (independent of $|{\mathcal{P}}|$) such that if in any
run any process $p$ executes $\texttt{recover}_{p}()$ without crashing and
with $\mbox{\em status}_{p}\in\\{\mbox{\em good},\mbox{\em recover-from-
rem}\\}$, the method completes in at most $b$ steps of $p$.

###### Proof.

An inspection of the $\texttt{recover}_{p}()$ method reveals that the method
completes within a constant number of steps, when a process $p$ executes
$\texttt{recover}_{p}()$ without crashing. ∎

######  Lemma B.15 (Bounded Recovery to Remainder).

There is an integer $b$ such that if in any run $\texttt{recover}_{p}()$,
executed by a process $p$ with $\mbox{\em status}_{p}=\mbox{\em recover-from-
try}$, returns IN_REM, $p$ must have completed that execution of
$\texttt{recover}_{p}()$ in at most $b$ of its steps.

###### Proof.

An inspection of the $\texttt{recover}_{p}()$ method reveals that the method
completes within a constant number of steps, when a process $p$ executes
$\texttt{recover}_{p}()$ without crashing. ∎

###  B.4 RMR Complexity

We know that the base lock incurs $O(1)$ RMR complexity to execute the
procedures $\texttt{try}_{p}()$, $\texttt{exit}_{p}()$, and
$\texttt{reset}_{p}()$. Hence, Lines 1, 1, 1, and 1 take $O(1)$ RMR to
execute. From an inspection of the algorithm it is clear that the rest of the
lines from the algorithm in Figure 1 incur $O(1)$ RMR on CC machines. It
follows that a process incurs $O(1)$ RMR per passage when executing the
algorithm in Figure 1.

###  B.5 Proof of Invariant

The proof of the invariant is in Appendix C

###  B.6 CC Algorithm Main theorem

The theorem below summarizes the result of the CC algorithm.

######  Theorem B.16.

The algorithm in Figure 1 solves the RME problem on CC machines for an
arbitrary and unknown number of processes. It satisfies mutual exclusion,
bounded exit, bounded critical section reentry, and starvation freedom. The
RMR complexity of the algorithm on CC machines is $O(1)$ per passage.

##  Appendix C Invariant Proof

######  Lemma C.1.

The algorithm in Figure 1 satisfies the invariant (i.e., the conjunction of
all the conditions) stated in Figure 2, i.e., the invariant holds in every
configuration of every run of the algorithm.

###### Proof.

We prove the lemma by induction. Specifically, we show (i) base case:  the
invariant holds in the initial configuration, and (ii) induction step:  if the
invariant holds in a configuration $C$ and a step of a process takes the
configuration $C$ to $C^{\prime}$, then the invariant holds in $C^{\prime}$.

In the initial configuration, we have $\mbox{\sc Seq}=1$, each of the
$\mbox{\sc Lock}[0\dots 2]$ are in their initial state, $\mbox{\sc
Stop}[0\dots 2]$ are all $false$, $\mbox{\sc CSowner}=\perp$, $\forall
p,\mbox{Active}_{p}=false$, and $\mbox{\sc S}_{p}=1$. Note, since the locks
are in their initial state, $\forall i\in[0,2],\mbox{\sc Lock}[i].\mbox{\em
status}=(\phi,\phi,\phi)$. Since all processes are in the Remainder section,
$\forall p,\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:1}}$. It follows that all
the conditions hold trivially the initial configuration. Hence, we have the
base case.

For the induction step, let $C$ be an arbitrary configuration of an arbitrary
run. The induction hypothesis states that Conditions 1 through 14 hold in $C$.
Let $(C,\sigma,C^{\prime})$ be an arbitrary (normal or crash) step of a
process in ${\mathcal{P}}$. We now establish the induction step by arguing
that each of Conditions 1 through 14 holds in $C^{\prime}$.

We use the following notation in the proof: (i) IH denotes the induction
hypothesis and, for all
$i\in[\ref{inv:fullcrash:cond1},\ref{inv:fullcrash:cond14}]$, IH:$i$ is the
part of IH that states that Condition $i$ of the invariant holds in $C$, and
(ii) If $D$ is any configuration and $x$ is any variable, $D.x$ is the value
of $x$ in $D$.

  1. 1.

Proof that Condition 1 holds in $C^{\prime}$
Seq changes only when some process executes Line 1. When a process $p$
executes that line, by IH:11, $\mbox{\sc S}_{p}\in\\{\mbox{\sc
Seq}-1,\mbox{\sc Seq}\\}$. If $\mbox{\sc S}_{p}=\mbox{\sc Seq}$, then Seq
increases by 1; otherwise, it remains unchanged. Thus, $C^{\prime}.\mbox{\sc
Seq}$ is always greater than or equal to 1.

Similarly, $\mbox{\sc S}_{p}$ changes at Line 1 or 1. When $\mbox{\sc S}_{p}$
changes at Line 1, it assumes the value of Seq, hence we have
$C^{\prime}.\mbox{\sc S}_{p}\leq C^{\prime}.\mbox{\sc Seq}$. When $\mbox{\sc
S}_{p}$ changes at Line 1, by IH:11, $\mbox{\sc S}_{p}=\mbox{\sc Seq}-1$.
Therefore, by the step $\mbox{\sc S}_{p}=\mbox{\sc Seq}$ and hence
$C^{\prime}.\mbox{\sc S}_{p}\leq C^{\prime}.\mbox{\sc Seq}$.

  2. 2.

Proof that Condition 2 holds in $C^{\prime}$
We establish each of the conjuncts of Condition 2 separately as below.

    1. (a).

$C^{\prime}.\mbox{\sc Lock}[(\mbox{\sc Seq}+1)\%3].\mbox{\sc
State}=(\phi,\phi,\phi)$.
Whenever the $\texttt{try}_{p}()$ or $\texttt{exit}_{p}()$ of the base lock is
called, it is called at Lines 1, 1, or 1. By IH:11, $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$ at these lines, which implies
that these lines do not affect either of $\mbox{\sc Lock}[(\mbox{\sc
Seq}+1)\%3].\mbox{\sc TrySet}$, $\mbox{\sc Lock}[(\mbox{\sc
Seq}+1)\%3].\mbox{\sc CSSet}$, or $\mbox{\sc Lock}[(\mbox{\sc
Seq}+1)\%3].\mbox{\sc ExitSet}$. The only place Seq is changed is at Line 1
when $\mbox{\sc S}_{p}=\mbox{\sc Seq}$. We know from IH:2 that when
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}$, $\mbox{\sc Lock}[(\mbox{\sc
S}_{p}-1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$. Since the step will
increment Seq by 1, it follows that $(C^{\prime}.\mbox{\sc
S}_{p}-1)\%3=((C^{\prime}.\mbox{\sc Seq}-1)-1)\%3=(C^{\prime}.\mbox{\sc
Seq}-2)\%3=(C^{\prime}.\mbox{\sc Seq}+1)\%3$. Therefore, by the step of $p$ at
Line 1 when $\mbox{\sc S}_{p}=\mbox{\sc Seq}$, $\mbox{\sc
Lock}[(C^{\prime}.\mbox{\sc Seq}+1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$.

    2. (b).

$C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rec:3}},{\bf\ref{ln:fullcrash:rec:4}}\\}\Rightarrow\mbox{\sc
Lock}[(C^{\prime}.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$.
To prove this implication, assume that
$C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rec:3}},{\bf\ref{ln:fullcrash:rec:4}}\\}$.

In case $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:2}}$, $p$ executes
$\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\texttt{reset}_{p}()$, which sets
$\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\mbox{\sc State}$ to
$(\phi,\phi,\phi)$.

In case
$C.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:rec:3}},{\bf\ref{ln:fullcrash:rec:4}}\\}$,
by IH:2 $\mbox{\sc Lock}[(C.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc
State}=(\phi,\phi,\phi)$ and the step from $C$ to $C^{\prime}$ is by some
$q\neq p$. $q$ can modify the TrySet, CSSet, or ExitSet of a lock only by
executing either of Lines 1, 1, or 1. By IH:11, $\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$ when
$\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:exit:2}}\\}$,
and $\mbox{\sc S}_{p}=\mbox{\sc Seq}$ when
$\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:try:9}}$. If $q$ executed a step with
$\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:exit:2}}\\}$
and $\mbox{\sc S}_{q}=\mbox{\sc Seq}-1$, then by IH:13, $C.\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$. We note that the step by $q$ doesn’t affect either
Seq or $\mbox{\sc S}_{p}$. Thus the step by $q$ doesn’t affect $\mbox{\sc
Lock}[(C.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc TrySet}$, $\mbox{\sc
Lock}[(C.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc CSSet}$, or $\mbox{\sc
Lock}[(C.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc ExitSet}$. Hence, by IH:2,
$\mbox{\sc Lock}[(C^{\prime}.\mbox{\sc S}_{p}-1)\%3].\mbox{\sc
State}=(\phi,\phi,\phi)$.

In case $q$ executed a step with
$\mbox{$PC_{q}$}\in\\{{\bf\ref{ln:fullcrash:try:3}},{\bf\ref{ln:fullcrash:try:9}},{\bf\ref{ln:fullcrash:exit:2}}\\}$
and $\mbox{\sc S}_{q}=\mbox{\sc Seq}$, we know from IH:11 that $C.\mbox{\sc
S}_{p}\in\\{\mbox{\sc Seq}-1,\mbox{\sc Seq}\\}$. It follows from IH:2 that
$C.\mbox{\sc Lock}[(\mbox{\sc S}_{p}-1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$
and since the step by $q$ doesn’t affect the TrySet, CSSet, or ExitSet for
either of $\mbox{\sc Lock}[(\mbox{\sc Seq}-1)\%3]$ or $\mbox{\sc
Lock}[(\mbox{\sc Seq}-2)\%3]$, we have $C^{\prime}.\mbox{\sc Lock}[(\mbox{\sc
S}_{p}-1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$.

  3. 3.

Proof that Condition 3 holds in $C^{\prime}$
We establish each of the conjuncts of Condition 3 separately as below.

    1. (a).

$C^{\prime}.\mbox{\sc Stop}[\mbox{\sc Seq}\%3]=false$.
A cell from Stop is changed only at Line 1 and 1. Line 1 sets $\mbox{\sc
Stop}[(\mbox{\sc S}_{p}-1)\%3]$ to $false$, therefore it is not of concern to
argue this case. If $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:5}}$, by IH:11,
$\mbox{\sc S}_{p}=\mbox{\sc Seq}-1$. It follows that an execution of Line 1
doesn’t modify $\mbox{\sc Stop}[\mbox{\sc Seq}\%3]$.

The only place Seq is changed is at Line 1 when $\mbox{\sc S}_{p}=\mbox{\sc
Seq}$. We know from IH:3 that $\mbox{\sc Stop}[(\mbox{\sc Seq}+1)\%3]=false$.
Since the step will increment Seq by 1, it follows that $(C^{\prime}.\mbox{\sc
Seq})\%3=(C.\mbox{\sc Seq}+1)\%3$. Therefore, by the step of $p$ at Line 1
when $\mbox{\sc S}_{p}=\mbox{\sc Seq}$, $\mbox{\sc Stop}[C^{\prime}.\mbox{\sc
Seq}\%3]=false$.

    2. (b).

$C^{\prime}.\mbox{\sc Stop}[(\mbox{\sc Seq}+1)\%3]=false$.
A cell from Stop is changed only at Line 1 and 1. Line 1 sets $\mbox{\sc
Stop}[(\mbox{\sc S}_{p}-1)\%3]$ to $false$, therefore it is not of concern to
argue this case. If $\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:5}}$, by IH:11,
$\mbox{\sc S}_{p}=\mbox{\sc Seq}-1$. It follows that an execution of Line 1
doesn’t modify $\mbox{\sc Stop}[(\mbox{\sc Seq}+1)\%3]$.

The only place Seq is changed is at Line 1 when $\mbox{\sc S}_{p}=\mbox{\sc
Seq}$. We know from IH:3 that when
$\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}$, $\mbox{\sc Stop}[(\mbox{\sc
S}_{p}-1)\%3]=false$. Since the step will increment Seq by 1, it follows that
$(C^{\prime}.\mbox{\sc S}_{p}-1)\%3=((C^{\prime}.\mbox{\sc
Seq}-1)-1)\%3=(C^{\prime}.\mbox{\sc Seq}-2)\%3=(C^{\prime}.\mbox{\sc
Seq}+1)\%3$. Therefore, by the step of $p$ at Line 1 when $\mbox{\sc
S}_{p}=\mbox{\sc Seq}$, $\mbox{\sc Stop}[(C^{\prime}.\mbox{\sc
Seq}+1)\%3]=false$.

    3. (c).

$C^{\prime}.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}\Rightarrow\mbox{\sc
Stop}[(C^{\prime}.\mbox{\sc S}_{p}-1)\%3]=false$.
To prove this implication, assume that
$C^{\prime}.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}$.

In case $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:3}}$, $p$ sets $\mbox{\sc
Stop}[(\mbox{\sc S}_{p}-1)\%3]$ to $false$ during the step.

In case $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:4}}$, by IH:3 $\mbox{\sc
Stop}[(C.\mbox{\sc S}_{p}-1)\%3]=false$ and the step from $C$ to $C^{\prime}$
is by some $q\neq p$. $q$ can set a cell from Stop to $true$ only at Line 1,
specifically, $q$ sets $\mbox{\sc Stop}[\mbox{\sc S}_{q}\%3]$ to $false$ at
Line 1. By IH:11 when $\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:5}}$,
$\mbox{\sc S}_{q}=\mbox{\sc Seq}-1$. It follows from IH:13 that $\mbox{\sc
S}_{p}=\mbox{\sc Seq}-1$.

Thus $\mbox{\sc Stop}[(C.\mbox{\sc S}_{p}-1)\%3]=\mbox{\sc
Stop}[(C^{\prime}.\mbox{\sc S}_{p}-1)\%3]=false$.

  4. 4.

Proof that Condition 4 holds in $C^{\prime}$
We establish each of the conjuncts of Condition 4 separately as below.

    1. (a).

$(C^{\prime}.\mbox{Active}_{p}=false\vee C^{\prime}.\mbox{\sc
S}_{p}<C^{\prime}.\mbox{\sc Seq}\vee
C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\})$
$\Rightarrow$ $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$.
We divide the implication into sub-parts as below and argue the correctness of
each part.

      1. i.

$C^{\prime}.\mbox{Active}_{p}=false$ $\Rightarrow$ $p\notin\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$.
To prove this implication, assume that $C^{\prime}.\mbox{Active}_{p}=false$.

In case $C.\mbox{Active}_{p}=false$, by IH:4 $p\notin\mbox{\sc
Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$ and the step from $C$ to
$C^{\prime}$ is by some $q\neq p$. The only step that can affect the condition
is $q$’s changing of the value of Seq, which could happen at Line 1 and that
line only increments Seq by 1. We note that IH:2 implies that $\mbox{\sc
Lock}[(C.\mbox{\sc Seq}+1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$ and $q$’s
increment of Seq means that $\mbox{\sc Lock}[(C^{\prime}.\mbox{\sc
Seq})\%3].\mbox{\sc State}=(\phi,\phi,\phi)$, which means $p\notin\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$.

In case $C.\mbox{Active}_{p}=true$, only $p$’s execution of one of Lines 1 or
1 could turn $\mbox{Active}_{p}$ to $false$. Hence,
$C.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:7}}\\}$.
By IH:4 we have that $p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$, which implies $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
Seq}\%3].\mbox{\sc Set}$.

      2. ii.

$C^{\prime}.\mbox{\sc S}_{p}<C^{\prime}.\mbox{\sc Seq}$ $\Rightarrow$
$p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$.
To prove this implication, assume that $C^{\prime}.\mbox{\sc
S}_{p}<C^{\prime}.\mbox{\sc Seq}$.

In case $C.\mbox{\sc S}_{p}<C.\mbox{\sc Seq}$, by IH:4 $p\notin\mbox{\sc
Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$ and the step from $C$ to
$C^{\prime}$ is by some $q\neq p$. This case is similar to the one as argued
for Case i argued above.

We know from IH:1 that $C.\mbox{\sc S}_{p}\leq C.\mbox{\sc Seq}$. Thus, the
other case is that $C.\mbox{\sc S}_{p}=C.\mbox{\sc Seq}$. It follows from an
inspection of the algorithm that $C^{\prime}.\mbox{\sc Seq}=C.\mbox{\sc
Seq}+1$, because $\mbox{\sc S}_{p}$ is never decremented. Thus, the step is an
execution of Line 1 by a process $q$ (possibly same as $p$). By IH:2 we have
$C.\mbox{\sc Lock}[(\mbox{\sc Seq}+1)\%3].\mbox{\sc State}=(\phi,\phi,\phi)$,
which implies that $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
Seq}\%3].\mbox{\sc Set}$.

      3. iii.

$C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\}$
$\Rightarrow$ $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$.
To prove this implication, assume that
$C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\}$.

In case
$C.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\}$,
by IH:4 $p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. If $p$
took a step at one of Lines 1 or 1 to move to Lines 1 or 1, respectively, the
step doesn’t affect $\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$.
Which implies $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$. In case the step from $C$ to $C^{\prime}$ is by some $q\neq p$, the
case is similar to the one as argued for Case i argued above.

Assume that
$C.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:1}},{\bf\ref{ln:fullcrash:exit:1}},{\bf\ref{ln:fullcrash:exit:2}},{\bf\ref{ln:fullcrash:rec:1}},{\bf\ref{ln:fullcrash:rec:5}}\\}$
so that due to a step by $p$,
$C^{\prime}.\mbox{$PC_{p}$}\in\\{{\bf\ref{ln:fullcrash:try:2}},{\bf\ref{ln:fullcrash:exit:3}},{\bf\ref{ln:fullcrash:exit:4}},{\bf\ref{ln:fullcrash:rec:6}},{\bf\ref{ln:fullcrash:rec:7}}\\}$.
If $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:1}}$, by IH:10
$\mbox{Active}_{p}=false$ and by IH:4, $p\notin\mbox{\sc Lock}[C.\mbox{\sc
Seq}\%3].\mbox{\sc Set}$, which implies that $p\notin\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. If
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:exit:1}}$, it follows from the step
that $C.\mbox{\sc S}_{p}\neq C.\mbox{\sc Seq}$ and by IH:1 $C.\mbox{\sc
S}_{p}<C.\mbox{\sc Seq}$. By IH:4 it follows that $p\notin\mbox{\sc
Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$, which implies that
$p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. If
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:exit:2}}$, the step completes $p$’s
execution of $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$ and
hence removes $p$ from $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
ExitSet}$. By IH:5 $p$ is in at most one of $\mbox{\sc Lock}[C.\mbox{\sc
S}_{p}\%3].\mbox{\sc TrySet}$, $\mbox{\sc Lock}[C.\mbox{\sc
S}_{p}\%3].\mbox{\sc CSSet}$, or $\mbox{\sc Lock}[C.\mbox{\sc
S}_{p}\%3].\mbox{\sc ExitSet}$, which implies that $p\notin\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc S}_{p}\%3].\mbox{\sc Set}$. If $C.\mbox{\sc
S}_{p}=C.\mbox{\sc Seq}$, we have $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
Seq}\%3].\mbox{\sc Set}$; otherwise $C.\mbox{\sc S}_{p}<C.\mbox{\sc Seq}$ and
by IH:4, $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$. If $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:1}}$, it follows that
either $C.\mbox{Active}_{p}=false$ or $C.\mbox{\sc S}_{p}<C.\mbox{\sc Seq}$,
in either case $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$ as already argued above. If
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:rec:5}}$, by IH:11 $C.\mbox{\sc
S}_{p}<C.\mbox{\sc Seq}$, which implies that $p\notin\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$ as already argued above.

    2. (b).

$C^{\prime}.\mbox{\sc S}_{p}<C^{\prime}.\mbox{\sc Seq}-1\Rightarrow
p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc S}_{p}\%3].\mbox{\sc Set}$.
To prove this implication, assume that $C^{\prime}.\mbox{\sc
S}_{p}<C^{\prime}.\mbox{\sc Seq}-1$.

If $C.\mbox{\sc S}_{p}<C.\mbox{\sc Seq}-1$, then by IH:4 $p\notin\mbox{\sc
Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc Set}$ and the step from $C$ to
$C^{\prime}$ is by some $q\neq p$. This step by $q$ doesn’t affect $\mbox{\sc
S}_{p}$ and doesn’t put $p$ in any sets associated with any base lock.
Therefore it follows that $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
S}_{p}\%3].\mbox{\sc Set}$.

Since $C^{\prime}.\mbox{\sc S}_{p}<C^{\prime}.\mbox{\sc Seq}-1$, the only
other case possible is that $C.\mbox{\sc S}_{p}=C.\mbox{\sc Seq}-1$. In this
case Seq was incremented due to an execution of Line 1 by a process $q$. Since
the step increments Seq, it follows that $C.\mbox{\sc S}_{q}=C.\mbox{\sc Seq}$
and hence $p\neq q$. By IH:4, since $\mbox{\sc S}_{p}<\mbox{\sc Seq}$,
$p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$ and hence
$p\notin\mbox{\sc Lock}[(C.\mbox{\sc Seq}-1)\%3].\mbox{\sc Set}$. By IH:2,
$p\notin\mbox{\sc Lock}[(C.\mbox{\sc Seq}+1)\%3].\mbox{\sc Set}$ which implies
that $p\notin\mbox{\sc Lock}[C^{\prime}.\mbox{\sc Seq}\%3].\mbox{\sc Set}$.
Since we have $C.\mbox{$PC_{q}$}={\bf\ref{ln:fullcrash:rec:4}}$, by IH:2,
$p\notin\mbox{\sc Lock}[(C.\mbox{\sc S}_{q}-1)\%3].\mbox{\sc Set}$, which
implies $p\notin\mbox{\sc Lock}[(C^{\prime}.\mbox{\sc Seq}+1)\%3].\mbox{\sc
Set}$ (because the step by $q$ increments Seq by 1 and $C.\mbox{\sc
S}_{q}=C.\mbox{\sc Seq}$). It follows that $p$ is not in any of the lock sets
and we have the implication.

  5. 5.

Proof that Condition 5 holds in $C^{\prime}$
$p$ is moved to different sets only due to the invocation/execution of
$\ell.\texttt{try}_{p}()$ and $\ell.\texttt{exit}_{p}()$ on the base lock
$\ell$.

When $p$ executes Line 1 to invoke $\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
S}_{p}\%3].\texttt{try}_{p}()$ at Line 1, by IH:4 $p\notin\mbox{\sc
Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. Similarly when it executes Line 1,
by IH:11 $C.\mbox{\sc S}_{p}=C.\mbox{\sc Seq}-1$ and thus by IH:4
$p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. Since
$C^{\prime}.\mbox{\sc S}_{p}=C.\mbox{\sc Seq}$ due to the step, it follows
that the condition holds in $C^{\prime}$.

When $p$ successfully completes $\mbox{\sc Lock}[C.\mbox{\sc
S}_{p}\%3].\texttt{try}_{p}()$ at Lines 1 or 1, $p$ is moved to $\mbox{\sc
Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$ and removed from $\mbox{\sc
Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc TrySet}$. Thus the condition holds in
$C^{\prime}$.

When $p$ invokes $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\texttt{exit}_{p}()$
at Line 1, $p$ is moved from $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
CSSet}$ to $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc ExitSet}$.
Similarly when $p$ completes $\mbox{\sc Lock}[C.\mbox{\sc
S}_{p}\%3].\texttt{exit}_{p}()$ successfully, $p$ is removed from $\mbox{\sc
Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc Set}$. Thus the condition holds in
$C^{\prime}$.

When a process $q$ executes $\mbox{\sc Lock}[C.\mbox{\sc
S}_{q}\%3].\texttt{reset}_{q}()$ at Line 1, it only empties the three sets.
Thereby $p$ is in none of the sets in $C^{\prime}$ and thus satisfying the
condition.

  6. 6.

Proof that Condition 6 holds in $C^{\prime}$
When a process $p$ takes a step from Line 1 in $C$ to go to Line 1 in
$C^{\prime}$, by IH:4 $p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc
Set}$. The implication then holds since invoking $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3].\texttt{try}_{p}()$ at Line 1 puts $p$ into $\mbox{\sc
Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc TrySet}$. Similarly, when a process $p$
takes a step from Line 1 to go to Line 1, we have $C.\mbox{\sc
S}_{p}=C.\mbox{\sc Seq}-1<C.\mbox{\sc Seq}$ by IH:11, and hence by IH:4
$p\notin\mbox{\sc Lock}[C.\mbox{\sc Seq}\%3].\mbox{\sc Set}$. The implication
again holds since invoking $\mbox{\sc Lock}[\mbox{\sc
S}_{p}\%3].\texttt{try}_{p}()$ at Line 1 puts $p$ into $\mbox{\sc
Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc TrySet}$.

If a process $q\neq p$ takes a step at Line 1 to execute $\mbox{\sc
Lock}[(\mbox{\sc S}_{q}-1)\%3].\texttt{reset}_{q}()$ and thus set $\mbox{\sc
Lock}[(\mbox{\sc S}_{q}-1)\%3].\mbox{\sc State}$ to $(\phi,\phi,\phi)$, we
first note that by IH:11 $\mbox{\sc S}_{q}\in\\{\mbox{\sc Seq}-1,\mbox{\sc
Seq}\\}$. If $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:3}}$ and
$C.\mbox{\sc S}_{p}=C.\mbox{\sc Seq}-1$, then by IH:13 $C.\mbox{\sc
S}_{q}=C.\mbox{\sc Seq}-1$, which implies that $q$’s step doesn’t affect
$\mbox{\sc Lock}[\mbox{\sc S}_{p}\%3].\mbox{\sc State}$. If $C.\mbox{\sc
S}_{p}=C.\mbox{\sc Seq}$, then since $\mbox{\sc S}_{q}\in\\{\mbox{\sc
Seq}-1,\mbox{\sc Seq}\\}$, $q$’s step only affects $\mbox{\sc
Lock}[(C.\mbox{\sc Seq}-1)\%3].\mbox{\sc State}$ or $\mbox{\sc
Lock}[(C.\mbox{\sc Seq}-2)\%3].\mbox{\sc State}=\mbox{\sc Lock}[(C.\mbox{\sc
Seq}+1)\%3].\mbox{\sc State}$, and not $\mbox{\sc Lock}[C.\mbox{\sc
Seq}\%3].\mbox{\sc State}$.

  7. 7.

Proof that Condition 7 holds in $C^{\prime}$
We divide the implication into sub-parts as below and argue the correctness of
each part.

    1. (a).

$(C^{\prime}.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:4}}\wedge
C^{\prime}.\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=false)\Rightarrow
p\in\mbox{\sc Lock}[C^{\prime}.\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$.
Here we first argue the correctness of the condition when $p$ takes a step so
that $C^{\prime}.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:4}}$. There are two
possibilities: $C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:3}}$ or
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:5}}$. In case
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:3}}$, we know that
$C^{\prime}.\mbox{\sc Stop}[\mbox{\sc S}_{p}\%3]=false$ from the hypothesis of
the implication. Since the step doesn’t change $C.\mbox{\sc Stop}[\mbox{\sc
S}_{p}\%3]$, it follows that $p$ completed the execution of $\mbox{\sc
Lock}[\mbox{\sc S}_{p}\%3].\texttt{try}_{p}()$ successfully. As a result of
that $p$ is removed from $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
TrySet}$ and put into $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
CSSet}$, and thereby $p\in\mbox{\sc Lock}[C^{\prime}.\mbox{\sc
S}_{p}\%3].\mbox{\sc CSSet}$. In case
$C.\mbox{$PC_{p}$}={\bf\ref{ln:fullcrash:try:5}}$, by IH:7 $p\in\mbox{\sc
Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$ and hence $p\in\mbox{\sc
Lock}[C^{\prime}.\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$. In either case
$p\in\mbox{\sc Lock}[C^{\prime}.\mbox{\sc S}_{p}\%3].\mbox{\sc CSSet}$.

If the step from $C$ to $C^{\prime}$ is by a process $q\neq p$, only a step at
Line 1 could possibly affect $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
State}$. The argument for this situation is same as that argued for Condition
6 above, which shows that $\mbox{\sc Lock}[C.\mbox{\sc S}_{p}\%3].\mbox{\sc
State}$ is unaffected by $q$’s step.

    2. (b).