11institutetext: Department of Mathematics and Computer Science,
Eindhoven University of Technology
<EMAIL_ADDRESS>
#  Verification of the busy-forbidden protocol††thanks: This publication is
part of the MasCot PVSR project (00795160) which is partly financed by the
Dutch Research Council (NWO).
(using an extension of the cones and foci proof framework)

P.H.M. van Spaendonck  0000-0002-9536-1524

###### Abstract

The busy-forbidden protocol is a new readers-writer lock with no resource
contention between readers, which allows it to outperform other locks. For its
verification, specifications of its implementation and its less complex
external behavior are provided by the original authors but are only proven
equivalent for up to $7$ threads.

We provide a general equivalence proof using the cones and foci proof
framework, which rephrases whether two specifications are branching bisimilar
as six properties on the data objects of the specifications. We provide an
extension of this framework consisting of four additional properties and prove
that when the additional properties hold, the two systems are divergence-
preserving branching bisimilar, a stronger version of the aforementioned
relation that also distinguishes livelocks.

###### Keywords:

cones and foci proof framework $\cdot$ divergence-preserving branching
bisimulation $\cdot$ process algebra $\cdot$ protocol verification $\cdot$
readers-writer lock

##  1 Introduction

The readers-writer lock problem is a concurrency problem introduced and solved
by Courtois et al. [4]. The problem requires a synchronisation protocol that
provides safe access to both a shared readers section, which can be used
simultaneously by any number of threads, as well as an exclusive writer
section, which can not be used by more than one thread at any given time and
only when the readers section is not in use.

In [9], Groote et al. introduce a new readers-writer lock called the busy-
forbidden protocol. This locking protocol is of particular interest as it has
no resource contention between readers, and therefore provides a significant
speedup over other locks when having high readers section workloads.

To ensure the correctness of the protocol, the authors give process algebraic
specifications of both the implementation of the new algorithm as well as a
specification of its external behavior. The authors applied model checking and
proved the implementation and external behavior equivalent for up to $7$
threads using the mCRL2 toolset [3], but they were unable to do this for more
concurrent threads due to the statespace of the implementation becoming too
large.

But as readers-writer locks often use a large number of concurrent threads, a
general correctness proof for the busy-forbidden protocol is desired. We opt
to prove the process algebraic specifications of the implementation and
external behavior to be equivalent. The advantage of this technique over
contract-based approaches, such as Floyd-Hoare logic [11], and its extension
for parallel composed systems by Owicki and Gries [15, 16], is that the much
smaller equivalent model can also be used for the modeling and verification of
systems built on top of the busy-forbidden protocol. We consider this a
significant advantage, as this is the typical use-case for readers-writer
locks, e.g. the parallel term library which the protocol was originally
designed for.

We prove the equivalence of the implementation and its external behavior by
using the cones and foci proof framework, originally proposed in [8] by Groote
and Springintveld and later generalized by Fokkink et al. in [5]. This
framework simplifies the often complex and cumbersome branching bisimulation
proof by reducing it to a small set of propositions on the data objects
occurring in the implementation and specification. If these propositions are
shown to hold, it follows that the two systems are equivalent modulo branching
bisimulation.

The proof framework has already been used in several case studies to prove
implementation and specification models equivalent, such as the verification
of the 1-bit sliding window protocol in [1], a complex leader election
protocol in [6], and a part of the IEEE P1394 high-speed bus protocol [12] in
[17].

Since the equivalence relation proven by the cones and foci proof framework
does not distinguish livelock, we first provide an extension to the framework
such that it can also be used to prove equivalence modulo divergence-
preserving branching bisimulation. This relation is a stronger version of
branching bisimulation that does distinguish livelocks [7]. Our extension
provides four additional propositions on the data objects in the
implementation and specification models, that, when shown to also hold, imply
the equivalence of the two processes modulo divergence-preserving branching
bisimulation. We give a soundness proof of this extension and use it to prove
the equivalence of implementation and specification of the busy-forbidden
protocol.

##  2 The busy-forbidden protocol

We first discuss the busy-forbidden protocol. An overview of its
implementation using pseudocode is given in Table 1. The enter_- and
leave_shared functions are used to have a thread $p$ enter or leave the
readers section. Similarly, enter_- and leave_exclusive provide functionality
for safe access to the writer section.

The protocol uses two binary flags per thread and a single mutex. The first
flag, the busy flag, indicates that a thread is either working or going to
work inside of the readers section. The second flag, the forbidden flag,
indicates that a thread is not allowed to enter the readers section. All flags
are initially set to false. The mutex, called mutex, enforces exclusive access
to the writer section.

$\texttt{enter\\_shared}(\textit{thread}~{}p):$ $p.\textit{busy}:=\textit{true}$; $\textbf{while}~{}p.\textit{forbidden}$ $p.\textit{busy}:=\textit{false};$ $\textbf{if}~{}\textit{mutex}.\textit{timed\\_lock}()$ $\textit{mutex}.\textit{unlock}();$ $p.\textit{busy}:=\textit{true};$ |  $\texttt{enter\\_exclusive}(\textit{thread}~{}p):$ $\textit{mutex}.\textit{lock}();$ $\textbf{while exists}~{}\textit{thread}~{}q\textbf{ with}$ $\neg q.\textit{forbidden}$ $\textbf{select}~{}\textit{thread}~{}r$ $r.\textit{forbidden}:=\textit{true};$ $\textbf{if}~{}r.\textit{busy}~{}\textbf{or sometimes}$ $r.\textit{forbidden}:=\textit{false};$
---|---
$\texttt{leave\\_shared}(\textit{thread}~{}p):$ $p.\textit{busy}:=\textit{false};$ |  $\texttt{leave\\_exclusive}(\textit{thread}~{}p):$ while exists thread q with $q.\textit{forbidden}$ $\textbf{select }\textit{thread }r$ usually do
$r.\textit{forbidden}:=\textit{false};$ sometimes do
$r.\textit{forbidden}:=\textit{true}$ $mutex.unlock();$
Table 1: Pseudocode description of the busy-forbidden protocol.

When entering the readers section, a thread sets its busy flag and enters iff
its forbidden flag is false. If the forbidden flag is true, the busy flag is
set back to false to avoid deadlock and the process is repeated again. To
reduce resource contention on the flags, a
$\textit{mutex}.\textit{timed\\_lock}()$ can be used without altering the
externally visible behavior of the protocol [9]. Upon leaving the readers
section, the thread sets its busy flag back to false.

A thread that wants to enter the writer section must first acquire the mutex.
This ensures that no other thread can be in the writer section simultaneously
and that only the given thread is altering the forbidden flags. Once the mutex
has been acquired, the thread sets the forbidden flag of each thread, but will
immediately undo this if the busy flag of the same thread is true. To prevent
a thread that is acquiring the writer section from locking out some reader
threads while still waiting for others to leave the readers section, random
forbidden flags can sometimes be set back to false. The writer section is
entered once all forbidden flags are true. Upon leaving, all forbidden flags
are set back to false and the mutex is released. During this, random forbidden
flags can be set back to true. This prevents each iteration that occurs while
leaving, from becoming externally visible and significantly reduces the number
of states in the external specification.

The externally visible behavior of the protocol is given in Figure 1 and, as
we will prove later, provides an equivalent overview of how threads interact
via the protocol. Individual threads move from node to node. Transition labels
ending with -call represent the identically named function being called by a
thread moving across, and those ending with -return represent those function
calls terminating. All transitions not labeled as such represent some sequence
of internal calculations that occurs during these function calls. Transitions
labeled with a guard, i.e. starting with if, only allow a thread to progress
if the given condition is met.

The Free node represents a thread not interacting with the protocol and being
outside of any section. Each thread initially starts out in this node. The
Shared and Exclusive nodes represent the readers and writer sections,
respectively.

A thread starting to acquire the readers lock enters the EnterShared (ES)
node. The thread stays in the ES node as long as its forbidden flag is true.
As repeatedly checking the flag is discouraged through the timed_lock call,
the internal loop is labeled as improbable. When the forbidden flag is
evaluated to false, the thread moves to the LockedOffExclusive (LOE) node.
After this, it is no longer possible for any other thread to enter the writer
section until the readers section is completely freed. The LeaveShared (LS)
node represents a thread leaving this section.

FreeESLOESharedLS Enter
---
shared
call
if No threads in
---
LOS or Exclusive
improbable
---
if At least 1 thread
in LOS or Exclusive
Enter
---
shared
return
Leave
---
shared
call
Leave
---
shared
return
EESAFLOSExclusiveLEOE Enter
---
exclusive
call
if No threads in
---
SAF, LOS, LE
or Exclusive
improbable if No threads in
---
LOE or Shared
Enter
---
exclusive
return
Leave
---
exclusive
call
improbable Leave
---
exclusive
return
Figure 1: The external behaviour.

When a thread tries to acquire the writer lock, it enters the EnterExclusive
(EE) node. Once the thread acquires the mutex variable, it will move to the
SetAllForbidden (SAF) node and it will not be possible for any other thread to
acquire the writer lock before it is released by this thread. The loop in the
SAF node represents a forbidden flag being set back to false; this transition
is labeled as improbable as this only rarely occurs. Once the last busy flag
is evaluated to false, exclusive access is attained and the thread will move
to the LockedOutShared (LOS) node before officially terminating the function
call.

When the thread starts releasing the writer lock, it enters the
LeavingExclusive (LE) node. Similar to the SAF node, a thread within the LE
node can repeatedly turn the forbidden flag off and on again, thus never fully
opening up the readers section. Because a forbidden flag is only very rarely
set back to true when releasing the lock, this transition is also labeled as
improbable. Once the last forbidden flag is set to false, this is no longer
possible and the thread moves to the OpenedExclusive (OE) node, after which it
will officially terminate the function call and move back to the Free node.

We can use the model of the external behavior to reason about certain safety
properties. For example, from the guarded transitions from ES to LOE and from
SAF to LOS, we can quickly see that the Shared and Exclusive sections can not
be populated simultaneously, as they require the other respective section to
be empty. The guarded transition from EE to SAF also assures that only a
single thread can be present in the Exclusive section at any given time.

##  3 Linear process equations

Both the implementation of the pseudocode shown in Table 1 and the external
behavior have been modeled in the mCRL2 language [10]. The mCRL2 language is
based on the Algebra of Communicating Processes [2] and Calculus of
Communicating Processes [14].

The mCRL2 language models processes using a combination of states and actions.
States represent a collection of internal values that are used to calculate
which actions can occur and what the resulting state will be. Actions
represent any sort of atomic event such as calling a function, or setting or
reading a flag. An action consists of a label and a possible set of data
parameters, e.g. the action $\textit{lock}(p)$ has lock as the label and $p$
as the data parameter. Parameters can be of varying types such as booleans,
algebraic data types, and mappings. The exact data types used within the busy-
forbidden models are given later.

A special action $\tau$, the so-called hidden or internal action, is used to
represent an action that is externally not directly visible. We use distinct
action labels for internal actions to be able to easily distinguish between
them. We explicitly state which actions should be considered to be $\tau$
actions.

We require all process algebraic equations to be in a clustered linear form,
see Definition 1. This form specifies for each action when it can occur and
what the resulting state will be. The $\sum_{e{:}S}$ operator models the
application of the non-deterministic choice operator $+$ over all elements in
some set $S$. We also allow process equations in which the $\sum$ operators
are split into separate smaller $\sum$ operators and individual $+$ operators.

Since the cones and foci proof framework concerns itself only with the actions
that are enabled in a single given state, the clustered normal form becomes
especially useful, as we can directly infer for any given state if an action
is enabled and what the resulting state will be. In [19], Usenko shows that
any mCRL2 specification can be transformed into a clustered linear process
equation.

###### Definition 1

A clustered linear process equation (LPE) is a process specification of the
form:

$X(d{:}D)=\sum_{a{:}\textit{Act}}\,\sum_{e_{a}{:}E_{a}}c_{a}(d,e_{a})\to
a(f_{a}(d,e_{a}))\cdot X(g_{a}(d,e_{a}))\text{,}$

where $D$ is the set of states, Act is the set of action labels including
$\tau$, $E_{a}$ is an indexed set of all data types that need to be considered
for label $a$, the boolean function $c_{a}(d,e_{a})$ specifies when the action
$a$ with parameters resulting from the function $f_{a}(d,e_{a})$ is enabled in
state $d$, and $g_{a}(d,e_{a})$ gives the resulting state from taking this
action from state $d$.

Often we end up in a situation in which the set of states $D$ also contains
unreachable states. As we are only interested in the reachable states, we
introduce the notion of an invariant in Definition 2. An invariant is a
predicate on states in an LPE such that when it holds for a given state
$d{:}D$, it also holds for all subsequent states.

###### Definition 2

Given a clustered LPE $X$ as per Definition 1. A predicate $\mathcal{I}$ on
the set of states $D$ is called an invariant iff the following holds: for all
$a{:}\textit{Act},d{:}D$ and $e_{a}{:}E_{a}$,

$\mathcal{I}(d)\wedge c_{a}(d,e_{a})\Rightarrow\mathcal{I}(g_{a}(d,e_{a}))$

##  4 Equivalence and the cones and foci proof framework

As stated before, we prove the model of the implementation and the
specification of the busy-forbidden protocol equivalent modulo divergence-
preserving branching bisimulation. We define this equivalence relation in
Definition 4, which is based on the definitions used in [13] and has been
adapted to work with process equations instead of transition systems. In
Definition 3, we provide some syntactic glue to make this shift between
labeled transition systems and clustered LPEs more intuitive.

###### Definition 3

Given a clustered LPE as per Definition 1, states $d,d^{\prime}\in D$, and
action l, we define the following relations:

  * •

$d\xrightarrow{l}d^{\prime}$ iff there is an action $a$ with an associated
data type $e_{a}$ such that $l=a(f_{a}(d,e_{a}))$, the condition
$c_{a}(d,e_{a})$ holds, and $g_{a}(d,e_{a})=d^{\prime}$.

  * •

$d\xrightarrow{l}\\!\\!\\!^{*}d^{\prime}$ iff there is a finite sequence of
states $d_{0},\ldots,d_{k}$ such that $d_{0}=d$, $d_{k}=d^{\prime}$ and for
all $0\leq i<k$ we have $d_{i}\xrightarrow{l}d_{i+1}$.

###### Definition 4

Given two clustered LPEs as per Definition 1 with sets of states $D$ and
$D^{\prime}$. A relation $R$ on the states $D\times D^{\prime}$ is a
divergence-preserving branching bisimulation iff the following conditions for
all states $s\in D$, $t\in D^{\prime}$, and actions
$\textit{l}\in\textit{Act}$ hold:

  * ($\textit{B}_{1}$)

If $sRt$ and $s\xrightarrow{l}s^{\prime}$ for some state $s^{\prime}\in D$,
then either $l=\tau$ and $s^{\prime}Rt$, or there are states
$t^{\prime},t^{\prime\prime}\in D^{\prime}$ such that
$t\xrightarrow{\tau}\\!^{*}t^{\prime}\xrightarrow{l}t^{\prime\prime}$,
$sRt^{\prime}$, and $s^{\prime}Rt^{\prime\prime}$.

  * ($\textit{B}_{2}$)

If $sRt$ and $t\xrightarrow{l}t^{\prime}$ for some state $t^{\prime}\in
D^{\prime}$, then either $l=\tau$ and $sRt^{\prime}$, or there are states
$s^{\prime},s^{\prime\prime}\in D$ such that
$s\xrightarrow{\tau}\\!^{*}s^{\prime}\xrightarrow{l}s^{\prime\prime}$,
$s^{\prime}Rt$, and $s^{\prime\prime}Rt$.

  * ($\textit{D}_{1}$)

If $sR\,t$ and there is an infinite sequence of states
$(s_{n})_{n\in\mathbb{N}}$ such that $s=s_{0}$, and
$s_{k}\overset{\tau}{\to}s_{k+1}$ and $s_{k}R\,t$ for all $k\in\mathbb{N}$,
then there is a state $t^{\prime}\in D^{\prime}$ such that
$t\overset{\tau}{\to}t^{\prime}$, and $s_{k}R\,t^{\prime}$ for some
$k\in\mathbb{N}$.

  * ($\textit{D}_{2}$)

If $sR\,t$ and there is an infinite sequence of states
$(t_{n})_{n\in\mathbb{N}}$ such that $t=t_{0}$, and
$t_{k}\overset{\tau}{\to}t_{k+1}$ and $sR\,t_{k}$ for all $k\in\mathbb{N}$,
then there is a state $s^{\prime}\in D$ such that
$s\overset{\tau}{\to}s^{\prime}$, and $s^{\prime}R\,t_{k}$ for some
$k\in\mathbb{N}$.

Two clustered LPEs with respective initial states $d_{0}$ and $d_{0}^{\prime}$
are divergence-preserving branching bisimilar iff there is a divergence-
preserving branching bisimulation $R$ such that $d_{0}R\,d_{0}^{\prime}$.

Note that in (divergence-preserving) branching bisimulation, $\tau$-actions
are said to be externally visible iff their begin- and endpoint are not
equivalent.

In [8], it is noted that in communicating systems, equivalent states often
have a “cone-like” structure as is shown in Figure 2. In this figure,
equivalent states are grouped together in the cone $C$. In the focus point
state fc, all externally visible actions of said cone, i.e. $a$ and $b$, are
enabled. For all other states in which not all externally visible actions are
simultaneously enabled, such as $d$ or the states along the edges, there is
always a path of internal actions, i.e. $\tau$ actions within the cone, that
ends in the state fc. We show one such path for the state $d$, using the
dashed arrows.

fc$d$$a$$b$$a$$a$$a$$a$$b$$b$$b$$b$$C$ Figure 2: A cone $C$ with focus point
fc.

If a given system consists of such “cones”, the cones and foci proof framework
can be used to prove equivalence. To do so, we must provide a state mapping
$h:D\to D^{\prime}$ that maps states in the implementation to their equivalent
state in the specification, a focus condition $\textit{FC}:D\to\mathbb{B}$
that indicates if a state should be considered a focus point, i.e. all
externally observable actions are enabled, and a well-founded ordering $<_{M}$
on $D$ that orders states by their distance to a focus point. We must then
prove that a small set of requirements are met by the LPEs and the provided
state mapping, focus condition and ordering.

Any $\tau$ action in the implementation that does not leave a cone, i.e. the
state mapping $h$ maps begin- and endpoint to the same state, is renamed to
int (short for internal action). This allows us to easily distinguish between
$\tau$ actions that are externally observable, i.e. that are preserved in our
specification, and those that are not. While an int action is considered a
$\tau$ action, we exclude them from the set of actions Act.

In Theorem 4.1, we extend the proof framework towards divergence-preserving
branching bisimulation with a labeling $p$ on cones that labels cones as
either divergent $(\Delta)$ or non-divergent $(\nabla)$, and four additional
requirements on the LPEs. The divergent $\tau$-loops in the specification,
i.e. a $\tau$ transition with the same begin- and endpoint, are renamed to int
to relate these to the divergent internal behavior in the implementation, i.e.
repeatable paths of int actions.

###### Theorem 4.1

Consider a clustered linear process equation of an implementation with initial
state $d_{0}$ and some invariant $\mathcal{I}$ that holds in $d_{0}$,

$X(d{:}D)=\sum_{a{:}\textit{Act}\cup\\{\textit{int}\\}}\sum_{e_{a}{:}E_{a}}c_{a}(d,e_{a})\rightarrow
a(f_{a}(d,e_{a}))\cdot X(g_{a}(d,e_{a}))\text{,}$

and a clustered linear process equation of a specification with initial state
$d_{0}^{\prime}$,

$Y(d^{\prime}{:}D^{\prime})=\sum_{a{:}\textit{Act}\cup\\{\textit{int}\\}}\sum_{e_{a}{:}E_{a}}c_{a}^{\prime}(d^{\prime},e_{a})\rightarrow
a(f_{a}^{\prime}(d^{\prime},e_{a}))\cdot
Y(g_{a}^{\prime}(d^{\prime},e_{a}))\text{.}$

The LPEs $X$ and $Y$ are divergence-preserving branching bismilar if there is
a state mapping $h:D\to D^{\prime}$, a focus condition
$\textit{FC}:D\to\mathbb{B}$, a well founded ordering $<_{M}$ on $D$, and a
cone labeling $p:D^{\prime}\to\\{\Delta,\nabla\\}$ such that
$h(d_{0})=d_{0}^{\prime}$ and the following requirements hold for all states
$d{:}D$ in which invariant $\mathcal{I}$ holds:

  1. I

If not a focus point, there is at least one internal step such that the target
state is closer to the focus point:

$(\neg\textit{FC}(d))\Rightarrow(\exists
e_{\textit{int}}{:}E_{\textit{int}}.~{}c_{\textit{int}}(d,e_{\textit{int}})\wedge
g_{\textit{int}}(d,e_{\textit{int}})<_{M}d)$

  2. II

For every internal step, the mapping $h$ maps source and target states to the
same states in the specification:

$\forall
e_{\textit{int}}{:}E_{\textit{int}}.c_{\textit{int}}(d,e_{\textit{int}})\Rightarrow
h(d)=h(g_{\textit{int}}(d,e_{\textit{int}}))$

  3. III

Every visible action in the specification must be enabled after a finite
number of int actions for each corresponding focus point: For all
$a{:}\textit{Act}$

$\forall e_{a}{:}E_{a}.(\textit{FC}(d)\wedge
c_{a}^{\prime}(h(d),e_{a}))\Rightarrow(\exists
d_{\textit{int}}{:}D.d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}d_{\textit{int}}\wedge
c_{a}(d_{\textit{int}},e_{a}))$

  4. IV

Every visible action in the implementation must be mimicked in the
corresponding state in the specification: For all $a{:}\textit{Act}$

$\forall e_{a}{:}E_{a}.c_{a}(d,e_{a})\Rightarrow c_{a}^{\prime}(h(d),e_{a})$

  5. V

Matching actions have matching parameters: For all $a{:}\textit{Act}$

$\forall e_{a}{:}E_{a}.c_{a}(d,e_{a})\Rightarrow
f_{a}(d,e_{a})=f^{\prime}_{a}(h(d),e_{a})$

  6. VI

For all matching actions in specification and implementation, their endpoints
must be related: For all $a{:}\textit{Act}$

$\forall e_{a}{:}E_{a}.c_{a}(d,e_{a})\Rightarrow
h(g_{a}(d,e_{a}))=g_{a}^{\prime}(h(d),e_{a})$

  1. I$\\!{}_{\Delta}$

Any internal action in the specification is part of an int-loop:

$\forall_{e_{\textit{int}}}{:}E_{\textit{int}}.c_{\textit{int}}^{\prime}(h(d),e_{\textit{int}})\Rightarrow
g_{\textit{int}}^{\prime}(h(d),e_{\textit{int}})=h(d)$

  2. II$\\!{}_{\Delta}$

The cone labeling indicates whether or not a specification state allows an
int-loop:

$p(h(d))=\Delta\Leftrightarrow(\exists
e_{\textit{int}}{:}E_{\textit{int}}.~{}c^{\prime}_{\textit{int}}(h(d),e_{\textit{int}}))$

  3. III$\\!{}_{\Delta}$

A cone is labelled as divergent if and only if it is possible to take an
internal action in its focus points:

$\textit{FC}(d)\Rightarrow(p(h(d))=\Delta\Leftrightarrow\exists
e_{\textit{int}}{:}E_{\textit{int}}.c_{\textit{int}}(d,e_{\textit{int}}))$

  4. IV$\\!{}_{\Delta}$

All internal transitions within a non-divergent cone must bring us closer to a
focus point:

$\forall e_{\textit{int}}{:}E_{\textit{int}}.((p(h(d))=\nabla\wedge
c_{\textit{int}}(d,e_{\textit{int}}))\Rightarrow
g_{\textit{int}}(d,e_{\textit{int}})<_{M}d)$

Proof. We define $R\subseteq D\times D^{\prime}$ as $\\{\langle
d,h(d)\rangle~{}|~{}d\in D\wedge\mathcal{I}(d)\\}$.

Proving that $R$ is a branching bisimulation, i.e. proving conditions
$\textit{B}_{1}$ and $\textit{B}_{2}$ from Defininition 4, follows the same
general proof structure as is used in both [5], and [8]. We give a concise
proof sketch.

Condition $\textit{B}_{1}$. Consider the states $d,d^{\prime}{:}D$, and label
$l{:}\textit{Act}\cup\\{\textit{int}\\}$ such that
$d\overset{a}{\to}d^{\prime}$. As per Requirement II, if $l=\textit{int}$ then
$h(d)=h(d^{\prime})$. If $l\neq\textit{int}$, then we have
$h(d)\overset{l}{\to}h(d^{\prime})$ as per Requirement IV, and VI.

Condition $\textit{B}_{2}$. Consider the states
$d{:}D,d^{\prime}_{2}{:}D^{\prime}$, and label
$l{:}\textit{Act}\cup\\{\textit{int}\\}$ such that
$h(d)\overset{l}{\to}d_{2}^{\prime}$. If $l=\textit{int}$, then
$h(d_{2}^{\prime})=h(d)$, as per Requirement I$\\!{}_{\Delta}$. If
$l\neq\textit{int}$, then there is a state $d_{2}{:}D$ such that
$d\xrightarrow{\small{\textit{int}}}\\!\\!\\!^{*}d_{2}$ and
$\textit{FC}(d_{2})$ as per Requirement I and $<_{M}$ being well founded. As
per Requirements III and VI, there are states $d_{3},d_{4}{:}D$ such that
$d\xrightarrow{\small{\textit{int}}}\\!\\!\\!^{*}d_{2}\xrightarrow{\small{\textit{int}}}\\!\\!\\!^{*}d_{3}\overset{l}{\to}d_{4}$
and $h(d_{4})=d_{2}^{\prime}$. From Requirement II follows that all states
along the int path are related to $h(d)$.

We show that the branching bisimulation $R$ is also divergence-preserving by
proving the two remaining conditions.

Condition $\textit{D}_{1}$. Consider the pair $\langle d,h(d)\rangle\in R$ and
an infinite sequence $(d_{n})_{n\in\mathbb{N}}$ over states in $D$ such that
$d_{0}=d$ and for any $n\in\mathbb{N}$ we have $h(d_{n})=h(d)$ and
$d_{n}{\xrightarrow{\scriptsize{\textit{int}}}}d_{n+1}$. We show that there is
some $e_{\textit{int}}{:}E_{\textit{int}}$ such that
$c^{\prime}_{\textit{int}}(h(d),e_{\textit{int}})$ and
$g^{\prime}_{\textit{int}}(h(d),e_{\textit{int}})=h(d)$. If $h(d)$ is labeled
$\Delta$ then this directly follows from Requirements I$\\!{}_{\Delta}$, and
II$\\!{}_{\Delta}$.

Assume, for sake of contradiction, that $h(d)$ is labeled as $\nabla$ instead.
Since $<_{M}$ is a well-founded ordering on $D$, the sequence
$(d_{n})_{n\in\mathbb{N}}$ contains some minimal element $d_{\bot}$ such that
no other element in the sequence is smaller than $d_{\bot}$. However, as per
Requirement IV$\\!{}_{\Delta}$, any outgoing int action from $d_{\bot}$ must
have an endpoint that is smaller than $d_{\bot}$, and thus the state that
comes directly after $d_{\bot}$ in the sequence would have to be smaller,
contradicting that $d_{\bot}$ is the minimal element.

Condition $\textit{D}_{2}$. Consider the pair $\langle d,h(d)\rangle\in R$ and
an infinite sequence $(d^{\prime}_{n})_{n\in\mathbb{N}}$ over states in
$D^{\prime}$ such that $d^{\prime}_{0}=h(d)$ and for any $n\in\mathbb{N}$ we
have $d~{}R~{}d^{\prime}_{n}$, i.e. $d^{\prime}_{n}=h(d)$, and
$d^{\prime}_{n}{\xrightarrow{\scriptsize{\textit{int}}}}d^{\prime}_{n+1}$.

Since $h(d)$ allows an int-loop, we have $p(h(d))=\Delta$ as per Requirement
II$\\!{}_{\Delta}$. If $d$ is not a focus point then this action is enabled as
per Requirement I. If $d$ is a focus point then this action is enabled as per
Requirement III$\\!{}_{\Delta}$, since its corresponding cone is labeled as
$\Delta$. Requirement II gives us that the endpoint of this internal action is
related to $h(d)$. Thus, if a state in the specification diverges then so do
the related states in the implementation.

We thus conclude that the relation $R$ is a divergence-preserving branching
bisimulation.∎

##  5 Models of the specification and the implementation

We now discuss the models of the specification and implementation of the busy-
forbidden protocol, such that we can use the extended proof framework to prove
them equivalent in Section 6. From here on, we use $N$ to denote the number of
concurrent threads and we define $P=\\{p_{1},\ldots,p_{N}\\}$ to be the set
containing all $N$ threads.

The linear process equation of the external behavior of the busy-forbidden
protocol is given in Table 9 in the appendix [18]. The set $S$ contains the
nodes shown in Figure 1. Each state in the specification is represented using
a mapping $s$ that maps each thread to its current node, with each thread
starting in the Free node. The set of specification states for $N$ threads is
denoted by $D^{\prime}_{N}$. Note that each condition in the specification is
the same as the conditions shown in Figure 1. The improbable actions are
considered to be int actions.

The linear process equation of the implementation is given in Table 10 in the
appendix [18]. All non-typewriter font actions are considered to be $\tau$
actions and italicized actions are specifically considered to be int actions.
The set of implementation states $D_{N}$ is given in Definition 5. A part of
each state consists of $N$ substates, with each substate giving the state of
that specific thread. The set of substates is given in Definition 6, in which
substates corresponding to the same node are grouped together.

###### Definition 5

Each state in the linearized process of the busy-forbidden implementation for
$N$ threads is defined as the tuple

$d=\langle
d_{p_{1}},d_{p_{2}},\ldots,d_{p_{N}},\textit{busy},\textit{forbidden},\textit{mtx}\rangle{:}D_{N}\text{,
in which:}$

  * •

$d_{p_{1}},d_{p_{2}},\ldots,d_{p_{N}}$ are the substates of threads $1$
through $N$.

  * •

$\textit{busy}:P\rightarrow\mathbb{B}$ is the mapping that keeps track of all
the busy flags, in which $\textit{busy}(p)$ is the current value of the busy
flag of thread $p$.

  * •

$\textit{forbidden}:P\rightarrow\mathbb{B}$ is the mapping that keeps track of
all the forbidden flags in the same way as the busy mapping.

  * •

mtx is a boolean that indicates whether the mutual exclusion variable mtx is
locked or unlocked.

###### Definition 6

The set of substates for each individual process is defined as the union of
the following sets:

  * •

$\textit{Free}=\\{\textit{Free}\\}$,
$\textit{ES}=\\{\textit{ES}_{1},\textit{ES}_{2},\textit{ES}_{3},\textit{ES}_{4}\\}$,
$\textit{LOE}=\\{\textit{LOE}\\}$,
$\textit{Shared}=\\{\textit{Shared}\\}$,
$\textit{LS}=\\{\textit{LS}_{1},\textit{LS}_{2}\\}$,
$\textit{EE}=\\{\textit{EE}\\}$,
$\textit{LOS}=\\{\textit{LOS}_{1},\textit{LOS}_{2}\\}$,
$\textit{Exclusive}=\\{\textit{Exclusive}\\}$, and
$\textit{OE}=\\{\textit{OE}_{1},\textit{OE}_{2}\\}$,

  * •

$\textit{SAF}=\\{\textit{SAF}_{U}|U\subset
P\\}\\!\cup\\!\\{\textit{SAF}_{p_{x},U}|p_{x}{:}P,U\subset
P\\}\\!\cup\\!\\{\textit{SAF}^{\textit{undo}}_{p_{x},U}|p_{x}{:}P,U\subset
P\\}$,

  * •

and $\textit{LE}=\\{\textit{LE}_{U}|U\subseteq P\wedge U\neq\emptyset\\}$.

Note that the singleton sets, such as Free, contain a single state with the
same name as the set and do not contain themselves.

In the initial state of the implementation for $N$ threads, all substates are
set to Free, busy and forbidden map each thread $p$ to false and mtx is set to
false.

Since the state tuple contains a large number of elements, we use a shorthand
notation for writing down the resulting state. All elements which remain the
same are not listed and are abbreviated with “$\textit{etc}.$”. A substate or
the mtx variable being changed in the resulting state is denoted with the
“$=$” operator, where the lefthand side is assigned the value on the righthand
side, e.g. $d_{p}=\textit{ES}_{2}$ indicates that the substate of thread $p$
becomes $\textit{ES}_{2}$ in the next state. The function update $f[e\mapsto
n]$ specifies that in the next state $f(x)$ equals the new value $n$ if
$x\approx e$ and otherwise equals its original value.

We introduce the Invariants 5, 5, and 5. These exclude some unreachable states
and show that for any given state, the exact values of busy, forbidden, and
mtx can be inferred from just the set of substates, i.e.
$d_{p_{1}},d_{p_{2}},\ldots,d_{p_{N}}$. In the proof of Invariant 5, we show
that the value of mtx can be inferred from just the set of substates and that
it is not possible to have multiple threads simultaneously present in the set
of states fenced off by the mutex operations. We show that the values of the
busy and forbidden flags can also be inferred from just the set of substates
in the proofs of Invariants 5 and 5.

The exact proofs for these invariants can be found in the appendix [18]. All
of them follow the same general structure. Namely, the actions that result in
a thread entering or leaving the given set of states, e.g. $B$, are the exact
same actions that result in the value, e.g. $\textit{busy}(p)$, being altered.
And thus the exact values can be inferred from just the set of substates.

  * Invariant 1.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\exists p{:}P.~{}d_{p}\in M\Leftrightarrow\textit{mtx}\text{, and }\forall
p_{x},p_{y}{:}P.~{}d_{p_{x}},d_{p_{y}}\in M\Rightarrow p_{x}=p_{y}\text{,}$

where
$M=\textit{SAF}\cup\textit{LOS}\cup\textit{Exclusive}\cup\textit{LE}\cup\\{\textit{OE}_{2}\\}$.

  * Invariant 2.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\forall p{:}P.d_{p}\in B\Leftrightarrow\textit{busy}(p)\text{, where
}B=\textit{LOE}\cup\textit{Shared}\cup\\{\textit{ES}_{1},\textit{ES}_{4},\textit{LS}_{2}\\}\text{.}$

  * Invariant 3.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\forall p{:}P.\textit{forbidden}(p)\Longleftrightarrow\exists q{:}P.d_{q}\in
F\\!\text{,}$

where $F=\textit{LOS}\cup\textit{Exclusive}\cup\\{\textit{LE}_{U}|U\subset
P\wedge p\in U\\}\cup\\{\textit{SAF}_{U}|U\subset P\wedge p\in
U\\}\cup\\{\textit{SAF}_{p,U}|U\subset
P\\}\cup\\{\textit{SAF}_{p,U}^{\textit{undo}}|U\subset P\\}$.

##  6 Correctness of the busy-forbidden protocol

The state mapping, focus condition, state ordering and cone labeling used
during the equivalence proof are given in Definitions 7, 8, 9, and 10,
respectively. These data objects only need to use substates since the values
of the busy, forbidden, and mtx data objects can be directly inferred from the
substates in any given state.

###### Definition 7

We define our state-mapping $h:D_{N}\to D_{N}^{\prime}$ as follows:

$h(\langle
d_{1},d_{2},\ldots,d_{N},\textit{busy},\textit{forbidden},\textit{mtx}\rangle)=s\text{
where }s(p)=h_{P}(d_{p})\text{ for any }p{:}P\text{.}$

The mapping $h_{P}$, referred to as the substate-mapping, maps each substate
to the specification state with the same name as the set, shown in Definition
6, that it belongs to, e.g. $h_{P}(\textit{ES}_{3})=\textit{ES}$ and
$h_{P}(\textit{SAF}_{\\{p_{1},p_{3},p_{4}\\}})=\textit{SAF}$.

###### Definition 8

We define our focus condition $\textit{FC}:D_{N}\to\mathbb{B}$ as follows:

$\textit{FC}(\langle d_{p_{1}},d_{p_{2}},\ldots,d_{p_{N}},\textit{busy,
forbidden,
mtx}\rangle)=\bigwedge_{p_{x}{:}P}\textit{FC}_{p_{x}}(d_{p_{x}})\text{,}$

where
$\textit{FC}_{p_{x}}(d_{p_{x}})\overset{\scriptsize{\textit{def}}}{=}p_{x}\in\\{\textit{Free},\textit{ES}_{1},\textit{LOE,
Shared},\textit{LS}_{1},\textit{EE},\textit{SAF}_{\emptyset},\textit{LOS}_{1},\textit{Exclu-}\\\
\textit{sive},\textit{LE}_{\\{p_{x}\\}},\textit{OE}_{1}\\}$. We refer to the
predicate $\textit{FC}_{p_{x}}$, for any given $p_{x}{:}P$, as the sub-focus
condition.

###### Definition 9

Given two states $d=\langle
d_{p_{1}},d_{p_{2}},\ldots,d_{p_{N}},\textit{busy},\textit{forbidden},\textit{mtx}\rangle$
and $d^{\prime}=\langle d^{\prime}_{p1},d^{\prime}_{p2},\ldots,$
$d^{\prime}_{pN},\textit{busy}^{\prime},\textit{forbidden}^{\prime},\textit{mtx}^{\prime}\rangle$,
we define the ordering on these states as follows:

$d<_{M}d^{\prime}\overset{\textit{def}}{=}\bigwedge_{p{:}P}d_{p}<_{p}d_{p}^{\prime}\text{,}$

where, given some thread $p{:}P$, the ordering $<_{p}$ on its substates is
defined such that only the following holds:

  * •

$\textit{ES}_{1}<_{p}\textit{ES}_{2}<_{p}\textit{ES}_{3}<_{p}\textit{ES}_{4}$,
$\textit{LS}_{1}<_{p}\textit{LS}_{2}$,
$\textit{LOS}_{1}<_{p}\textit{LOS}_{2}$,
and $\textit{OE}_{1}<_{p}\textit{OE}_{2}$,

  * •

$\textit{SAF}_{p_{x},U}<_{p}\textit{SAF}_{U}$ iff $p_{x}\in U$ for any given
$U{:}\mathcal{P}(P)$ and $p_{x}{:}P$,
$\textit{SAF}_{U\setminus\\{p_{x}\\}}<_{p}\textit{SAF}_{p_{x},U}$ for any
given $U{:}\mathcal{P}(P)$ and $p_{x}{:}P$,
$\textit{SAF}_{U}<\textit{SAF}^{\textit{undo}}_{p_{x},U^{\prime}}$ for any
given given $U,U^{\prime}{:}\mathcal{P}(P)$ and $p_{x}{:}P$,

  * •

$\textit{LE}_{U}<_{p}\textit{LE}_{U^{\prime}}$ iff $U\subset U^{\prime}\wedge
p\in U$ or $p\in U\wedge p\not\in U^{\prime}$ for any given
$U,U^{\prime}{:}\mathcal{P}(P)$

###### Definition 10

We define the cone labeling $p:D^{\prime}_{N}\to\\{\Delta,\nabla\\}$ as
follows: Given any state $s{:}D_{N}^{\prime}$, $p(s)=\Delta$ iff $\exists
q{:}P.s(q)\in\\{\textit{SAF},\textit{LE}\\}\vee(\exists
q:P.s(q)=\textit{ES}\wedge\exists
q^{\prime}{:}P.q^{\prime}\in\\{\textit{LOS},\textit{Exclusive}\\})$ otherwise
$p(s)=\nabla$.

The specification indicates that if there is one thread in the ES node and one
thread in the SAF node, either one of them should be able to progress to the
next node. This is not simultaneously possible in the implementation, as
progressing to the LOE node requires the busy flag to be true and the
forbidden flag to be false, while progressing to the LOS node requires all
busy flags to be false and all forbidden flags to be true. Thus, the subfocus
point of each node is chosen such that the external actions are enabled
directly given that they would also be enabled in the specification, with the
exception of $\textit{SAF}_{\emptyset}$ which is used as the focus point of
the SAF node.

We show that there is a path of int actions from this to some state
$d_{\textit{int}}$ in which the transition to LOE is enabled. This is outlined
in Theorem 6.1 for which the proof is given in the appendix [18]. The general
idea behind the proof is that if the forbidden flag is set before it is read
by the thread in the ES node, the busy flag will be set back to false.
Repeating this, leads to all busy flags being false and all forbidden flags
being true, thus enabling the transition to LOE.

We now conclude by proving the implementation and specification of the busy-
forbidden protocol equivalent in Theorem 6.2.

###### Theorem 6.1

Given some state $d{:}D$, some thread $p_{\textit{SAF}}{:}P$, and some data
configuration $e_{\tau}{:}E_{\tau}$ such that $\textit{FC}(d)$ and
$c^{\prime}_{\tau}(h(d),e_{\tau})$ hold, $h(d)(p_{\textit{SAF}})=\textit{SAF}$
and $g^{\prime}_{\tau}(h(d),e_{\tau})=\textit{LOE}$. There must be some state
$d_{\textit{int}}{:}D$ such that
$d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}d_{\textit{int}}$ and
$c_{\tau}(d_{\textit{int}},e_{\tau})$ hold and
$h(g_{\tau}(d_{\textit{int}},e_{\tau}))(p_{\textit{SAF}})=\textit{LOE}$.

###### Theorem 6.2

The LPE of the implementation given in Table 10 and the LPE of the
specification given in Table 9 are divergence-preserving branching bisimilar.

Proof. To prove the aforementioned equivalence, we show that all ten
requirements given in Theorem 4.1 hold using Invariants 5, 5, and 5, and the
state mapping, focus condition, ordering and cone labeling, given in
Definitions 7, 8, 9, and 10, respectively. From the linear process equation,
it is relatively easy to see that Requirements I, II, V, VI,
I$\\!{}_{\Delta}$, and II$\\!{}_{\Delta}$ are not invalidated. As such, we
refer the reader to their extended proofs, found in the appendix [18].

Both the implementation and specification contain exactly three externally
observable actions that are not always enabled. For these actions, we show
that if the action in the specification is enabled, the same action is also
enabled in the corresponding focus point in the implementation, and if the
action in the implementation is enabled, the corresponding specification
action is also enabled, thus showing that Requirements III, and IV hold.

The first action is the $\text{load}(\textit{Forbidden}(p),\textit{false},p)$
action in $\textit{ES}_{2}$ and the $\tau$ transition from the ES to the LOE
node in the specification. The load action is only enabled when
$\textit{forbidden}(p)$ is false, and the $\tau$ transition in the
specification is only enabled if there are no threads in LOS or Exclusive
node. As per Invariant 5, these conditions hold exactly when they hold in the
corresponding focus points.

The second action is the $\text{lock}(p)$ action in EE and the $\tau$
transition in the EE node in the specification. The lock action is only
enabled when mtx is false, and the $\tau$ transition in the specification is
only enabled if there is no thread in the SAF, LOS, Exclusive, and LE node. As
per Invariant 5, these conditions, again, hold exactly when they would hold in
the corresponding focus points of the implementation.

The third action is the $\text{load}(\textit{Busy}(p_{x}),\textit{false},p)$
action in $\textit{SAF}_{p_{x},U}$ and the $\tau$ transition from the SAF to
the LOS node in the specification. The load action is only enabled when
$\textit{Busy}(p)$ is false and the $\tau$ transition is only enabled if there
is no thread in the LOE and Shared nodes. As per Invariant 5, if
$\textit{busy}(p)$ is false then the LOE and Shared node are empty and thus,
if the action is enabled in the implementation, it is also enabled in the
specification. As per the same invariant, the only focus points in which the
action would not be enabled while it would be in the corresponding
specifications state, are the ones in which a thread is in the SAF node, i.e.
some thread $p{:}P$ has the substate $\textit{SAF}_{\emptyset}$. In these
cases, as per Theorem 6.1, there must be some finite path of int actions to
some state $d_{\textit{int}}$ in which this action is enabled.

In the corresponding focus points for the SAF and LE cone, there is always at
least one internal action enabled. In the focus point for the ES cone, the
$\textit{load}(\textit{Forbidden}(p),\textit{true},p)$ action is enabled iff
$\textit{forbidden}(p)$ is true. As per Invariant 5, the only focus points in
which $\textit{Forbidden}(p)$ is true are the ones in which the LOS or
Exclusive node are occupied. In all other focus points, there are no further
internal actions enabled. Thus Requirement III$\\!{}_{\Delta}$ holds.

If a cone is labelled as non-diverging ($\nabla$), then each thread should be
in one of the following nodes: Free, LOE, Shared, LS, EE, LOS, Exclusive, or
OE, or ES, given that there are no threads present in either LOS or Exclusive.
With the exception of the
$\textit{load}(\textit{Forbidden}(p),\textit{true},p)$ action in the ES node,
all the internal actions within these nodes take us closer to a focus point.
As per Invariant 5, forbidden is true only if there is a thread present in
either the LOS or Exclusive, LE, or SAF node, which are known to be empty.
Thus Requirement IV$\\!{}_{\Delta}$ also holds and the implementation and
specification are divergence-preserving branching bisimilar as per Theorem
4.1. ∎

##  7 Conclusion and future work

We have extended the cones and foci proof framework [5, 8] with four
additional requirements, i.e. Requirements I$\\!{}_{\Delta}$,
II$\\!{}_{\Delta}$, III$\\!{}_{\Delta}$, and IV$\\!{}_{\Delta}$, such that it
can be used to prove divergence-preserving branching bisimulation. We have
proven this extension to be sound and have used it to prove the implementation
and specification of the novel busy-forbidden protocol [9] to be equivalent.

We note some opportunities to extend upon the work in this paper:

  * •

The completeness of the extended cones and foci proof framework has not been
formally proven. We assume its completeness due to the weakening of
Requirement III, and it is of similar interest as to whether this Requirement
can be made stronger without loss of our assumed completeness.

  * •

As mentioned before, the original cones and foci proof framework has been used
for the verification of the sliding window protocol [1]. The communication
channels used by this protocol are unreliable and thus allow divergence. As
such, the sliding window protocol could provide an interesting case study for
our extension of the cones and foci proof framework.

  * •

The diverging loops in the external behavior are considered to be improbable,
as such, we abstract away any actual, but potentially informative,
probabilistic analysis of the protocol.

## References

  * [1] Bahareh Badban et al.  “Verification of a sliding window protocol in $\mu$CRL and PVS”  In _FAC_ 17.3 Springer, 2005, pp. 342–388  DOI: 10.1007/s00165-005-0070-0
  * [2] J.C.M. Baeten and W.P. Weijland  “Process algebra” 18, Cambridge tracts in theoretical computer science  Cambridge University Press, 1990  DOI: 10.1017/CBO9780511624193
  * [3] Olav Bunte et al.  “The mCRL2 Toolset for Analysing Concurrent Systems”  In _Tools and Algorithms for the Construction and Analysis of Systems_ Cham: Springer International Publishing, 2019, pp. 21–39  DOI: 10.1007/978-3-030-17465-1˙2
  * [4] P.. Courtois, F. Heymans and D.. Parnas  “Concurrent Control with “Readers” and “Writers””  In _Commun. ACM_ 14.10 New York, NY, USA: Association for Computing Machinery, 1971, pp. 667–668  DOI: 10.1145/362759.362813
  * [5] W.J. Fokkink, J. Pang and J.C. van de Pol  “Cones and foci: A mechanical framework for protocol verification” DBLP:journals/fmsd/FokkinkPP06  In _Formal Methods in System Design_ 29.1 Springer Netherlands, 2006, pp. 1–31  DOI: 10.1007/s10703-006-0004-3
  * [6] Lars-åke Fredlund, Jan Friso Groote and Henri Korver  “Formal verification of a leader election protocol in process algebra”  In _Theoretical Computer Science_ 177.2, 1997, pp. 459–486  DOI: 10.1016/S0304-3975(96)00256-3
  * [7] Rob Glabbeek, Bas Luttik and Nikola Trcka  “Computation Tree Logic with Deadlock Detection”  In _Logical Methods in Computer Science_ Volume 5, Issue 4, 2009  DOI: 10.2168/LMCS-5(4:5)2009
  * [8] J.F. Groote and J. Springintveld  “Focus points and convergent process operators : a proof strategy for protocol verification”  In _Journal of Logic and Algebraic Programming_ 49 Elsevier, 2001, pp. 31–60  DOI: 10.1016/S1567-8326(01)00010-8
  * [9] Jan Friso Groote, Maurice Laveaux and P… Spaendonck  “A Thread-Safe Term Library”  In _Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles_ Cham: Springer International Publishing, 2022, pp. 422–459  DOI: 10.1007/978-3-031-19849-6˙25
  * [10] Jan Friso Groote and Mohammad Reza Mousavi  “Modeling and Analysis of Communicating Systems”  The MIT Press, 2014
  * [11] C… Hoare  “An Axiomatic Basis for Computer Programming”  In _Commun. ACM_ 12.10 New York, NY, USA: Association for Computing Machinery, 1969, pp. 576–580  DOI: 10.1145/363235.363259
  * [12] “IEEE Standard for a High Performance Serial Bus”  In _IEEE Std 1394-1995_ , 1996, pp. 1–384  DOI: 10.1109/IEEESTD.1996.81049
  * [13] Bas Luttik  “Divergence-preserving branching bisimilarity” Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, EXPRESS/SOS 2020 ; Conference date: 31-08-2020  In _EPTCS_ 322 Open Publishing Association, 2020, pp. 3–11  DOI: 10.4204/EPTCS.322.2
  * [14] R. Milner  “A Calculus of Communicating Systems” 92, LNCS  Springer, 1980  DOI: 10.1007/3-540-10235-3
  * [15] Susan Owicki and David Gries  “An axiomatic proof technique for parallel programs I”  In _Acta informatica_ 6.4 Springer, 1976, pp. 319–340  DOI: 10.1007/BF00268134
  * [16] Susan Owicki and David Gries  “Verifying properties of parallel programs: An axiomatic approach”  In _Communications of the ACM_ 19.5 ACM New York, NY, USA, 1976, pp. 279–285
  * [17] Carron Shankland and Mark Van Der Zwaag  “The tree identify protocol of IEEE 1394 in $\mu$CRL”  In _Formal Aspects of Computing_ 10.5 Springer, 1998, pp. 509–531
  * [18] P H M Spaendonck  “Verification of the busy-forbidden protocol (using an extension of the cones and foci framework)”, 2022  DOI: 10.48550/arxiv.2208.05334
  * [19] Yaroslav S Usenko  “Linearization of $\mu$CRL specifications”  In _Proc. 3rd Workshop on Verification and Computational Logic, Technical Report DSSE-TR-2002-5. Department of Electronics and Computer Science, University of Southampton_ , 2002  Citeseer

##  Appendix 0.A Process equations of the original implementation model

Tables 4, 5, 6, and 7 contain the process equations used to model a thread
$p{:}P$ calling the enter_shared, leave_shared, enter_exclusive, and
leave_exclusive functions, shown in Table 1, respectively. Table 8 contains
the process equation of a thread $p{:}P$ which repeatedly attempts to enter
and then leave either the shared or exclusive section by calling these
functions. Table 3 contains the process equations for modelling the busy and
forbidden flags and the mutex. The initial composition of these processes is
given in Table 10.

The $||$ operator models the parallel composition of processes and allows for
both the interleaving of actions as-well as for actions to occur in parallel.
The comm and allow operators are used to enforce that only the combinations of
actions, listed under the comm operation, can and must occur in parallel. This
enforces communication between the Thread processes and the Flags and Mutex
processes.

The linearization of the implementation, is shown in Table 10. With the
exception of this linearization, all process equations shown in Appendix 0.A
are taken from the original paper [9].

$\textbf{allow}(\\{$
---
$\textit{store},\textit{load},$
$\textit{lock},\textit{unlock},$
internal, improbable,
$\texttt{enter\\_shared\\_call},\texttt{enter\\_shared\\_return},$
$\texttt{leave\\_shared\\_call},\texttt{leave\\_shared\\_return},$
$\texttt{enter\\_exclusive\\_call},\texttt{enter\\_exclusive\\_return},$
$\texttt{leave\\_exclusive\\_call},\texttt{leave\\_exclusive\\_return}$
$\\},\textbf{comm}(\\{$
$\textit{store}_{f}|\textit{store}_{p}\rightarrow\textit{store},$
$\textit{load}_{f}|\textit{load}_{p}\rightarrow\textit{load},$
$\textit{lock}_{m}|\textit{lock}_{p}\rightarrow\textit{lock},$
$\textit{unlock}_{m}|\textit{unlock}_{p}\rightarrow\textit{unlock}$
$\\},$
$\textit{Thread}(p_{1})~{}||$
$\vdots$
$\textit{Thread}(p_{N})~{}||$
$\textit{Flags}(\lambda f{:}F.\textit{false})~{}||$
$\textit{Mutex}(\textit{false})$
$)$
$)$
Table 2: Parallel composition used to model the busy-forbidden protocol.
$\textit{Flags}(\textit{flags}:F\rightarrow\mathbb{B})=$
---
$\sum_{f{:}F,p{:}P}.($
$\sum_{b{:}\mathbb{B}}.\textit{store}_{f}(f,b,p)~{}\cdot~{}\textit{Flag}(\textit{flags}[f\mapsto
b])$
+$\textit{load}_{f}(f,\textit{flags}(f),p)~{}\cdot~{}\textit{Flag}(\textit{flags})$
$)$
$\textit{Mutex}(\textit{locked}:\mathbb{B})=$
$\sum_{p{:}P}.($
locked
$\rightarrow$$\textit{lock}_{m}(p)~{}\cdot~{}\textit{Mutex}(\textit{true})$
$\diamond$$\textit{unlock}_{m}(p)~{}\cdot~{}\textit{Mutex}(\textit{false})$
$)$
Table 3: Model of the components used during busy-forbidden.
$\textit{EnterShared}(p:P)=$
---
$\texttt{enter\\_shared\\_call}(p)~{}\cdot$
$\textit{TryBothFlags}(p)~{}\cdot$
$\texttt{enter\\_shared\\_return}(p)$
$\textit{TryBothFlags}(p:P)=$
$\textit{store}_{p}(\textit{Busy}(p),\textit{false},p)~{}\cdot~{}($
$\textit{load}_{p}(\textit{Forbidden}(p),~{}\textit{true},~{}p)~{}\cdot$
$\textit{store}_{p}(\textit{Busy}(p),\textit{false},p)~{}\cdot~{}\textit{improbable}~{}\cdot~{}\textit{TryBothFlags}(p)$
+$\textit{load}_{p}(\textit{Forbidden}(p),\textit{false},p)$
)
Table 4: Model of the enter_shared function shown in Table 1.
$\textit{LeaveShared}(p:P)=$
---
$\texttt{leave\\_shared\\_call}(p)~{}\cdot$
$\textit{store}_{p}(\textit{Busy}(p),\textit{false},p)~{}\cdot$
$\texttt{leave\\_shared\\_return}(p)$
Table 5: Model of the leave_shared shown in Table 1.
$\textit{EnterExclusive}(p:P)=$
---
$\texttt{enter\\_exclusive\\_call}(p)$
$\textit{lock}_{p}(p)~{}\cdot$
$\textit{SetAllForbiddenFlags}(p,~{}\emptyset)~{}\cdot$
$\texttt{enter\\_exclusive\\_return}(p)$
$\textit{SetAllForbiddenFlags}(p:P,~{}\textit{forbidden}:Set(P))=$
$(\forall_{p^{\prime}{:}P}.p\in\textit{forbidden})$
$\rightarrow$$internal$
$\diamond$$\sum_{p^{\prime}{:}P}.\textit{store}_{p}(\textit{Forbidden}(p^{\prime}),\textit{true},p)~{}\cdot~{}($
$\textit{load}_{p}(\textit{Busy}(p^{\prime}),\textit{false},p)~{}\cdot$
$\textit{SetAllForbiddenFlags}(p,~{}\textit{forbidden}\cup\\{p^{\prime}\\})$
+$l\textit{oad}_{p}(\textit{Busy}(p^{\prime}),\textit{true},p)~{}\cdot$
$\textit{store}_{p}(\textit{Forbidden}(p^{\prime}),\textit{false},p)~{}\cdot~{}\textit{improbable}~{}\cdot$
$\textit{SetAllForbiddenFlags}(p,~{}\textit{forbidden}\setminus\\{p^{\prime}\\})$
+$\textit{store}_{p}(\textit{Forbidden}(p^{\prime}),\textit{false},p)~{}\cdot~{}\textit{improbable}~{}\cdot$
$\textit{SetAllForbiddenFlags}(p,~{}\textit{forbidden}\setminus\\{p^{\prime}\\})$
$)$
Table 6: Model of the enter_exclusive function shown in Table 1.
$\textit{LeaveExclusive}(p:P)=$
---
$\texttt{leave\\_exclusive\\_call}(p)~{}\cdot$
$\textit{AllowAllThreads}(p,\emptyset)~{}\cdot$
$\textit{unlock}_{p}(p)~{}\cdot$
$\texttt{leave\\_exclusive\\_return}(p)$
$\textit{AllowAllThreads}(p:P,~{}\textit{allowed}:\textit{Set}(P))=$
$(\forall_{q{:}P}.q\in\textit{allowed})$
$\rightarrow$internal
$\diamond$$\sum_{p^{\prime}{:}P}.($
$\textit{store}_{p}(\textit{Forbidden}(p^{\prime}),\textit{false},p)~{}\cdot$
$\textit{AllowAllThreads}(p,~{}\textit{allowed}\cup\\{p^{\prime}\\})$
+$\textit{store}_{p}(\textit{Forbidden}(p^{\prime}),\textit{true},p)~{}\cdot~{}\textit{improbable}~{}$
$\textit{AllowAllThreads}(p,~{}\textit{allowed}\setminus\\{p^{\prime}\\})$
$)$
Table 7: Model of the leave_exclusive function shown in Table 1.
$\textit{Thread}(p:P)=$
---
$\textit{EnterShared}(p)~{}\cdot$
$\textit{LeaveShared}(p)~{}\cdot$
$\textit{Thread}(p)$
+$\textit{EnterExclusive}(p)~{}\cdot$
$\textit{LeaveExclusive}(p)~{}\cdot$
$\textit{Thread}(p)$
Table 8: Model of a thread p interacting with the protocol.
$\textit{BF}(s:P\rightarrow S)=$
---
$\sum_{p{:}P}(s(p)\approx\textit{Free})\to\texttt{enter\\_share\\_call}(p)\cdot\textit{BF}(s[p\mapsto\textit{ES}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{ES}\wedge\neg\exists
p^{\prime}{:}P.s(p)\in\\{\textit{LOS,
Exclusive}\\})\to\textit{improbable}\cdot\textit{BF}(s)$
$+$$\sum_{p{:}P}(s(p)\approx\textit{ES}\wedge\exists
p^{\prime}{:}P.s(p)\in\\{\textit{LOS,
Exclusive}\\})\to\tau\cdot\textit{BF}(s[p\mapsto\textit{LOE}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{LOE})\to\texttt{enter\\_shared\\_return}(p)\cdot\textit{BF}(s[p\mapsto\textit{Shared}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{Shared})\to\texttt{leave\\_shared\\_call}(p)\cdot\textit{BF}(s[p\mapsto\textit{LS}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{LS})\to\texttt{leave\\_shared\\_return}(p)\cdot\textit{BF}(s[p\mapsto\textit{Free}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{Free})\to\texttt{enter\\_exclusive\\_call}(p)\cdot\textit{BF}(s[p\mapsto\textit{EE}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{EE}\wedge\neg\exists
p^{\prime}{:}P.s(p^{\prime})\in\\{\textit{SAF, LOS,
Exclusive}\\})\to\tau\cdot\textit{BF}(s[p\mapsto\textit{SAF}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{SAF})\to\textit{improbable}\cdot\textit{BF}(s)$
$+$$\sum_{p{:}P}(s(p)\approx\textit{SAF}\wedge\neg\exists
p^{\prime}{:}P.s(p)\in\\{\textit{LOE,
Shared}\\})\to\tau\cdot\textit{BF}(s[p\mapsto\textit{LOS}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{LOS})\to\texttt{enter\\_exclusive\\_return}(p)\cdot\textit{BF}(s[p\mapsto\textit{Exclusive}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{Exclusive})\to\texttt{leave\\_exclusive\\_call}(p)\cdot\textit{BF}(s[p\mapsto\textit{LE}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{LE})\to\textit{improbable}\cdot\textit{BF}(s)$
$+$$\sum_{p{:}P}(s(p)\approx\textit{LE})\to\tau\cdot\textit{BF}(s[p\mapsto\textit{OE}])$
$+$$\sum_{p{:}P}(s(p)\approx\textit{OE})\to\texttt{leave\\_exclusive\\_return}(p)\cdot\textit{BF}(s[p\mapsto\textit{Free}])$
Table 9: Process equation of the external behavior as shown in Figure 1.
$\textit{BF}(d=\langle
d_{p_{1}},\ldots,d_{p_{N}},\textit{busy},\textit{forbidden},\textit{mutex}\rangle:D_{N})=$
---
$\sum_{p{:}P}(d_{p}\approx\textit{Free})\to\texttt{enter\\_shared\\_call}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{ES}_{2},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{Free})\to\texttt{enter\\_exclusive\\_call}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{EE},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{ES}_{2})\to\textit{store}(\textit{Busy}(p),\textit{true},p)\cdot\textit{BF}(\langle
d_{p}=\textit{ES}_{1},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{ES}_{1}\wedge\textit{forbidden}(p))$
$\to$$\textit{load}(\textit{Forbidden}(p),\textit{true},p)\cdot\textit{BF}(\langle
d_{p}=\textit{ES}_{4},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{ES}_{1}\wedge\neg\textit{forbidden}(p))$
$\to$$\text{load}(\textit{Forbidden}(p),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{LOE},\textit{etc}.\rangle)$
$+$$\sum_{p{:}P}(d_{p}\approx\textit{ES}_{4})\to\textit{store}(\textit{Busy}(p),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{ES}_{3},\textit{busy}[p\mapsto\textit{false}],\textit{etc}.\rangle\rangle$
$+$$\sum_{p{:}P}(d_{p}\approx\textit{ES}_{3})\to\textit{improbable}\cdot\textit{BF}(\langle
d_{p}=\textit{ES}_{2},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{LOE})\to\texttt{enter\\_shared\\_return}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{Shared},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{Shared})\to\texttt{leave\\_shared\\_call}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{LS}_{2},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{LS}_{2})\to\textit{store}(\textit{Busy}(p),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{LS}_{1},\textit{busy}[p\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{LS}_{1})\to\texttt{leave\\_shared\\_return}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{EE},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{EE}\wedge\neg\textit{mutex})\to\text{lock}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{SAF}_{\emptyset},\textit{mtx}=\textit{true},\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}_{U})$
$\to$$\textit{store}(\textit{Forbidden}(p_{x}),\textit{true},p)\cdot\textit{BF}(\langle
d_{p}=\textit{SAF}_{p_{x},U},\textit{forbidden}[p_{x}\mapsto\textit{true}],\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}_{p_{x},U}\wedge\textit{busy}(p_{x}))$
$\to$$\textit{load}(\textit{Busy}(p_{x}),\textit{true},p)\cdot\textit{BF}(\langle
d_{p}=\textit{SAF}_{p_{x},U}^{\textit{undo}},\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}_{p_{x},U}\wedge
P\setminus\\{p_{x}\\}\approx U\wedge\neg\textit{busy}(p_{x}))$
$\to$$\text{load}(\textit{Busy}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{LOS}_{2},\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}_{p_{x},U}\wedge
P\setminus\\{p_{x}\\}\not\approx U\wedge\neg\textit{busy}(p_{x}))$
$\to$$\textit{load}(\textit{Busy}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{SAF}_{U\cup\\{p_{x}\\}},\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}_{p_{x},U})$
$\to$$\textit{store}(\textit{Forbidden}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}{=}\textit{SAF}_{U\setminus\\{p_{x}\\}},\textit{forbidden}[p_{x}\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{SAF}^{\textit{undo}}_{p_{x},U})$
$\to$$\textit{store}(\textit{Forbidden}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}{=}\textit{SAF}_{U\setminus\\{p_{x}\\}},\textit{forbidden}[p_{x}\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{LOS}_{2})\to\textit{internal}\cdot\textit{BF}(\langle
d_{p}=\textit{LOS}_{1},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{LOS}_{1})\to\texttt{enter\\_exclusive\\_return}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{Exclusive},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{Exclusive})\to\texttt{leave\\_exclusive\\_call}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{LE}_{P},\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{LE}_{U}\wedge
U\approx\\{p_{x}\\})$
$\to$$\text{store}(\textit{Forbidden}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{OE}_{1},\textit{forbidden}[p_{x}\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{LE}_{U}\wedge
U\not\approx\\{p_{x}\\})$
$\to$$\textit{store}(\textit{Forbidden}(p_{x}),\textit{false},p)\cdot\textit{BF}(\langle
d_{p}=\textit{LE}_{U\setminus\\{p_{x}\\}},\textit{forbidden}[p_{x}\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p,p_{x}{:}P,U{:}\mathcal{P}(P)}(d_{p}\approx\textit{LE}_{U})$
$\to$$\textit{store}(\textit{Forbidden}(p_{x}),\textit{true},p)\cdot\textit{BF}(\langle
d_{p}=\textit{LE}_{U\cup\\{p_{x}\\}},\textit{forbidden}[p_{x}\mapsto\textit{false}],\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{OE}_{2})\to\textit{unlock}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{OE}_{1},\textit{mtx}=\textit{false},\textit{etc}.\rangle)$
+$\sum_{p{:}P}(d_{p}\approx\textit{OE}_{1})\to\texttt{leave\\_exclusive\\_return}(p)\cdot\textit{BF}(\langle
d_{p}=\textit{Free},\textit{etc}.\rangle)$
Table 10: Linear process equation of the busy-forbidden implementation.

##  Appendix 0.B Linear process equations of the busy-forbidden protocol

Table 9 contains the linear process equation of the externally visible
behaviour of the busy-forbidden protocol.

##  Appendix 0.C Proofs of invariants and reachable states

In this section of the appendix, we give the explicit proofs of the invariants
shown in Section 5. We also provide the proof of Theorem 6.1, in which we show
that: Given a state $d:D$ in which a thread is present in the SAF node and
such that the focus condition holds and the transition from SAF to LOE is
enabled in the specification. There must be some finite path of $int$ actions
from this state to a state $d_{\textit{int}}$ in which the aforementioned
action to the LOE node is enabled.

  * Invariant 1.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\exists p{:}P.~{}d_{p}\in M\Leftrightarrow\textit{mtx}\text{, and }\forall
p_{x},p_{y}{:}P.~{}d_{p_{x}},d_{p_{y}}\in M\Rightarrow p_{x}=p_{y}\text{ where
}$
$M=\textit{SAF}\cup\textit{LOS}\cup\textit{Exclusive}\cup\textit{LE}\cup\\{\textit{OE}_{1}\\}$

Proof. This invariant holds in the initial state as all substates are
initially set to Free and mtx is set to false.

Consider some state $d{:}D$ in which the invariant holds and no thread is
present in the given set of substates $M$. A thread can only enter this set
through the $\textit{lock}(p)$ action in EE. This is also the only action that
results in mtx being set to true, thus the invariant will also hold in each
subsequent state of $d$ given that no thread is present in $M$.

Now consider some state $d\textit{:}D$ in which the invariant holds and a
(single) thread is present in the given set of substates MTX. A thread con
only leave this set through the $\textit{unlock}(p)$ action in
$\textit{OE}_{1}$. This is also the only action that results in mtx being set
to false, thus the invariant will hold in all subsequent states of $d$. ∎

  * Invariant 2.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\forall p{:}P.d_{p}\in B\Leftrightarrow\textit{busy}(p)\text{ where
}B=\textit{LOE}\cup\textit{Shared}\cup\\{\textit{ES}_{2},\textit{ES}_{3},\textit{LS}_{1}\\}\text{.}$

Proof. This invariant holds in the initial state as all substates are
initially set to Free and busy initially maps each thread $p$ to false.

Consider some state $d{:}D$ in which the invariant holds. A thread $p$ can
only enter the set of substates $B$ through the
$\textit{store}(\textit{Busy}(p),\textit{true},p)$ action in
$\textit{ES}_{1}$. This is the only action that results in busy mapping $p$ to
true. Thus if there is no thread present in the set of substates $B$, the
invariant will also hold after each enabled action. Similarly, a thread $p$
can only leave the set of substates $B$ through the
$\textit{store}(\textit{Busy}(p),\textit{false},p)$ action in either
$\textit{ES}_{3}$ or $\textit{LS}_{1}$, which are the only actions that result
in busy mapping $p$ to false. Thus if the invariant holds in some state
$d{:}D$, it also holds in all subsequent states. ∎

  * Invariant 3.  The following invariant holds in the initial state and all subsequent states of the implementation: Given any state $d{:}D$ as per Definition 5,

$\forall p{:}P.\textit{forbidden}(p)\Longleftrightarrow\exists q{:}P.d_{q}\in
F\text{,}$

where $F=\textit{LOS}\cup\textit{Exclusive}\cup\\{\textit{LE}_{U}|U\subset
P\wedge p\in U\\}\cup\\{\textit{SAF}_{U}|U\subset P\wedge p\in
U\\}\cup\\{\textit{SAF}_{p,U}|U\subset
P\\}\cup\\{\textit{SAF}_{p,U}^{\textit{undo}}|U\subset P\\}$.

Proof. The invariant holds in the initial state as all substates are initially
set to Free and forbidden initially maps each thread $p$ to false.

Consider some state $d{:}D$ in which the invariant holds. The set of substates
$F$ is a subset of $M$, given in Invariant 5, and thus there can be at most
$1$ thread present in $F$. The only action that results in forbidden mapping
$p$ to true is the $\textit{store}(\textit{Forbidden}(p),\textit{true},q)$
action that is enabled in the states $\textit{SAF}_{U}$ and $\textit{LE}_{U}$.
This is also the only action that results in some thread $q$ entering $F$.
Thus if there is no thread present in $F$, the invariant will also hold after
each enabled action. Similarly, a thread $q$ can only leave $F$ through the
$\textit{store}(\textit{Forbidden}(p),\textit{false},q)$ action in
$\textit{SAF}_{p,U}$, $\textit{SAF}_{p,U}^{\textit{undo}}$, and
$\textit{LE}_{U}$, which are the only actions that result in forbidden mapping
$p$ to false. Thus if the invariant holds in $d$, it also holds in all
subsequent states. ∎

###### Theorem 0.C.2

Given some state $d{:}D$, some thread $p_{\textit{SAF}}{:}P$, and some data
configuration $e_{\tau}{:}E_{\tau}$ such that $\textit{FC}(d)$ and
$c^{\prime}_{\tau}(h(d),e_{\tau})$ hold, $h(d)(p_{\textit{SAF}}=\textit{SAF}$
and $g^{\prime}_{\tau}(h(d),e_{\tau})=\textit{LOE}$. There must be some state
$d_{\textit{int}}{:}D$ such that
$d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}d_{\textit{int}}$ and
$c_{\tau}(d_{\textit{int}},e_{\tau})$ hold and
$h(g_{\tau}(d_{\textit{int}},e_{\tau}))(p_{\textit{SAF}})=\textit{LOE}$.

Proof. We define the state $\textit{aux}_{U}(d)=\langle
d_{1}^{\prime},\ldots,d_{N}^{\prime},\textit{busy}^{\prime},\textit{forbidden}^{\prime},\textit{mutex}^{\prime}\rangle$,
for any given subset of tread $U\subset P$, such that for all $p{:}P$ we have:

$\displaystyle d_{p}^{\prime}=\textit{ES}_{1}$ $\displaystyle\text{ iff
}d_{p}\in\textit{ES}\wedge d_{p}\in U$ $\displaystyle
d_{p}^{\prime}=\textit{ES}_{2}$ $\displaystyle\text{ iff
}d_{p}\in\textit{ES}\wedge d_{p}\not\in U$ $\displaystyle
d_{p}^{\prime}=\textit{SAF}_{U}$ $\displaystyle\text{ iff
}d_{p}\in\textit{SAF}$ $\displaystyle d_{p}^{\prime}=d_{p}$ otherwise

The values of $\textit{busy}^{\prime}$, $\textit{forbidden}^{\prime}$, and
$\textit{mutex}^{\prime}$ can be inferred from
$d_{p_{1}}^{\prime},\ldots,d_{p_{N}}^{\prime}$ as per the invariants.

We show that
$d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}\textit{aux}_{U}(d)$ holds
for any given $U\subset P$ using induction over $U$. For the base-case,
$U=\emptyset$, we have $d=\textit{aux}_{\emptyset}$. Now take any $U\subset P$
such that $d=_{\textit{int}}\textit{aux}_{U}(d)$ and any $p{:}P$ such that
$p\not\in U$ and $U\cup\\{p\\}\subset P$. We show that
$\textit{aux}_{U}(d)=_{\textit{int}}\textit{aux}_{U\cup\\{p\\}}(d)$. Take
$p_{\textit{SAF}}{:}P$ such that $d_{p_{\textit{SAF}}}=\textit{SAF}_{U}$. If
$d_{p}\in\textit{ES}$, then the sequence of actions
$\textit{store}(\textit{Forbidden}(p),\textit{true},p_{\textit{SAF}})\cdot$
$\textit{load}(\textit{Forbidden}(p),\textit{true},p)\cdot$
$\textit{store}(\textit{Busy}(p),\textit{false},p)\cdot$
$\textit{load}(\textit{Busy}(p),\textit{false},p_{\textit{SAF}})$
takes us from $\textit{aux}_{U}(d)$ to $\textit{aux}_{U\cup\\{p\\}}(d)$. If
$p\not\in\textit{ES}$, then the sequence of actions $\textit{store}($
$\textit{Forbidden}(p),$ $\textit{true},$
$p_{\textit{SAF}})\cdot\textit{load}(\textit{Busy}(p),$
$\textit{false},p_{\textit{SAF}})$ takes us from $\textit{aux}_{U}(d)$ to
$\textit{aux}_{U\cup\\{p\\}}(d)$. As the relation
${\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}$ is transitive, it follows
that $d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}\textit{aux}_{U}(d)$
for any given $U\subset P$.

We have thus shown that if we take $U=P\setminus\\{p_{\textit{SAF}}\\}$ such
that $p_{\textit{SAF}}\in\textit{SAF}$, we have
$d{\xrightarrow{\scriptsize{\textit{int}}}}\\!^{*}\textit{aux}_{U}(d)$, from
which we can take a single int action, i.e.
$\textit{store}(\textit{Forbidden}(p_{\textit{SAF}}),$
$\textit{true},p_{\textit{SAF}})$, after which the transition to the LOE node
will be enabled. ∎

##  Appendix 0.D Detailed equivalence proof

We give a more detailed version of the equivalence proof shown in the main
paper.

###### Theorem 0.D.1

The LPE of the implementation given in Table 10 and the LPE of the
specification given in Table 9 are divergence-preserving branching bisimilar.

Proof. We show that all ten requirements given in Theorem 4.1 hold using
Invariants 5, 5, and 5, and the state mapping, focus condition, ordering and
cone labeling, given in Definitions 7, 8, 9, and 10, respectively. And thus
the implementation and specification are divergence-preserving branching
bisimilar.

Requirement I holds since for each substate that does not satisfy the sub-
focus condition, at least one internal action with a smaller endpoint, is
always enabled. We can see that none of the int actions in the implementation,
i.e. italicized actions in Table 10, have an endpoint that is in a different
cone then their beginpoint. Thus, Requirement II also holds.

Both the implementation and specification contain exactly three externally
visible actions that are not always enabled. We show that if the action in the
implementation is enabled, the action in the specification is also enabled,
thus showing that Requirement IV holds. Simultaneously, we show that if an
action in the specification is enabled, the same action is also enabled in the
corresponding focus point in the implementation, thus showing that Requirement
III holds.

The first action is the $\text{load}(\textit{Forbidden}(p),\textit{false},p)$
action in $\textit{ES}_{2}$ and the $\tau$ transition from the ES to the LOE
node in the specification. The load action is only enabled when
$\textit{forbidden}(p)$ is false, and the $\tau$ transition in the
specification is only enabled if there are no threads in LOS or Exclusive
node. As per Invariant 5, $\textit{forbidden}(p)$ is true iff there is a
thread present in one of these nodes, and thus when the transition is not
enabled in the specification it is also not enabled in the implementation. As
per the same invariant, if the action is enabled in the specification it is
also enabled in all corresponding focus points.
The second action is the $\text{lock}(p)$ action in EE and the $\tau$
transition in the EE node in the specification. The lock action is only
enabled when mtx is false, and the $\tau$ transition in the specification is
only enabled if there is no thread in the SAF, LOS, Exclusive, and LE node. As
per Invariant 5, if mtx is false iff there is no thread in any of the states
belonging to the aforementioned nodes or in the $\textit{OE}_{1}$ substate.
Thus, if the action is enabled in the implementation it is also enabled in the
specification. Because the focus condition does not hold in $\textit{OE}_{1}$,
we have that if the action is enabled in the specification, it is also enabled
in the corresponding focus point in the implementation.
The third action is the $\text{load}(\textit{Busy}(p_{x}),\textit{false},p)$
action in $\textit{SAF}_{p_{x},U}$ and the $\tau$ transition from the SAF to
the LOS node in the specification. The load action is only enabled when
$\textit{Busy}(p)$ is false and the $\tau$ transition is only enabled if there
is no thread in the LOE and Shared nodes. As per Invariant 5, if
$\textit{busy}(p)$ is false then the LOE and Shared node are empty and thus,
if the action is enabled in the implementation, it is also enabled in the
specification. As per the same invariant, the only focus points in which the
action would not be enabled while it would be in the corresponding
specifications state, are the ones in which a thread is in the SAF node, i.e.
some thread $p{:}P$ has the substate $\textit{SAF}_{\emptyset}$. In these
cases, as per Theorem 6.1,there must be some finite path of int actions to
some state $d_{\textit{int}}$ in which this action is enabled. The only
visible actions with parameters are the eight
enter/leave_shared/exclusive_call/return actions. We can thus quickly see that
the parameters of these actions match and Requirement V holds.
Similarly, it should be clear from the linear process equations that the
endpoints of all externally visible transitions are also related and thus
Requirement VI is also met. Requirement II$\\!{}_{\Delta}$ holds, as the cone
labeling $p$ labels a cone as divergent exactly when one of the three
improbable loops would be enabled in the specification.
In the corresponding focus points for the SAF and LE cone, there is always at
least one internal action enabled. In the focus point for the ES cone, the
$\textit{load}(\textit{Forbidden}(p),\textit{true},p)$ action is enabled iff
$\textit{forbidden}(p)$ is true. As per Invariant 5, the only focus points in
which $\textit{Forbidden}(p)$ is true are the ones in which the LOS or
Exclusive node are occupied. In all other focus points, there are no further
internal actions enabled. Thus Requirement III$\\!{}_{\Delta}$ holds.
If a cone is labelled as non-diverging ($\nabla$), then each thread should be
in one of the following nodes: Free, LOE, Shared, LS, EE, LOS, Exclusive, or
OE, or ES, given that there are no threads present in either LOS or Exclusive.
With the exception of the
$\textit{load}(\textit{Forbidden}(p),\textit{true},p)$ action in the ES node,
all the internal actions within these nodes take us closer to a focus point.
As per Invariant 5, forbidden is true only if there is a thread present in
either the LOS or Exclusive, LE, or SAF node, which are known to be empty.
Thus Requirement IV$\\!{}_{\Delta}$ also holds and the implementation and
specification are divergence-preserving branching bisimilar as per Theorem
4.1. ∎