Keywords

1 Introduction

The readers-writer lock problem is a concurrency problem introduced and solved by Courtois et al. [5]. 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 [4], 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 [12], 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 [11] by Groote and Springintveld and later generalized by Fokkink et al. in [6]. 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 [2], a complex leader election protocol in [7], and a part of the IEEE P1394 high-speed bus protocol [1] 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 [8]. 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 \(\textit{false}\). The mutex, called mutex, enforces exclusive access to the writer section.

Table 1. Pseudocode description of the busy-forbidden protocol
Full size table

When entering the readers section, a thread sets its busy flag and enters iff its forbidden flag is \(\textit{false}\). If the forbidden flag is \(\textit{true}\), the busy flag is set back to \(\textit{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 \(\textit{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 \(\textit{false}\). The writer section is entered once all forbidden flags are \(\textit{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 \(\textit{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 Fig. 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 \(\textit{forbidden}\) flag is \(\textit{true}\). As repeatedly checking the flag is discouraged through the timed_lock call, the internal loop is labeled as improbable. When the \(\textit{forbidden}\) flag is evaluated to \(\textit{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.

Fig. 1.
figure 1

The external behaviour

Full size image

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 \(\textit{false}\); this transition is labeled as improbable as this only rarely occurs. Once the last \(\textit{busy}\) flag is evaluated to \(\textit{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 \(\textit{true}\) when releasing the lock, this transition is also labeled as improbable. Once the last forbidden flag is set to \(\textit{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 [3] 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 \(\textit{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) \rightarrow a(f_a(d,e_a)) \cdot X(g_a(d,e_a)) \text {,}$$

where D is the set of states, \(\textit{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' \in D\), and action l, we define the following relations:

  • \(d \xrightarrow {l} d'\) 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'\).

  • \(d \xrightarrow {l}\!\!\!^* d'\) iff there is a finite sequence of states \(d_0, \ldots , d_k\) such that \(d_0 = d\), \(d_k = d'\) and for all \(0 \le 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'\). A relation R on the states \(D \times D'\) is a divergence-preserving branching bisimulation iff the following conditions for all states \(s \in D\), \(t\in D'\), and actions \(\textit{l} \in \textit{Act}\) hold:

  • (\({B}_1\)) If sRt and \(s \xrightarrow {l} s'\) for some state \(s'\in D\), then either \(l = \tau \) and \(s' R t\), or there are states \(t', t'' \in D'\) such that \(t \xrightarrow {\tau }\!^* t' \xrightarrow {l} t''\), \(s R t'\), and \(s' R t''\).

  • (\({B}_2\)) If sRt and \(t \xrightarrow {l} t'\) for some state \(t'\in D'\), then either \(l = \tau \) and \(s R t'\), or there are states \(s', s'' \in D\) such that \(s \xrightarrow {\tau }\!^* s' \xrightarrow {l} s''\), \(s' R t\), and \(s'' R t\).

  • (\({D}_1\)) If \(s R\, 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 }{\rightarrow }s_{k+1}\) and \(s_k R\, t\) for all \(k \in \mathbb {N}\), then there is a state \(t' \in D'\) such that \(t \overset{\tau }{\rightarrow }\ t'\), and \(s_k R\, t'\) for some \(k\in \mathbb {N}\).

  • (\({D}_2\)) If \(s R\, 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 }{\rightarrow }t_{k+1}\) and \(s R\, t_k\) for all \(k \in \mathbb {N}\), then there is a state \(s' \in D\) such that \(s \overset{\tau }{\rightarrow }\ s'\), and \(s' R\, t_k\) for some \(k\in \mathbb {N}\).

Two clustered LPEs with respective initial states \(d_0\) and \(d_0'\) are divergence-preserving branching bisimilar iff there is a divergence-preserving branching bisimulation R such that \(d_0 R\, d_0'\).

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

In [11], it is noted that in communicating systems, equivalent states often have a “cone-like” structure as is shown in Fig. 2. In this figure, equivalent states are grouped together in the cone C. In the focus point state \(\textit{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 \(\textit{fc}\). We show one such path for the state d, using the dashed arrows.

Fig. 2.
figure 2

A cone C with focus point fc

Full size image

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 \rightarrow D'\) that maps states in the implementation to their equivalent state in the specification, a focus condition \(\textit{FC} : D \rightarrow \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 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 \(\textit{int} \) actions.

Theorem 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'\),

$$Y(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 Y(g_a'(d', e_a)) \text {.}$$

The LPEs X and Y are divergence-preserving branching bismilar if there is a state mapping \(h: D \rightarrow D'\), a focus condition \(\textit{FC} : D \rightarrow \mathbb {B}\), a well founded ordering \(<_M\) on D, and a cone labeling \(p : D' \rightarrow \{\Delta , \nabla \}\) such that \(h(d_0) = d_0'\) 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:

    $$(\lnot \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'(h(d), e_a)) \Rightarrow (\exists d_{\textit{int}}{:}D. d {\xrightarrow {{\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'(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'_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'(h(d), e_a)$$
I\(_\Delta \):

Any internal action in the specification is part of an \(\textit{int} \)-loop:

$$\begin{aligned} \forall _{e_{\textit{int}}}{:}E_{\textit{int}}.c_{\textit{int}}'(h(d), e_{\textit{int}}) \Rightarrow g_{\textit{int}}'(h(d), e_{\textit{int}}) = h(d) \end{aligned}$$
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'_{\textit{int}}(h(d),e_{\textit{int}}))$$
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}}))$$
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'\) 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 [6], and [11]. We give a concise proof sketch.

Condition \(\textit{B}_1\). Consider the states \(d,d'{:}D\), and label \(l{:}{} \textit{Act}\cup \{\textit{int} \}\) such that \(d\overset{a}{\rightarrow }d'\). As per Requirement II , if \(l=\textit{int} \) then \(h(d) = h(d')\). If \(l\ne \textit{int} \), then we have \(h(d)\overset{l}{\rightarrow }h(d')\) as per Requirement IV , and VI.

Condition \(\textit{B}_2\). Consider the states \(d{:}D, d'_2{:}D'\), and label \(l{:}{} \textit{Act}\cup \{\textit{int} \}\) such that \(h(d) \overset{l}{\rightarrow }\ d_2'\). If \(l=\textit{int} \), then \(h(d_2') = h(d)\), as per Requirement I\(_\Delta \) . If \(l\ne \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}{\rightarrow }\ d_4\) and \(h(d_4) = d_2'\). From Requirement II follows that all states along the \(\textit{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 {{\textit{int}}}} d_{n+1}\). We show that there is some \(e_{\textit{int}}{:}E_{\textit{int}}\) such that \(c'_{\textit{int}}(h(d),e_{\textit{int}})\) and \(g'_{\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'_n)_{n\in \mathbb {N}}\) over states in \(D'\) such that \(d'_0 = h(d)\) and for any \(n\in \mathbb {N}\) we have \(d~R~d'_n\), i.e. \(d'_n = h(d)\), and \(d'_n {\xrightarrow {{\textit{int}}}} d'_{n+1}\).

Since h(d) allows an \(\texttt {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.   \(\square \)

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 Sect. 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 Fig. 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'_N\). Note that each condition in the specification is the same as the conditions shown in Fig. 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

$$\begin{aligned} d = \langle d_{p_1}, d_{p_2}, \ldots , d_{p_N}, \textit{busy}, \textit{forbidden}, \textit{mtx}\rangle {:} D_N\text {, in which:} \end{aligned}$$

  • \(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 \(\textit{busy}\) mapping.

  • \(\textit{mtx}\) is a boolean that indicates whether the mutual exclusion variable \(\textit{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 \ne \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 \(\textit{false}\) and mtx is set to \(\textit{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 1, 2, and 3. 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 1, 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 2 and 3.

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 \rightarrow D_N'\) 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 \rightarrow \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{{\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' = \langle d'_{p1}, d'_{p2}, \ldots ,\) \( d'_{pN}, \textit{busy}', \textit{forbidden}', \textit{mtx}' \rangle \), we define the ordering on these states as follows:

$$d<_M d' \overset{\textit{def}}{=} \bigwedge _{p{:}P} d_p <_p d_p' \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'}\) for any given given \(U,U'{:}\mathcal {P}(P)\) and \(p_x{:}P\),

  • \(\textit{LE}_U <_p \textit{LE}_{U'}\) iff \(U \subset U' \wedge p \in U\) or \(p \in U \wedge p\not \in U'\) for any given \(U,U'{:}\mathcal {P}(P)\)

Definition 10

We define the cone labeling \(p : D'_N \rightarrow \{\Delta , \nabla \}\) as follows: Given any state \(s {:} D_N'\), \(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'{:}P. q' \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 \(\textit{true}\) and the forbidden flag to be \(\textit{false}\), while progressing to the LOS node requires all busy flags to be false and all forbidden flags to be \(\textit{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 2 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 \(\textit{false}\) and all forbidden flags being \(\textit{true}\), thus enabling the transition to LOE.

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

Theorem 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'_\tau (h(d), e_\tau )\) hold, \(h(d)(p_{\textit{SAF}}) = \textit{SAF}\) and \(g'_\tau (h(d), e_\tau ) = \textit{LOE}\). There must be some state \(d_{\textit{int}}{:}D\) such that \(d {\xrightarrow {{\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 3

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 1 hold using Invariants 1, 2, and 3, 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 \(\textit{false}\), and the \(\tau \) transition in the specification is only enabled if there are no threads in LOS or Exclusive node. As per Invariant 3, 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 \(\textit{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 1, 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 \(\textit{false}\) and the \(\tau \) transition is only enabled if there is no thread in the LOE and Shared nodes. As per Invariant 2, if \(\textit{busy}(p)\) is \(\textit{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 2, 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 \(\textit{true}\). As per Invariant 3, the only focus points in which \(\textit{Forbidden}(p)\) is \(\textit{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 3, forbidden is \(\textit{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 1.    \(\square \)

7 Conclusion and Future Work

We have extended the cones and foci proof framework [6, 11] 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 [2]. 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.