Basic Properties

We present three lemmas about a process that is locally spinning and show that for any local-spin mutual exclusion algorithm, there exists a reachable system state at which some process is locally spinning.

First, a definition is needed to describe a system state at which some process is locally spinning in T. Informally, a process i locally spinning in T at a system state s has two features: by running i alone from s, (1) i will not perform any RMR step; and (2) i will never change regions. The definition below tries to capture this notion.

Definition 5.1 Let s be a system state of a mutual exclusion algorithm. We say that process i is locally spinning in T at s if

1. i is in T at s, and

2. for any finite i-execution fragment α executable from s, α contains no RMR step and i remains in T from s to α(s).

The following lemma says that whether a process is locally spinning at a system state depends on the state of the process and the values of its local shared variables.

Lemma 5.2 Let s and t be system states of a mutual exclusion algorithm such that s∼ⁱ

Vi

t for process i. Then i is locally spinning in T at s if and only if i is locally spinning in T at t.

Proof.

1. (→) Suppose i is locally spinning in T at s. Since i is in T at s and s∼ⁱ

Vi

t, i is in T at t. It remains to show that for any finite i-execution fragment α executable from t, α contains no RMR step and i remains in T from t to α(t). By way of contradiction, suppose that α is a finite i-execution fragment executable from t such that α contains an RMR step or i changes regions in α. Let α⁰ be the prefix of α including and ending with the first step that is either an RMR step or an operation that makes i change regions. Since s∼ⁱ

Vi

t, α⁰ is also executable from s. (If α⁰ ends with an RMR step, this follows from Corollary 2.3; otherwise, this follows from Lemma 2.2.) This contradicts the assumption that i is locally spinning in T at s.

2. (←) The other direction follows from symmetry.

2 The next lemma says that starting from a system state at which process i is locally spinning, i will not perform any RMR step before any other process takes an RMR step to i.

Lemma 5.3 Let s be a system state of a mutual exclusion algorithm at which process i is locally spinning in T. In any execution fragment executable from s, no RMR step from i exists before the first RMR step to i occurs.

Proof. Suppose for the sake of contradiction that α is an execution fragment executable from s in which an RMR step from i exists before the first RMR step to i occurs. We construct an i-execution fragment that is executable from s but ends with an RMR step from i. This contradicts the assumption that i is locally spinning at s.

Let α⁰ be the prefix of α including and ending with the first RMR step from i.

Note that the assumption on α implies that α⁰ contains no RMR step to i. We show that α⁰|i is also executable from s. This is the needed contradiction because α⁰|i ends with an RMR step from i. By the definition of α⁰, it is executable from s, ends

with an RMR step from i, and contains neither RMR steps from i nor RMR steps to i except the last step. Also, it is trivial that s∼ⁱ

Vi

s. By Corollary 2.3, α⁰|i is also

executable from s. 2

Intuitively, if a process i is locally spinning in T at some point and i enters C at a later point, then some other process must have taken at least one RMR step to wake up i. The next lemma, also called the inherent cost lemma, formalizes this intuition. A similar observation in a message-passing model can be found in Chandy and Misra’s work about “knowledge” among processes [12].

Lemma 5.4 (inherent cost) Let s be a system state of a mutual exclusion algo-rithm at which process i is locally spinning in T. Suppose that process i reaches C in a finite execution fragment α executable from s. Then, α must contain at least one RMR step to i.

Proof. By way of contradiction, suppose that α contains no RMR step to i. We con-struct an i-execution fragment that is executable from s but violates the assumption that i is locally spinning in T at s.

By Lemma 5.3, α contains no RMR step from i and therefore it contains neither RMR steps form i nor RMR steps to i. In addition, it is clear that s∼ⁱ

Vi

s. Thus, by Lemma 2.2, α|i is also executable from s and process i has the same state at α(s) and (α|i)(s). Since i is in C at α(s), i is also in C at (α|i)(s). Thus, α|i is the needed execution fragment because i changes regions in α|i. 2 Finally, the following lemma says that for any locspin mutual exclusion al-gorithm, if some process has been in C at a system state, then running another requesting process i alone eventually leads to a system state at which i is locally spinning.

Lemma 5.5 Let A be a local-spin mutual exclusion algorithm for n > 1 processes.

Let s be a reachable system state of A at which process i is in R and some other process is in C. Then there exists a finite i-execution fragment α executable from s such that i is locally spinning T at system state α(s).

Proof. Starting from s, let i enter T and continue to run i alone. This must lead to a system state at which i is locally spinning since otherwise the RMR time complexity would be unbounded or i would change regions. The former violates the assumption that A is a local-spin mutual exclusion algorithm; while, the latter

violates the mutual exclusion condition. 2