ec${}_{2}$}.(c_{1}.\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{2}$}.\bar{d_{2}}.Y+\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{2}$}.(c_{1}.\bar{d_{2}}.Y+\bar{d_{2}}.X))\end{array}$

$\scriptscriptstyle X$$\scriptscriptstyle X$ln1$\scriptscriptstyle
Y$$\tau_{c1}$ec1lc1$\tau_{d1}$en1$\scriptscriptstyle X$ ln2$\scriptscriptstyle
Z$$\hskip 18.0pt\tau_{c2}$ ec2 lc2$\hskip 18.0pt\tau_{d2}$
en2$\scriptscriptstyle X$ ln2ln1$\scriptscriptstyle Y$ ln2$\tau_{c1}$ ln2ec1
ln2lc1 ln2$\tau_{d1}$en1$\scriptscriptstyle
Z$ln1$\tau_{c1}$$\tau_{c1}$ec1ec2$\hskip 18.0pt\tau_{c2}$$\hskip
18.0pt\tau_{c2}$lc1$\hskip 18.0pt\tau_{c2}$$\tau_{d1}$$\hskip
18.0pt\tau_{c2}$en1ln1 ec2$\tau_{c1}$ln1 lc2$\tau_{c1}$ lc2ln1$\hskip
18.0pt\tau_{d2}$$\tau_{c1}$$\hskip 18.0pt\tau_{d2}$ en2 en2

Figure 4. Encapsulated gatekeeper

This mutual exclusion protocol satisfies ME 6J, for as soon as eni has
occurred (and in the initial state) Process $I_{i}$ is in its initial state
$\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{i}$}.\bar{c_{i}}.I_{i}$, and nothing stands in the way of the action
lni. In other words, justness is a strong enough assumption for lni to occur.
Clearly, the protocol also satisfies ME 1 and 2, as well as ME 4Pr and 5Pr.
The only downside is that it takes weak fairness to achieve ME 3, starvation-
freedom. This assumption is needed to assure that the synchronisation between
actions $\bar{c_{i}}$ and $c_{i}$ will actually occur.

Intuitively, the encapsulated gatekeeper is an equally unacceptable mutual
exclusion protocol as the gatekeeper, for the input interface ought to make no
difference. This shows that weak fairness in any dimension of Figure 3 is too
strong an assumption. However, due to the impossibility result of [GH15b], the
two remaining entries of Figure 3 cannot be realised in CCS. Theoretically,
that result leaves open the possibility of achieving justness in both the
dimensions “request” and “granting”, at the expense of assuming weak fairness
for ME 4 or 5. I do not think this is actually possible, and even if it were,
a solution that requires weak fairness to escape the critical section, or to
enter the noncritical one, appears equally unacceptable as the (encapsulated)
gatekeeper.

##  Part III Impossibility Results for Peterson’s Mutual Exclusion Algorithm

Here I recall three impossibility results for mutual exclusion protocols that
have been shown or claimed earlier, and illustrate or substantiate them for
Peterson’s mutual exclusion protocol. I could have equally well done this for
another mutual exclusion protocol, such as Lamport’s bakery algorithm [Lam74],
Szymański’s mutual exclusion algorithm [Szy88] or the _round-robin_
scheduler.101010As a mutual exclusion protocol, the round-robin is a central
scheduler that grants access to the critical section to $N$ processes numbered
$1-N$ by cycling through all competing processes in the order $1-N$. Each time
it is the turn of Process $i$, the round-robin scheduler checks whether
Process $i$ wants to enter the critical section, and if so, grants access.
When Process $i$ leaves the critical section, or if it didn’t want to enter,
it will be the turn of Process $i{+}1$ mod $N$. When confronted with the claim
that under some natural assumptions no correct mutual exclusion protocols
exist, some people reply that in that case one could always use a round-robin
scheduler, as if this somehow constitutes an exception. My reason for choosing
Peterson’s protocol in this paper is that it is (one of) the simplest of all
mutual exclusion protocols.

The first impossibility result stems from [Vog02, KW97, GH15b], and says that
in Petri nets, and in CCS and similar process algebras, it is not possible to
model a mutual exclusion protocol in such a way that it is correct without
making an assumption as strong as weak fairness. In [Vog02] this is shown for
finite Petri nets, and in [KW97] for a class of Petri nets that interact with
their environment through an interface of a particular shape, similar to the
one of Section 15. In [GH15b] the same is shown for all structural conflict
nets (and thus for all safe nets), as well as for the process algebra CCS,
with strong hints on how the result extends to many similar process algebras.
For the latter result, either the concurrency relation between CCS transitions
defined in Section 4.4, or directly the resulting concept of a just path,
needs to be seen as an integral part of CCS. In Sections 18 and 19 I will
illustrate this impossibility result for a rendering of Peterson’s protocol as
a Petri net and as a CCS expression, respectively. In [GH15b, GH19] moreover
the point of view is defended that assuming (strong or weak) fairness is
typically unwarranted, in the sense that there is no reason to assume that
reality will behave in a fair way. From this point of view, a model of a
mutual exclusion that hinges on a fairness assumption can be seen as incorrect
or unsatisfactory. This makes the above into a real impossibility result.

The second impossibility result was claimed in [Gla18], but unaccompanied by
written evidence. It blames the first impossibility result above on the
combination of two assumptions or protocol features, which I here call
_atomicity_ and _speed independence_. Atomicity, or rather the special case of
atomicity that is relevant for the second impossibility result, will be
formally defined as (1) in Section 20. It can be seen as an assumption on the
behaviour of the hardware on which an implementation of a mutual exclusion
protocol will be running. Atomicity is explicitly assumed in the original
paper of Dijkstra where the mutual exclusion problem was presented [Dij65],
and implicitly in many other papers on mutual exclusion, but not in the work
of Lamport [Lam74]. Speed independence can either be seen as an assumption on
the underlying hardware, or as a feature of a mutual exclusion protocol. The
assumption stems from Dijkstra [Dij65] and was quoted in Section 9. The claims
of [Gla18] employ a rather strict interpretation of speed independence,
illustrated in Example LABEL:ex:speed_independence.

In a setting where solutions based on the assumption of weak fairness are
rejected, as well as solutions that are merely probabilistically correct,
[Gla18] claims that when assuming atomicity, speed-independent mutual
exclusion is impossible. This means that when assuming atomicity and speed
independence, there is no mutual exclusion protocol satisfying ME 1–6 with
$CC=J$. The assumption of speed independence is built in in CCS and Petri
nets, in the sense that any correct mutual exclusion protocol formalised
therein is automatically speed independent. This is because these models lack
the expressiveness to make anything dependent on speed. When taking the
concurrency relation between CCS or net transitions defined in Section 4.4 as
an integral part of semantics of CCS or Petri nets, also the assumption of
atomicity is built in in these frameworks. This makes the first impossibility
result a special case of the second. The latter can be seen as a
generalisation of the former that is not dependent on a particular modelling
framework. In Section 22 I will substantiate the above claim of [Gla18] for
the special case of Peterson’s protocol.

The third impossibility result, also claimed in [Gla18], says that when
dropping the assumption of atomicity, but keeping speed independence, there
still exists no mutual exclusion protocol satisfying ME 3Pr. That is, the
assumption of progress is not strong enough to obtain starvation-freedom of
any speed-independent mutual exclusion protocol. I will substantiate this
claim for the special case of Peterson’s protocol in Section 16. In Part IV I
aim for a formalisation of Peterson’s protocol that satisfies ME 3Pr. It
follows that there I will have to drop speed independence.

###  16\. Peterson’s Mutual Exclusion Protocol

A pseudocode rendering of Peterson’s protocol is depicted in Figure 5. The two
processes, here called A and B, use three shared variables: ${\it readyA}$,
${\it readyB}$ and ${\it turn}$. The Boolean variable ${\it readyA}$ can be
written by Process ${\rm A}$ and read by Process ${\rm B}$, whereas ${\it
readyB}$ can be written by ${\rm B}$ and read by ${\rm A}$. By setting ${\it
readyA}$ to ${\it true}$, Process ${\rm A}$ signals to Process ${\rm B}$ that
it wants to enter the critical section. The variable ${\it turn}$ can be
written and read by both processes. Its carefully designed functionality
guarantees mutual exclusion as well as deadlock-freedom. Both ${\it readyA}$
and ${\it readyB}$ are initialised with ${\it false}$ and ${\it turn}$ with
$\it A$.

$\begin{array}[]{@{}l@{}}\underline{\bf Process~{}{\rm A}}\\\\[1.93748pt] {\bf
repeat~{}forever}\\\ \left\\{\begin{array}[]{ll}\ell_{1}&{\bf
leave~{}noncritical~{}section}\\\ \ell_{2}&\it{\it readyA}:={\it true}\\\
\ell_{3}&\it{\it turn}:=B\\\ \ell_{4}&{\bf await}\,(\it{\it readyB}={\it
false}\vee{\it turn}=A)\\\ \ell_{5}&{\bf enter~{}critical~{}section}\\\
\ell_{6}&{\bf leave~{}critical~{}section}\\\ \ell_{7}&\it{\it readyA}:={\it
false}\\\ \ell_{8}&{\bf enter~{}noncritical~{}section}\\\
\end{array}\right.\end{array}~{}~{}~{}~{}~{}~{}\begin{array}[]{@{}l@{}}\underline{\bf
Process~{}{\rm B}}\\\\[1.93748pt] {\bf repeat~{}forever}\\\
\left\\{\begin{array}[]{ll}m_{1}&{\bf leave~{}noncritical~{}section}\\\
m_{2}&\it{\it readyB}:={\it true}\\\ m_{3}&\it{\it turn}:=A\\\ m_{4}&{\bf
await}\,({\it readyA}={\it false}\vee{\it turn}=B)\\\ m_{5}&{\bf
enter~{}critical~{}section}\\\ m_{6}&{\bf leave~{}critical~{}section}\\\
m_{7}&\it{\it readyB}:={\it false}\\\ m_{8}&{\bf
enter~{}noncritical~{}section}\\\ \end{array}\right.\end{array}$

Figure 5. Peterson’s algorithm (pseudocode)

$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{1}\end{array}$ lnA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{2}\end{array}$ lnAlnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{3}\end{array}$ lnA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{8}\end{array}$ lnAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{6}\end{array}$ecB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{7}\end{array}$lcB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{1}\end{array}$ ecA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{2}\end{array}$ ecAlnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{3}\end{array}$ ecA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{8}\end{array}$ ecAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{1}\end{array}$ lcA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{2}\end{array}$ lcAlnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{3}\end{array}$ lcA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{8}\end{array}$ lcAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{8}\end{array}$enB enA enA enA enA$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{6}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{8}\end{array}$enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{1}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{2}\end{array}$lnA lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{3}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{4}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{5}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{6}\end{array}$lnA ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{7}\end{array}$lnA lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{8}\end{array}$lnA enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{6}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{8}\end{array}$enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{4}\end{array}$ecA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{4}\end{array}$lcA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{6}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{8}\end{array}$enBenA enA enA enA enA enA enA enA

Figure 6. LTS of Peterson’s mutual exclusion algorithm

Figure 6 presents a labelled transition system for this protocol. The name of
a state $\begin{array}[]{c}T\\\\[-3.0pt] \ell_{i}m_{j}\end{array}$ where $T$
is $A$ or $B$ indicates that Process ${\rm A}$ is in State $\ell_{i}$, Process
${\rm B}$ in State $m_{j}$ and the variable $turn$ has value $T$, with the
convention that Instruction $\ell_{i}$ leads from State $\ell_{i}$ to State
$\ell_{i+1}$. This completely determines the values of the variables ${\it
readyA}$ and ${\it readyB}$. The actions lnA, lnB, ecA, ecB, lcA, lcB, enA and
enB are visible; they correspond to the instructions $\ell_{1}$, $m_{1}$,
$\ell_{5}$, $m_{5}$, $\ell_{6}$, $m_{6}$, $\ell_{8}$ and $m_{8}$,
respectively. All other transitions, unlabelled in Figure 6, are labelled
$\tau$. When assuming speed independence, none of the paths in Figure 6 can be
ruled out due to timing considerations. This makes Figure 6 an adequate
rendering of Peterson’s protocol.

From the pseudocode in Figure 5 one sees immediately that Peterson’s protocol
satisfies ME 1 (all visible actions occur in the right order) and ME 6J
(nothing stands in the way of a process leaving its noncritical section). By
inspecting the LTS in Figure 6 one sees that it moreover satisfies ME 2 (the
mutual exclusion property) and ME 4Pr (assuming progress and willingness to do
so is enough to ensure that a process will leave its critical section after
entering). One obtains ME 5J (assuming justness suffices to ensure that a
process always enters its noncritical section after leaving its critical
section) by combining the code and the LTS. The LTS shows that assuming
progress suffices to ensure that lcB is always followed by $m_{7}$. The code
shows that assuming justness suffices to ensure that $m_{7}$ is always
followed by lnB. Of course the same applies to Process A.

More problematic is Requirement ME 3, starvation-freedom. Thanks to symmetry,
I may restrict attention to ME 3 for Process A. Will
$\ell_{1}=\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{A}$}$ always be followed by
$\ell_{4}=\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{A}$}$? The LTS shows that $\ell_{2}$ is always followed by
$\ell_{4}=\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{A}$}$, even when merely assuming progress. However, it is less clear
whether
$\ell_{1}=\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{A}$}$ is always followed by $\ell_{2}$. The only111111when considering
two paths essentially the same if they differ merely on a finite prefix
progressing path $\pi_{P}$ on which is $\ell_{1}$ not followed by $\ell_{2}$
visits state $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{4}\end{array}$
infinitely often and always takes the transition going right. This path
witnesses that progress is not strong enough an assumption to ensure ME 3,
whereas weak fairness is, provided all the transitions stemming from
Instruction $\ell_{2}$ form a task.121212Formally, $\mbox{\it
Peterson}\models_{B}^{{\it WF}(\Tsk)}{\bf
G}(\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{i}$}\Rightarrow{\bf
F}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{i}$})$ when $\textsc{l}_{2},\textsc{m}_{2}\in\Tsk$, where
$\textsc{l}_{2}$ (resp. $\textsc{m}_{2}$) contains all transitions stemming
from instruction $\ell_{2}$ (resp. $m_{2}$). Namely, $\pi_{P}$ fails to be
weakly fair, for it has a suffix on which task $\textsc{l}_{2}$ is perpetually
enabled but never occurs. Whether justness is a strong enough assumption for
ME 3 depends solely on the question whether $\pi_{P}$ is just.

To answer that question one can interpret the LTS of Figure 6 as an LTSC, by
investigating an appropriate concurrency relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$ on
the transitions. Whether two transitions are concurrent ought to depend solely
on the instructions $\ell_{i}$ and $m_{j}$ from Figure 5 that gave rise to
these transitions, that is, whether $\ell_{i}\smile m_{j}$ for
$i,j=1,\dots,8$. Assuming that the three variables ${\it readyA}$, ${\it
readyB}$ and ${\it turn}$ are stored in independent stores or registers, the
only pairs that may violate $\ell_{i}\smile m_{j}$ are
$\ell_{3}\,\not\\!\smile m_{3}$, $\ell_{2}\,\not\\!\smile m_{4}$,
$\ell_{3}\,\not\\!\smile m_{4}$, $\ell_{7}\,\not\\!\smile m_{4}$,
$\ell_{4}\,\not\\!\smile m_{2}$, $\ell_{4}\,\not\\!\smile m_{3}$ and
$\ell_{4}\,\not\\!\smile m_{4}$, for these instruction compete for access to
the same register.131313The verdicts $\ell_{1}\smile m_{j}$, $\ell_{8}\smile
m_{j}$, $\ell_{i}\smile m_{1}$ and $\ell_{i}\smile m_{8}$ were already used
implicitly in the above derivation of ME 6J and ME 5J from the pseudocode. The
only pair out of these 7 that affects the justness of $\pi_{P}$ is
$\ell_{2}\,\not\\!\smile m_{4}$. Considering that in State
$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{4}\end{array}$ it is possible to
perform Instruction $m_{4}$, moving to State $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{5}\end{array}$, yet in State $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{4}\end{array}$, thus after performing $\ell_{2}$, it is no longer
possible to perform Instruction $m_{4}$, one surely has
$m_{4}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}\ell_{2}$,
that is, Instruction $m_{4}$ is affected by $\ell_{2}$—compare (2). On the
other hand, one cannot derive from Figure 6 alone whether
$\ell_{2}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$.
In case one decides that
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$
then $\pi_{P}$ is not $B$-just by Definition LABEL:df:Bjustness; as nothing
blocks the execution of Instruction $\ell_{2}$, it must eventually occur. In
this case ME 3J holds. However, in case one decides that
$\ell_{2}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$,
then $\pi_{P}$ is just and ME 3J does not hold.

Sections 18–19 examine whether
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$
holds in renderings of this protocol as a Petri net and in CCS. In Section 20
I will reflect on whether
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$
holds, and thus on whether Peterson’s protocol satisfies ME 3J, based on a
classification as to what could happen if two processes try to access the same
register at the same time, one writing and one reading.

###  17\. Verifications of Starvation-Freedom Merely Assuming Progress

Above, I argued that in any formalisation $P$ of Peterson’s algorithm that is
consistent with the LTS of Figure 6—including any speed-independent
formalisation—one has $P\not\models_{B}^{\it Pr}{\bf
G}(\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{i}$}\Rightarrow{\bf
F}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{i}$})$, that is, Requirement ME 3Pr does not hold, or, the
formalisation $P$ does not satisfy starvation-freedom when merely assuming
progress. The path $\pi_{P}$ from Section 16 constitutes a counterexample. In
Part IV of this paper I will bypass this verdict by proposing a formalisation
of Peterson’s algorithm that is not consistent with the LTS of Figure 6.

In [Wal89], Peterson’s algorithm was formalised in a way that is consistent
with Figure 6, yet starvation-freedom was proven, even by automatic means,
while assuming no more than progress. The contradiction with the above is only
apparent, because the starvation-freedom property obtained by [Wal89] can be
stated as $P\not\models_{B}^{\it Pr}{\bf G}(\ell_{2}\Rightarrow{\bf
F}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{A}$})$, and symmetrically $P\not\models_{B}^{\it Pr}{\bf
G}(m_{2}\Rightarrow{\bf
F}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{B}$})$, that is, once a process expresses its intention to enter its
critical section, by executing Instruction $\ell_{2}$ (or $m_{2}$), then it
will surely reach its critical section.141414In the literature [SGG12, Ray13]
it is frequently claimed that once Process ${\rm A}$ expresses its intention
to enter its critical section, by executing Instruction $\ell_{2}$, Process
${\rm B}$ will enter the critical section at most once before ${\rm A}$ does
(and the same with ${\rm A}$ and ${\rm B}$ reversed, of course). A
counterexample is provided by the path that turns right as much as possible
from the state $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{3}m_{5}\end{array}$.
Here Process ${\rm A}$ has just executed $\ell_{2}$, but Process ${\rm B}$
enters the critical section twice before ${\rm A}$ does. (By the definitions
in [Ray13], in state $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{5}\end{array}$ the two processes are _competing_ , and ${\rm A}$
loses the competition twice.)  Thesame can be said for the verification of
starvation-freedom of Peterson’s algorithm in [VS96], and, in essence, for the
verification of starvation-freedom of Dekker’s algorithm in [EB96].

It can be (and has been) debated which is the better formalisation of
starvation-freedom. Since the greatest hurdle in the protocol is Instruction
$\ell_{2}$, it seems unfair to say that a process is only deemed interested in
entering the critical section when this hurdle is taken.151515Suppose I
promise all of you $1000, if only you express interest in getting it, by
filling in Form 316F. Then I implement this promise by making it impossible to
fill in Form 316F. In that case you might argue against the claim that the
Requirement $~{}~{}{\bf G}(\mbox{``has interest''}\Rightarrow{\bf
F}\mbox{``receive \$1000''})~{}~{}$ can be verified. The argument would be
that filling in Form 316F is an inadequate formalisation of having interest in
getting this price. Another tactic is to consider a form of Peterson’s
protocol in which Processes ${\rm A}$ and ${\rm B}$ are merely interfaces that
interact with the real clients that compete for access to the critical section
by synchronising on the actions lnA, lnB, ecA, ecB, lcA, lcB, enA and enB. In
such a case, the real intent of Client ${\rm A}$ to enter its critical section
is expressed in a message to Interface ${\rm A}$ that occurs strictly before
Interface ${\rm A}$ executes Instruction $\ell_{2}$.

Such arguments are less necessary now that I have formalised ME 6 as an
additional requirement. Suppose that one would redefine the action lnA that
appears in the antecedent of the starvation-freedom requirement ME 3 as the
occurrence of instruction
$\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{2}$
from Peterson’s algorithm, thus turning ME 3 for Process ${\rm A}$ into
$P\models_{B}^{CC}{\bf
G}({\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{2}}\Rightarrow{\bf
F}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{A}$})$, then ME 6 becomes
$P\models_{B\setminus\\{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{2}}\\}}^{CC}{\bf
F}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{2}}\wedge{\bf
G}(\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{A}$}\Rightarrow{\bf
F}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\ell_{2}})$.
Either way, it is required that $\ell_{1}$ will be followed by $\ell_{2}$;
this requirement is either part of ME 6 or of ME 3. In case it takes weak
fairness to perform Instruction $\ell_{2}$, either ME 3 or ME 6 will hold only
for $CC={\it WF}$, and depending on one’s modelling preferences one can choose
which one.

In Sections 18 and 19 I will show that in formalisations of Peterson’s
algorithm as a Petri net or a CCS expression, the path $\pi_{P}$ from Section
16 is just, implying that it takes weak fairness to perform Instruction
$\ell_{2}$. This implies that those formulations can in terms of Figure 3 be
situated either at the coordinates $({\it WF},{\it Pr})$ or $({\it J},{\it
WF})$, depending on one’s preferred modelling of intent to enter the critical
section. Either way, such a rendering of Peterson scores no better than the
(encapsulated) gatekeeper.

###  18\. Modelling Peterson’s Protocol as a Petri Net

Figure 7 shows a rendering of Peterson’s protocol as a Petri net. There is one
place for each of the local states $\ell_{1}$–$\ell_{8}$ and $m_{1}$–$m_{8}$
of Processes ${\rm A}$ and ${\rm B}$ and two for each of the Boolean variables
${\it readyA}$, ${\it readyB}$ and ${\it turn}$. There is one transition for
each of the instructions $\ell_{1}$–$\ell_{8}$ and $m_{1}$–$m_{8}$, except
that $\ell_{3}$, $m_{3}$, $\ell_{4}$ and $m_{4}$ yield two transitions each.
For $\ell_{3}$ and $m_{3}$ this is to deal with each of the possible values of
${\it turn}$ before the assignment is executed; for $\ell_{4}$ the two
transitions are for reading that ${\it turn}=A$, and for reading that ${\it
readyB}={\it false}$.

$\bullet$lnA$\ell_{2}$$\ell_{2}$$\ell_{3}$$\ell_{4}$$\ell_{5}$ecA$\ell_{6}$lcA$\ell_{7}$$\ell_{7}$$\ell_{8}$enA${\it
readyA}$${\it turn}$${\it readyA}$$\hskip 6.0pt{\it
false}$$\bullet$$\bullet$lnB$m_{2}$$m_{2}$$m_{3}$$m_{4}$$m_{5}$ecB$m_{6}$lcB$m_{7}$$m_{7}$$m_{8}$enB${\it
readyB}$${\it true}$${\it readyB}$$\hskip 6.0pt{\it
false}$$\bullet$$\ell_{3}$${\it turn}$$\hskip
10.0ptA$$\bullet$$m_{3}$$\ell_{3}$${\it
turn}$$B$$m_{3}$$\ell_{4}^{\,t\\!}$$m_{4}^{\,t\\!}$$\ell_{4}^{B\\!}$$m_{4}^{A\\!}$

Figure 7. Petri net representation of Peterson’s mutual exclusion algorithm

The transitions $\ell_{2}$ and $m_{4}^{A}$ are not concurrent, because they
compete for the same token on the place ${\it readyA}={\it false}$. For this
reason the run $\pi_{P}$, in which one token is stuck in place $\ell_{2}$
while the other four tokens keep moving around—with $m_{4}^{A}$ executed
infinitely many times—is just. Consequently, this Petri net does not satisfy
requirement ME 3J.

###  19\. Modelling Peterson’s Protocol in CCS

In order to model Peterson’s mutual exclusion protocol in CCS, I use the names
enA, enB, lnA, lnB, ecA, ecB, lcA and lcB for Processes A and B entering and
leaving their (non)critical section. Following [DGH17], I describe a simple
shared memory system in CCS, using the name ${\it asgn}_{x}^{\,v}$ for the
assignment of value $v$ to the variable $x$, and ${\it n}_{x}^{\,v}$ for
noticing or notifying that the variable $x$ has the value $v$. The action
$\overline{{\it asgn}_{x}^{\,v}}$ communicates the assignment $x:=v$ to the
shared memory, whereas ${\it asgn}_{x}^{\,v}$ is the action of the shared
memory of accepting this communication. Likewise, $\overline{{\it
n}_{x}^{\,v}}$ is a notification by the shared memory that $x$ equals $v$; it
synchronises with the complementary action ${\it n}_{x}^{\,v}$ of noticing
that $x=v$.

The Processes A and B can be modelled as

$\begin{array}[]{@{}l@{~\stackrel{{\it def}}{=}~}l@{}}{\rm
A}\hfil~{}\stackrel{{\scriptstyle{\it
def}}}{{=}}&\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{A}$}\mathbin{.}\overline{{\it asgn}_{{\it readyA}}^{\,{\it
true}}}\mathbin{.}\overline{{\it asgn}_{{\it turn}}^{\,B}}\mathbin{.}({\it
n}_{{\it readyB}}^{\,{\it false}}\ +\ {\it n}_{{\it
turn}}^{\,A})\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{A}$}\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{A}$}\mathbin{.}\overline{{\it asgn}_{{\it readyA}}^{\,{\it
false}}}\mathbin{.}\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{A}$}\mathbin{.}{\rm A}\ ,\\\ {\rm B}\hfil~{}\stackrel{{\scriptstyle{\it
def}}}{{=}}&\mbox{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\it
ln${}_{B}$}\mathbin{.}\overline{{\it asgn}_{{\it readyB}}^{\,{\it
true}}}\mathbin{.}\overline{{\it asgn}_{{\it turn}}^{\,A}}\mathbin{.}({\it
n}_{{\it readyA}}^{\,{\it false}}\ +\ {\it n}_{{\it
turn}}^{\,B})\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{B}$}\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{B}$}\mathbin{.}\overline{{\it asgn}_{{\it readyB}}^{\,{\it
false}}}\mathbin{.}\mbox{\color[rgb]{1,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,1}\pgfsys@color@cmyk@stroke{0}{1}{0}{0}\pgfsys@color@cmyk@fill{0}{1}{0}{0}\it
en${}_{B}$}\mathbin{.}{\rm B}\ ,\end{array}$

where $(a+b).P$ is a shorthand for $a.P+b.P$. This CCS rendering naturally
captures the await statement, requiring Process A to wait at Instruction
$\ell_{4}$ until it can read that ${\it readyB}={\it false}$ or ${\it
turn}=A$. We use two agent identifiers for each Boolean variable $x$, one for
each value:

$\begin{array}[]{r@{\ }c@{\ }l}x^{\it true}&\stackrel{{\scriptstyle\it
def}}{{=}}&{\it asgn}_{x}^{\,{\it true}}\mathbin{.}x^{\it true}\ +\ {\it
asgn}_{x}^{\,{\it false}}\mathbin{.}x^{\it false}\ +\ \overline{{\it
n}_{x}^{\,{\it true}}}\mathbin{.}x^{\it true}\ ,\\\ x^{\it
false}&\stackrel{{\scriptstyle\it def}}{{=}}&{\it asgn}_{x}^{\,{\it
true}}\mathbin{.}x^{\it true}\ +\ {\it asgn}_{x}^{\,{\it
false}}\mathbin{.}x^{\it false}\ +\ \overline{{\it n}_{x}^{\,{\it
false}}}\mathbin{.}x^{\it false}\ .\end{array}$

Likewise we have, for instance,

${\it Turn}^{A}~{}\stackrel{{\scriptstyle{\it def}}}{{=}}~{}{\it asgn}_{{\it
turn}}^{\,A}\mathbin{.}{\it Turn}^{A}\ +{\it asgn}_{{\it
turn}}^{\,B}\mathbin{.}{\it Turn}^{B}\ +\ \overline{{\it n}_{{\it
turn}}^{\,A}}\mathbin{.}{\it Turn}^{A}.$

Peterson’s mutual exclusion algorithm (PME) is the parallel composition of all
these processes, restricting all the communications

$({\rm A}\mid{\rm B}\mid{\it ReadyA}^{\,{\it false}}\mid{\it ReadyB}^{\,{\it
false}}\mid{\it Turn}^{A})\backslash L\ ,$

where $L$ is the set of all names except enA, enB, lnA, lnB, ecA, ecB, lcA and
lcB [DGH17].

The LTS of the above CCS expression PME is exactly as displayed in Figure 6.
By the interpretation of CCS as an LTSC, defined in Section 4.4, one obtains
$\ell_{2}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$,
where I use the names $\ell_{2}$ and $m_{4}$ of the underlying instructions
from Figure 5 to denote the two outgoing $\tau$-transitions from the state
$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{4}\end{array}$. In fact, this
could have been concluded without studying the above CCS rendering of
Peterson’s protocol, as Section 4.4 remarks that in the LTSC of CCS the
relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$ is
symmetric, while Section 16 concludes that
$m_{4}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}\ell_{2}$.
Thus, the CCS rendering of Peterson’s algorithm does not satisfy the
correctness criterion ME 3J.

###  20\. What Happens if Processes Try to Read and Write Simultaneously

A program instruction like $\ell_{2}$, $\ell_{3}$, $\ell_{4}$ or $\ell_{7}$
that reads or writes a value ${\it true}$, ${\it false}$, $A$ or $B$ from or
to a register ${\it readyA}$, ${\it readyB}$ or ${\it turn}$ cannot be
executed instantaneously, and is thus assumed to occur during a interval of
real time. Hence it may happen that Processes ${\rm A}$ and ${\rm B}$ try to
access the same register during overlapping periods of time. In such a case is
it common to assume that the register is _safe_ , meaning that

A read operation not concurrent with any write operation returns the value
written by the latest write operation, provided the last two write operations
did not overlap.

This assumption stems from [Lam86], although overlapping writes were not
considered there. “No assumption is made about the value obtained by a read
that overlaps a write, except that it must obtain one of the possible values
of the register.” [Lam86]161616This is not really a restriction, for one can
always follow a read action $r:=x$ of a variable $x$, where $r$ is a local
register, by a default assignment $r:=v_{0}$ in case the read yields a value
that is out of range. In the same spirit, one may assume that two overlapping
writes may put any of its possible values in the register, in the sense that
subsequent reads will return that value. I will assume safety in this sense of
the Boolean registers ${\it readyA}$, ${\it readyB}$ and ${\it turn}$. In an
architecture where safe registers are not available, and cannot be simulated,
implementing a correct mutual exclusion protocol appears to be
hopeless.171717This statement can be strengthened by considering its
contrapositive: if one has a correct mutual exclusion protocol, safe registers
can be simulated. Namely, when confronted with a weak memory, where it takes
time for writes to propagate after the instruction has been encountered, one
could put each read and write instruction in a critical section, together with
an appropriate memory barrier or fence instruction, to ensure propagation of
the write before any read occurs. This ought to yield safety.

For the fate of Peterson’s algorithm it matters what happens if one process
wants to start writing a register when another is busy reading it. There
appear to be only three (or five) possibilities.

  1. (1)

The register cannot handle a read and a write at the same time; as the read
started first, the writing process will need to await the termination of the
read action before the write can commence.

  2. (2)

The register cannot handle a read and a write at the same time, but the write
takes precedence and occurs when scheduled. This aborts the read action, which
can restart after the write has terminated.

  3. (3)

The read and write proceed as scheduled, thus overlapping in time.

A fourth possibility could be that reads and writes are instantaneously after
all, so that overlap can be avoided without postponing either. I deem this
unrealistic and do not consider this option here. A potential fifth
possibility could be a variation of (2), in which the read merely is
interrupted, and resumes after the write is finished. In that case, as with
option (3), it seems reasonable to assume that the read can return any value
of the register.

In Dijkstra’s original formulation of the mutual exclusion problem [Dij65],
possibility (1) above— _atomicity_ —was assumed—see the quote in Section 9.
Lamport, on the other hand, assumes (3) [Lam74]. On his webpage
https://lamport.azurewebsites.net/pubs/pubs.html#bakery Lamport takes the
position that assuming atomicity “cannot really be said to solve the mutual
exclusion problem”, as it assumes “lower-level mutual exclusion”. As
possibility (3) adds the complication of arbitrary register values returned by
reads that overlap a write, he implicitly takes the position that solving the
mutual exclusion problem under assumption (3) is more challenging; and this is
exactly what his bakery algorithm does.

Here I argue that atomicity is the more challenging assumption. The objection
that assuming reads and writes to be atomic amounts to assuming “lower-level
mutual exclusion” is based on the idea that securing the mutex property of a
mutual exclusion protocol is the main challenge. However, the real challenge
is doing this in a starvation-free way, and this feature is not inherited from
the lower level. By assuming atomicity one obtains
$\ell_{2}\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$,
that is, transition $\ell_{2}$ is affected by $m_{4}$, and consequently
Peterson’s algorithm fails the correctness requirement ME 3J. In Section 22
below I will argue that this is not merely a result of the way I choose to
model things in this paper, but actual evidence of the incorrectness of
Peterson’s algorithm, or any other mutual exclusion protocol for that matter,
provided one consistently assumes atomicity, as well as speed independence.

Assuming (2) instead yields
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$,
that is, the write $\ell_{2}$ is in no way affected by the read $m_{4}$. This
means that nothing can prevent Process ${\rm A}$ form executing $\ell_{2}$.
This makes Peterson’s algorithm correct, in the sense that it satisfies ME 3J.

Assuming (3) also yields
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$.
Also this would make the algorithm correct, provided that it is robust against
the effects of overlapping reads and writes. For Peterson’s algorithm this is
not the case; overlapping reads and writes can cause a violation of the mutex
property ME 2—see Section 21. However, various other mutual exclusion
protocols, including the ones of [Lam74] and [Szy88], are robust against the
effects of overlapping reads and writes and do satisfy ME 3J when assuming
(3).

In CCS, and in Petri nets,
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$ is
symmetric, and one has $\ell\,\not\\!\smile m$ whenever $\ell$ and $m$ are
read or write instructions on the same register, at least when employing the
concurrency relation $\smile$ of Section 4.4. This amounts to assuming
atomicity.

###  21\. Is Peterson’s Protocol Resistant Against Overlapping Reads and
Writes?

Those mutual exclusion protocols that were designed to be robust under
overlapping reads and writes, avoid overlapping writes altogether, either by
making sure that each variable can be written by only one process (although it
can be read by others) [Lam74, Szy88], or by putting writes to the same
variable right before [Dij63]181818The very first mutual exclusion algorithm
[Dij63], by Dekker, may not have been intended to be robust under overlapping
reads and writes, but it is not hard to check that it is. or after [Ara11] the
critical section, within the part of a process’ cycle that is made mutually
exclusive. Any protocol that doesn’t take this precaution, including
Peterson’s, is regarded with suspicion by those that make an effort to avoid
ill effects due to reads overlapping with writes. Nevertheless, until May 2021
no examples were known (to me at least) that overlapping reads and writes
actually cause any problem for Peterson’s protocol. I personally believed that
it was robust under overlap, reasoning as follows [unpublished notes].

> Two overlapping write actions to the same register may produce any value of
> that register. In Peterson’s algorithm, the only register that can be
> written by both processes contains the variable ${\it turn}$. It is a
> Boolean register, whose values are $A$ and $B$. The only write actions to
> this register are $\ell_{3}$ and $m_{3}$. When these overlap in time, any of
> the register values, that is $A$ or $B$, may result. However, $\ell_{3}$
> tries to write the value $B$, and $m_{3}$ the value $A$. So if the result of
> a simultaneous write is $A$, one can just as well assume that $\ell_{3}$
> occurred before $m_{3}$, and it it is $B$, that $m_{3}$ occurred before
> $\ell_{3}$. Thus the effects of overlapping writes are no different than
> those of atomic writes, and hence harmless.
>
> Peterson’s algorithm has six cases of a read overlapping with a write, and
> thanks to symmetry it suffices to study three of them. First consider the
> overlap of the write $\ell_{2}$ with the read $m_{4}$. Here the overlapping
> read can yield any register value, that is, ${\it true}$ or ${\it false}$.
> One should not ignore the possibility that Process ${\rm B}$, while cycling
> around, performs multiple $m_{4}$-reads of ${\it readyA}$ that may return
> any sequence of ${\it true}$ and ${\it false}$ during a single write action
> $\ell_{2}$ of Process ${\rm A}$. However, any read by Process ${\rm B}$ that
> returns ${\it readyA}={\it true}$ does not help to pass the await-statement
> in $m_{4}$, and is equivalent to no read of ${\it readyA}$ being carried
> out. So all reads that matter return ${\it readyA}={\it false}$, and can
> just as well be thought of as occurring prior to $\ell_{2}$. A similar
> argument applies to the overlap of the write $\ell_{3}$ with the read
> $m_{4}$, and of the write $\ell_{7}$ with the read $m_{4}$; also here any
> resulting behaviour can already be generated without assuming an overlap.

I leave it as a puzzle to the reader to find the fallacy in this argument. A
run of Peterson’s algorithm that violates the mutex property ME 2 was found in
2021 by means of the model checker mCRL2 by Myrthe Spronck [Spr21]. This
involved implementing safe registers, as described in Section 20, as mCRL2
processes.

###  22\. The Impossibility of Mutual Exclusion
when Assuming Atomicity and Speed Independence

In this section I argue that when assuming atomicity and a strict form of
speed independence, Peterson’s algorithm is not correct, in the sense that it
fails the requirement of starvation freedom. The argument is that the the run
corresponding with the path $\pi_{P}$ from Section 16 can actually occur. To
see why, let me illustrate the form of speed independence needed for this
argument by means of a simple example in CCS.

######  Example 22.1.

speed independence Consider the process $(X|Y){\setminus}\\{c\\}$ with
$X\stackrel{{\scriptstyle{\it def}}}{{=}}a.{\bf 0}+\bar{c}.X$ and
$Y\stackrel{{\scriptstyle{\it def}}}{{=}}c.d.e.Y$, where none of the actions
$a,d,e$ is blocked by the environment, that is, the environment is
continuously eager to partake in these actions. The question is whether action
$a$ is guaranteed to occur.

Here one may argue that when Process $X$ reaches the state $a.{\bf
0}+\bar{c}.X$ at a time when its environment, which is the Process $Y$, is not
yet ready to engage in the synchronisation on $c$, it will proceed by
executing $a$. If, on the other hand, both options $a$ and $\bar{c}$ are
available, it cannot be excluded that $\bar{c}$ is chosen, as no priority
mechanism is at work here.

Now after execution of $\bar{c}|c$, Process $X$ again faces a choice between
$a$ and $\bar{c}$, but Process $Y$ first has to execute the actions $d$ and
$e$. During the time that $Y$ is busy with $d$ and $e$, for Process $X$ it
feels like $\bar{c}$ is blocked, and it will do $a$.

A strict interpretation of speed independence, which I employ here, says that
actions $d$ and $e$ may be executed so fast that from the perspective of
Process $X$ one can just as well assume that no actions $d$ and $e$ were
scheduled at all. Thus the answer to the above question will not change upon
replacing Process $Y$ by $Y^{\prime}\stackrel{{\scriptstyle{\it
def}}}{{=}}c.Y^{\prime}$. However, for the process
$(X|Y^{\prime}){\setminus}\\{c\\}$ there is really no reason to assume that
$a$ will ever occur.

In CCS and related process algebras this form of speed independence is built
in: one sees $c$ and $d$ as $\tau$-transitions, as for the purpose of
answering the above question they can be regarded as unobservable, and then
applies the law $a.\tau.P=a.P$ [Mil90].

A run of Peterson’s protocol, or any implementation thereof in a setting where
atomicity and the above form of speed independence may be assumed, can visit
the state $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{4}\end{array}$ in which
Process ${\rm A}$ wants to write on register ${\it readyA}$, and that register
has a choice between being written or being read first, by Process ${\rm B}$.
One cannot exclude that the read action wins this race, which allows Process
${\rm B}$ to enter the critical section. During the execution of $m_{4}$,
reading ${\it readyA}$, Process ${\rm A}$ has to wait. Afterwards, Process
${\rm B}$ might execute actions $m_{5}$–$m_{3}$ so fast that from the
perspective of Process ${\rm A}$ no time elapses at all. This brings us again
in State $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{4}\end{array}$ where the
same race between $\ell_{2}$ and $m_{4}$ occurs. Again it could be won by
$m_{4}$. This behaviour can continue indefinitely.

The above argument stems from [Gla18], where it was made not just for
Peterson’s protocol, but for all conceivable mutual exclusion algorithms.
These include Lamport’s bakery algorithm [Lam74], Szymański’s algorithm
[Szy88], and the round-robin scheduler. To obtain a correct mutual exclusion
algorithm, one has to either employ register hardware in which the assumption
of atomicity—possibility (1) in Section 20—is not valid, or make the protocol
speed-dependent. The first option was already explored in Section 20; as
mentioned there, using hardware that works according to possibilities (2) or
(3) solves the problem. The second option will be explored in Part IV of this
paper.

###  23\. Variations of Petri nets and CCS with Non-blocking Reading

To escape from the failure of requirement ME 3J for Peterson’s protocol due to
the assumption (1) of atomicity as well as speed independence, one can instead
assume possibility (2) from Section 20 while keeping speed independence. I
refer to such an option as _non-blocking reading_ [CDV09], as a write cannot
be postponed by a read action on the same register. This yields
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$,
thereby saving ME 3J. Here I review how this can be modelled in variations of
Petri nets and CCS.

####  23.1. Read Arcs

A Petri net with _read arcs_ is a tuple $N=(S,T,F,R,M_{0},\ell)$ as in
Definition LABEL:df:net, but enriched with a object $R:S\times
T\rightarrow\mbox{\bbb N}$, such that $F(s,t)>0\Rightarrow R(s,t)=0$. An
element $(s,t)$ of the multiset $R$ is called a _read arc_. Read arcs are
drawn as lines without arrow heads. For $t\mathbin{\in}T$, the multiset
$\hat{t}\\!:S\rightarrow\mbox{\bbb N}$ is given by
$\hat{t}(s)\mathbin{=}R(s,t)$ for all $s\mathbin{\in}S$. Transition $t$ is
_enabled_ under $M$ iff ${\vphantom{t}}^{\bullet}t+\hat{t}\leq M$. In that
case $M\mathrel{\hbox{$\mathop{\hbox
to13.50002pt{\rightarrowfill}}\limits^{\hbox to13.50002pt{\hfil\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle
t$\hskip 2.25pt}\hfil}}$}}_{N}M^{\prime}$, where
$M^{\prime}=(M-{\vphantom{t}}^{\bullet}t)+{t}^{\bullet}$.

Thus, for a transition to be enabled, there needs to be a token at the other
end of each of its read arcs. However, these tokens are not consumed by the
firing. Clearly, the transition relation $\mathrel{\hbox{$\mathop{\hbox
to13.50002pt{\rightarrowfill}}\limits^{\hbox to13.50002pt{\hfil\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle
t$\hskip 2.25pt}\hfil}}$}}_{N}$ between the markings of a net is unaffected
when replacing each read arc $(s,t)$ by a loop between $s$ and $t$; that is,
by dropping $R$ and using the flow relation $F_{R}:=F+R+R^{-1}$. This does not
apply to the concurrency relation between transitions.

The definition of a structural conflict net can be extended to Petri nets with
read arcs by requiring, for all $t,u\in T$ and all reachable markings $M$,
that

if
$({\vphantom{t}}^{\bullet}t+\hat{t}\,)\cap{\vphantom{u}}^{\bullet}u=\emptyset$
then ${\vphantom{t}}^{\bullet}t+\hat{t}+{\vphantom{u}}^{\bullet}u\not\leq M$
or $\hat{u}\not\leq M$.

For such nets, one defines
$t\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}u$ iff
$({\vphantom{t}}^{\bullet}t+\hat{t}\,)\cap{\vphantom{u}}^{\bullet}u=\emptyset$.
This says that a transition $u$ affects a transition $t$ iff $u$ consumes a
token that is needed to enable $t$. The condition for a structural conflict
net guarantees exactly that if
$t\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}u$
and $u$ is enabled under a reachable marking $M$, then $t$ is not enabled
under the marking $M-{\vphantom{u}}^{\bullet}u$.

As pointed out by Vogler in [Vog02], the addition of read arcs makes Petri
nets sufficiently expressive to model mutual exclusion. When changing the
loops  ${\it readyA}={\it false}$$m_{4}^{\scriptscriptstyle A\\!}$ and  ${\it
readyB}={\it false}$$\ell_{4}^{\scriptscriptstyle B\\!}$ in Figure 7 into read
arcs, one obtains
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}^{\scriptscriptstyle
B\\!}$ and
$m_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}\ell_{4}^{\scriptscriptstyle
A\\!}$. So the resulting net satisfies ME 1–6 with $CC=J$, and correctly
solves the mutual exclusion problem. Two different solutions as Petri nets
with read arcs are given in [Vog02, Figures 8 and 9], the one in Figure 9
being a round-robin scheduler.

####  23.2. Broadcast Communication

A process algebraic solution was presented in [GH15a, Section 5], using an
extension ABC of CCS with broadcast communication. The most obvious
distinction between broadcast communication and CCS-style handshaking
communication is that the former allows multiple recipients of a message and
the latter exactly one. This feature of broadcast communication was not
exploited in the solution of [GH15a]. A more subtle feature of broadcast
communication is that the transmission of a broadcast occurs regardless of
whether anyone is listening. Thus a broadcast can be used to model a write
that cannot be blocked or postponed because the receiving register is busy
being read. This yields an asymmetric concurrency relation, in which a
broadcast transition is not affected by a competing transition from a receiver
of the broadcast, whereas the competing transition _is_ affected by the
broadcast.

Nevertheless, the semantics of ABC says that the broadcast _will_ be received
by all processes that are in a state with an outgoing receive transition. This
allows one to make receipt of a broadcast reliable, by giving the receiving
process an outgoing receive action in each of its states. This feature of the
semantics of ABC, which is essential for modelling mutual exclusion, is
somewhat debatable, as one could argue that a process that is engaged in its
own broadcast transmission through a transition between two states that each
have a outgoing receive transition, is temporary too busy to hear an incoming
message.

The solution proposed in [GH15a] is not a mutual exclusion protocol, but a
fair scheduler, which can be converted into a mutual exclusion protocol in the
manner of Section 10. In fact, it is a variant of the encapsulated gatekeeper,
where broadcast communication is used to merely assume justness for all
requirements. In the same spirit one can model Peterson’s protocol in ABC in
such a way that ME 3J is satisfied. It suffers to interpret $\overline{{\it
asgn}_{x}^{\,v}}$ and ${\it asgn}_{x}^{\,v}$ as broadcast transmit and receive
actions. The LTSC semantics of ABC [Gla19a] then yields
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$.

####  23.3. Signals

A different process algebraic solution, arguably less debatable, was proposed
in [CDV09, DGH17]. In [CDV09], processes $P$ are equipped with the possibility
to perform actions that do not change their state, and that, in
synchronisation with another parallel process $Q$, describe information on the
state of $P$ that is read by $Q$ in a non-blocking way. In [DGH17], following
[Ber88], such actions are called _signals_. The communication between, say, a
traffic light, emitting the signal _red_ , and a car, coming to a halt, is
binary, just like handshaking communication in CCS. The difference is that the
concurrency relation between transitions again becomes asymmetric, because the
car is affected by the traffic light, but the traffic light is not affected by
the car. A car stopping for a red light in no way blocks or postpones the
action of the traffic light of turning green.

In [Ber88, DGH17] the emission of a signal is modelled as a predicate on
states, whereas the receipt of such an emission is modelled as a transition.
In [CDV09, Bou18] the emission of a signal is modelled as a transition
instead. An advantage of the former approach is that it stresses the semantic
difference between signal emissions and handshaking actions, and emphasises
that signal emissions cannot possibly cause a state-change. An advantage of
the latter approach is that communication via signals can be treated in the
same way as a CCS handshaking communication, thereby simplifying the process
algebra. Technically, the two approaches are equivalent.

${\it true}$$\overline{{\it n}_{x}^{\,{\it true}}}$${\it asgn}_{x}^{\,{\it
true}}$${\it false}$${\it asgn}_{x}^{\,{\it false}}$${\it asgn}_{x}^{\,{\it
true}}$${\it asgn}_{x}^{\,{\it false}}$$\overline{{\it n}_{x}^{\,{\it
false}}}$

In CCS with signals [DGH17], modelling signal emissions as transitions [Bou18,
Gla19a], a Boolean variable $x$, such as ${\it readyA}$ in Peterson’s
protocol, has the exact same LTS as in the CCS model of Section 19: However,
this time the notifications $\overline{{\it n}_{x}^{\,v}}$ are signals
emissions rather than handshaking actions. The definition of the concurrency
relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$ on
CCS transitions from Section 4.4 is in [Gla19a] extended to CCS with signals
in such a way that with the above way of modelling variables, and the same
processes ${\rm A}$ and ${\rm B}$ as in Section 19, one obtains
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$.
Here the action $m_{4}$ of reading the register is like a car reading a
traffic light, and does not inhibit the write action $\ell_{2}$ on the same
register.

This shows that Peterson’s algorithm can be correctly modelled in CCS with
signals. Earlier, Dekker’s algorithm was correctly modelled in the process
algebra PAFAS with non-blocking reading [CDV09], and same was done for
Peterson’s algorithm in [BCC+11]. The latter paper also points out that non-
blocking reading is not strong enough an assumption to obtain starvation-
freedom, or even deadlock-freedom as defined in Section 9, for Knuth’s
algorithm [Knu66]; this requires a fairness assumption.

####  23.4. Modelling Non-blocking Reading in CCS

The rendering in [DGH17] of Peterson’s protocol employs an extension of CCS
with signals that arguably strictly increases the expressiveness of the
language. Namely in CCS with signals one obtains an asymmetric concurrency
relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$,
which turned out to be essential for the satisfactory modelling of Peterson;
restricted to proper CCS this relation is symmetric. Bouwman [Bou18] proposes
the same modelling of Peterson’s protocol, but entirely within the confines of
the existing language CCS, namely by simply declaring some of the action names
of CCS to be signals. As it is essential that the emission of a signal never
causes a state-change, care has to be taken to only use CCS-expressions in
which the actions that are chosen to be seen as signal emissions occur in
self-loops only. When doing this, creating a satisfactory rendering of
Peterson’s protocol within CCS is unproblematic [Bou18]. Neither [DGH17] nor
[Bou18] mention the concurrency relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$ at
all, and use a coinductive definition of justness instead. However, as shown
in [Gla19a], the concept of justness common to [DGH17] and [Bou18] can
equivalently be obtained as in Section 5 from an asymmetric concurrency
relation
$\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}$.
Thus, by declaring certain CCS actions to be signals, Bouwman effectively
changes the concurrency relation between CCS transitions labelled with those
actions.

In [GH15b] it was stated that fair schedulers and mutual exclusion protocols
cannot be rendered correctly in CCS without imposing a fairness assumption. In
making that statement, the (symmetric) concurrency relation $\smile$ between
CCS transitions defined in Section 4.4—or equivalently, the resulting notion
of justness—was seen as an integral part of the semantics of CCS. In the early
days of CCS, a lot of work has been done in formalising notions of concurrency
for CCS and and related process algebras [NPW81, GM84, BC87, Win87, GV87,
DDM87, Old87]. All that work is consistent with the concurrency relation
$\smile$ defined in Section 4.4. Changing the concurrency relation, as
implicitly proposed by Bouwman, alters the language CCS as seen from the
perspective of [NPW81, GM84, BC87, Win87, GV87, DDM87, Old87]. However, it is
entirely consistent with the interleaving semantics of CCS given by Milner
[Mil90].

####  23.5. Modelling and Verification of Peterson’s Algorithm with mCRL2

ACP [BW90, Fok00] and mCRL2 [GM14] are CCS-like process algebras that fall
under the scope of the impossibility result of [GH15b]. That is, when defining
a concurrency relation on the transitions of ACP or mCRL2 processes in the
traditional way, consistent with the viewpoint of [NPW81, GM84, BC87, Win87,
GV87, DDM87, Old87], and defining justness as in Section 5 in terms of this
concurrency relation, Peterson’s algorithm cannot be correctly rendered in ACP
or mCRL2 when merely assuming justness, i.e., without resorting to a fairness
assumption. Nevertheless, by the argument of [Bou18], Peterson’s algorithm
_can_ be correctly rendered in these formalisms under the assumption of
justness when using an alternative concurrency relation, one obtained by
treating certain actions as signals.

Using this insight, Bouwman, Luttik and Willemse [BLW20] render Peterson’s
algorithm in an instance of ACP or mCRL2 that uses much more informative
actions. This could be done without adapting those languages in any way,
simply by choosing appropriate actions. Each action labelling a transition
contains additional information on the components of the system from which
this transition stems. This information is preserved under synchronisation,
when a transition of a parallel composition is built from transitions of each
of the components. The latter requires the general communication format of ACP
or mCRL2, as in CCS synchronisation merely result in $\tau$-transitions. A
price paid for this approach is that the resulting LTSs have much fewer
$\tau$-transitions, so that there are fewer opportunities for state-space
reduction by abstraction from internal activity.

In Section 7 I showed how $B$-justness, and thereby the correctness criteria
for mutual exclusion protocols, can be expressed in standard LTL enriched with
a number of atomic propositions, such as ${\it en}^{t}$ and $\sharp t$.
Bouwman, Luttik and Willemse [BLW20] show not only that the same can de done
in the modal $\mu$-calculus, but also that all the necessary atomic
propositions can be expressed in terms of the carefully chosen actions that
are used in modelling the protocol. This made it possible to model the
protocol in such way that all correctness requirements can be checked with the
existing mCRL2 toolset [BGK+19].

##  Part IV A Speed-dependent Rendering of Peterson’s Protocol

In Part III I showed that when assuming atomicity and speed independence,
Peterson’s algorithm does not have the correctness property ME 3J—and in
[Gla18] I argued that the same can be said for any other mutual exclusion
protocol. That is, it satisfies starvation-freedom only under a weak fairness
assumption, which in my opinion is not warranted — if it was, even the
encapsulated gatekeeper of Section 15 would be an acceptable mutual exclusion
protocol.

Thus, to obtain a correct version of Peterson’s algorithm (or mutual exclusion
in general) one has to either drop the assumption of atomicity, or speed-
independence. The former possibility has been elaborated in Part III; Section
16 showed then when assuming non-blocking reading (option (2) from Section 20,
resulting the verdict
$\ell_{2}\mathrel{\mbox{$\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}m_{4}$)
instead of atomicity, Peterson’s algorithm is entirely correct. Section 23
recalled how to model this with process algebra or Petri nets.

The latter possibility will be elaborated here. I present a speed-dependent
incarnation of Peterson’s protocol that satisfies all correctness
requirements, even under the assumption of atomicity. Moreover, in the model
of Section 26, requirement ME 3J can be strengthened into ME 3Pr, thereby
attaining the best quality criteria in the hierarchy of Figure 3. As pointed
out in Part III, this is not possible when keeping speed independence, even
when dropping atomicity.

The idea is extremely simply. As explained in Section 16, all that is needed
to obtain starvation-freedom is the certainty that when Process ${\rm A}$
reaches the state $\ell_{2}$, it will in fact execute the instruction
$\ell_{2}$. The only thing that can stop Process ${\rm A}$ in state $\ell_{2}$
from executing $\ell_{2}$, is the register ${\it readyA}$ being too busy being
read by Process ${\rm B}$ to find time for being written by Process ${\rm A}$.
Now assume that there exists an amount $t_{0}$ of time, such that, if for a
period of at least $t_{0}$, Process ${\rm A}$ is in state $\ell_{2}$ and the
register ${\it readyA}$ is available, in the sense that it is not being read
by Process ${\rm B}$, then in that period the write action $\ell_{2}$ will
commence. Now further assume that Process ${\rm B}$ will spend a period of at
least $t_{0}$ in its critical or in its noncritical section. Then Process
${\rm A}$ will have enough time to perform the action ${\it readyA}:={\it
true}$, and starvation-freedom is ensured. This is the speed-dependent version
of Peterson’s protocol I propose. In fact I cannot exclude that mutual
exclusion protocols work in practice exactly because timing constraints such
as sketched above are always met.

The above solution is sufficiently clear not to need mathematical proof.
Nevertheless I proceed with an implementation of the above idea in process
algebra. The goal of this is mostly to see which process algebra we need to
formalise time-dependent reasoning such as performed above. Naturally a timed
process algebra that associates real numbers to various passages of time would
be entirely equipped for this task. However, I will show that the idea can
already be formalised in a realm of untimed process algebra, in the sense that
the progress of time is not quantified.

###  24\. CCS with Time-outs

Following [Gla21, Gla20a], my process algebra will be CCSt, which is CCS, as
presented in Section 4.3, but with $\alpha$ ranging over
$Act:=\A\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\bar{\A}\stackrel{{\scriptstyle\mbox{\huge.}}}{{\cup}}\\{\tau,{\rm
t}\\}$, with ${\rm t}$ a fresh _time-out action_. Relabellings $f$ extend to
this extended set of actions $Act$ by $f({\rm t}):={\rm t}$. The
interpretation of this language as an LTSC proceeds exactly as in Section 4.4.

All actions $\alpha\in Act$ are assumed to occur instantaneously. The time-out
action ${\rm t}$ models the end of a time-consuming activity from which we
abstract. When a system arrives in a state $P$, and at that time $X$ is the
set of actions allowed (= not blocked) by the environment, there are two
possibilities. If $P$ has an outgoing transition $t$ with $\ell(t)\in
X\cup\\{\tau\\}$, the system immediately takes one of the outgoing transitions
$t$ with $\ell(t)\in X\cup\\{\tau\\}$, without spending any time in state $P$.
The choice between these transitions is entirely nondeterministic. The system
cannot immediately take a transition $t$ with $\ell(t)\in A{\setminus}X$,
because the action $\ell(t)$ is blocked by the environment. Neither can it
immediately take a transition $t$ with $\ell(t)={\rm t}$, because such
transitions model the end of an activity with a finite but positive duration
that started when reaching state $P$.

In case $P$ has no outgoing transition $t$ with $\ell(t)\in X\cup\\{\tau\\}$,
the system idles in state $P$ for a positive amount of time. This idling can
end in two possible ways. Either one of the time-out transitions
$P\mathrel{\hbox{$\mathop{\hbox to13.50002pt{\rightarrowfill}}\limits^{\hbox
to13.50002pt{\hfil\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle{\rm
t}$\hskip 2.25pt}\hfil}}$}}Q$ occurs, or the environment spontaneously changes
the set of actions it allows into a different set $Y$ with the property that
$P\mathrel{\hbox{$\mathop{\hbox to13.50002pt{\rightarrowfill}}\limits^{\hbox
to13.50002pt{\hfil\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle
a$\hskip 2.25pt}\hfil}}$}}Q$ for some $a\in Y$. In the latter case a
transition $t$ with $\textit{src\/}(t)=P$ and $a\in Y$ occurs. The choice
between the various ways to end a period of idling is entirely
nondeterministic. It is possible to stay forever in state $P$ only if there
are no outgoing time-out transitions.

A fundamental law describing the interaction between $\tau$\- and ${\rm
t}$-transitions, motivated by the above, is $\tau.P+{\rm t}.Q=\tau.P$. It says
that when faced with a choice between a $\tau$\- and a ${\rm t}$-transition, a
system will never take the ${\rm t}$-transition. I could have devised an
operational semantics of CCSt, featuring negative premises, that suppresses
the generation of transitions $R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to22.84904pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle~{}{\rm
t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;C}~{}$\hskip
2.25pt}}$}}}Q$ when there is a transition
$R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to23.59062pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip
2.25pt$\scriptstyle~{}\tau{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;D}~{}$\hskip
2.25pt}}$}}}P$. However, following [Gla21, Gla20a], I take a different, and
simpler, approach. The operational semantics of CCSt is exactly like the one
of CCS, and generates such spurious transitions
$R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to22.84904pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle~{}{\rm
t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;C}~{}$\hskip
2.25pt}}$}}}Q$; instead, its semantics assures that these transitions are
never taken. In [Gla20a] a branching time semantics is proposed, and in
[Gla21] a linear-time semantics—the closest approximation of partial trace
semantics [Gla01] that yields a congruence for the operators of CCSt. Both
these semantics satisfy $\tau.P+{\rm t}.Q=\tau.P$.

Here I achieve the same by calling a path _potentially complete_ when it
features no transitions $R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to22.84904pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle~{}{\rm
t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;C}~{}$\hskip
2.25pt}}$}}}Q$ when there also exists a transition
$R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to23.59062pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip
2.25pt$\scriptstyle~{}\tau{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;D}~{}$\hskip
2.25pt}}$}}}P$. A completeness criterion now should set apart a subset of the
potentially complete paths as being complete. So all paths containing spurious
transitions $R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to22.84904pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle~{}{\rm
t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;C}~{}$\hskip
2.25pt}}$}}}Q$ count as incomplete, and hence do not contribute to the
evaluation of judgements in reactive temporal logic. In depictions of LTSs for
fragments of CCSt I will display the spurious transitions dotted, to emphasise
that they can not be taken.

A transition $R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to22.84904pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip 2.25pt$\scriptstyle~{}{\rm
t}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;C}~{}$\hskip
2.25pt}}$}}}Q$ also cannot be taken when there is an alternative
$R\mathrel{\mathrel{\hbox{$\mathop{\hbox
to24.16666pt{\rightarrowfill}}\limits^{\hbox{\vrule
height=5.81247pt,depth=3.09999pt,width=0.0pt\hskip
2.25pt$\scriptstyle~{}a{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\;,\;D}~{}$\hskip
2.25pt}}$}}}P$, with $a$ an action that surely will not be blocked by the
environment when the system is in state $R$. Thus, whether or not a transition
is spurious depends on the mood of the environment at the time this transition
is enabled. This dependency is encoded in the semantic equivalences of [Gla21]
and [Gla20a]. Given this, it was no extra effort to simultaneously inhibit the
selection of transitions that are spurious in any environment.

###  25\. Spurious Transitions and Completeness Criteria for LTSs with Time-
outs

In LTSs with ${\rm t}$-transitions, it makes sense to allow judgements
$P\models^{CC}_{B,E}\varphi$ with $B\subseteq E\subseteq A$, where $A$ is the
set of all actions except $\tau$ and ${\rm t}$. Here $B$ is the set of actions
that can be permanently blocked by the environment, and $E$ the ones that can
be blocked for finite periods of time. My interest is in the cases $CC={\it
Pr}$ and $CC=J$. When taking as default an environment that may block or allow
any action $a\in A$, the annotations $B$ and $E$ rule out those environments
in which an action from $A{\setminus}B$ is blocked permanently, or an action
from $A{\setminus}E$ is blocked temporary.

######  Definition 25.1.

spurious A transition $t$ is _$E$ -spurious_ if $\ell(t)={\rm t}$ and there
exists a transition $u\in\textit{Tr}$ with
$\textit{src\/}(u)=\textit{src\/}(t)$ and
$\ell(u)\in(A{\setminus}E)\cup\\{\tau\\}$. It is _spurious_ iff it is
$A$-spurious.

Note that $t$ is spurious iff it is $E$-spurious for all $E$. This is the case
iff it is a ${\rm t}$-transition sharing its source state with a
$\tau$-transition. When actions from $A{\setminus}E$ cannot be blocked by the
environment, not even temporary, $E$-spurious transitions can not be taken.

######  Definition 25.2.

BEprogresssing A path $\pi$ is _potentially $E$-complete_ if it contains no
$E$-spurious transitions. It is _$B,E$ -progressing_ if it (a) is potentially
$E$-complete, and (b) is either infinite or ends in a state of which all
outgoing transitions have a label from $B$. It is _$B,E$ -just_ if (a) it is
potentially $E$-complete, and (b) for each $t\in\textit{Tr}$ with
$\ell(t)\notin B$ and its source state $s:=\textit{src\/}(t)$ occurring on
$\pi$, any suffix of $\pi$ starting at $s$ contains a transition $u$ with
$t\mathrel{\mbox{$\,\not\\!\smile\raisebox{3.1pt}{$\scriptscriptstyle\bullet$}$}}u$.

The judgement $s\models^{\it Pr}_{B,E}\varphi$ (resp. $s\models^{\it
J}_{B,E}\varphi$) holds if $\pi\models\varphi$ holds for all $B,E$-progressing
(resp. $B,E$-just) paths $\pi$ starting in $s$.

For a finite path to be complete, its last state may have outgoing transitions
with labels from $B$ only, for a run comes to an end only when all subsequent
activity is permanently blocked by the environment. In the absence of ${\rm
t}$-transitions, judgements $s\models^{\it CC}_{B,E}\varphi$ are independent
of $E$, and agree with the ones defined in Part I of this paper.

In the context of the present paper, when describing properties for a given or
desired process $P$, I see no reason to combine judgements
$P\models^{CC}_{B,E}\varphi$ with different values of $E$. This suggests
writing $P\models^{CC}_{B,E}\varphi$ as $(P,E)\models^{CC}_{B}\varphi$. This
way, the quality criteria of Sections 11 and 12 can remain unchanged, and
apply to systems $(P,E)$. Here $P$ is a hypothetical fair scheduler or mutual
exclusion protocol, and $E$ the set of its actions that can be temporary
blocked by the environment.

$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{1}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{1}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{1}\end{array}$ lnA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{2}\end{array}$ lnAlnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{3}\end{array}$ lnA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{2}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{2}m_{8}\end{array}$ lnAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{3}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{3}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{4}m_{{\rm
t}}\end{array}$ecB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{6}\end{array}$${\rm t}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{7}\end{array}$lcB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{4}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{5}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{5}m_{8}\end{array}$enB$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{1}\end{array}$ ecA$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{2}\end{array}$ ecAlnB$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{3}\end{array}$ ecA$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm t}}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{{\rm
t}}m_{8}\end{array}$ ecAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{1}\end{array}$ ${\rm t}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{2}\end{array}$ ${\rm t}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{3}\end{array}$ ${\rm t}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{6}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{6}m_{8}\end{array}$ ${\rm t}$enB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{1}\end{array}$ lcA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{2}\end{array}$ lcAlnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{3}\end{array}$ lcA$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{7}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{7}m_{8}\end{array}$ lcAenB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{1}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{2}\end{array}$lnB$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{3}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{4}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{5}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt] \ell_{8}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{6}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{7}\end{array}$$\begin{array}[]{c}B\\\\[-3.0pt]
\ell_{8}m_{8}\end{array}$enB enA enA enA enA$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{1}m_{{\rm
t}}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{6}\end{array}$${\rm t}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{1}m_{8}\end{array}$enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{1}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{2}\end{array}$lnA lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{3}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{4}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{5}\end{array}$lnA $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{2}m_{{\rm
t}}\end{array}$lnA ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{6}\end{array}$lnA ${\rm t}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{7}\end{array}$lnA lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{2}m_{8}\end{array}$lnA enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{3}m_{{\rm
t}}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{6}\end{array}$${\rm t}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{3}m_{8}\end{array}$enB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{4}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{4}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{5}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{5}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{4}\end{array}$ecA $\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm t}}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{{\rm
t}}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{4}\end{array}$t $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{6}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{6}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{2}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{4}\end{array}$lcA $\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{7}m_{{\rm
t}}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{6}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{7}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{7}m_{8}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{1}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{2}\end{array}$lnB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{3}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{4}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{5}\end{array}$$\begin{array}[]{c}A\\\\[-3.0pt] \ell_{8}m_{{\rm
t}}\end{array}$ecB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{6}\end{array}$${\rm t}$$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{7}\end{array}$lcB$\begin{array}[]{c}A\\\\[-3.0pt]
\ell_{8}m_{8}\end{array}$enBenA enA enA enA enA enA enA enA enA

Figure 8. Speed dependent LTS of Peterson’s mutual exclusion algorithm

To gauge the influence of the environment on the visible actions eni, lni, eci
and lci of a mutual exclusion protocol, one can see the processes $i$ that
compete for the critical section as clients that communicate with the protocol
through synchronisation on these actions. As explained in Section 12, the
actions lni belong in $B$ (except when formulating requirement ME 6) because
lni is permanently blocked in case Client $i$ chooses not to leave its
noncritical section again. The actions lci belong in $E$, but not in $B$,
because the client may need some time before leaving its critical section, but
is assumed to do this eventually. As mentioned in Section 12, the actions eci
and eni do not belong in $B$, for we assume the client to eventually enter the
(non)critical section when allowed by the protocol. There is a choice between
putting these actions in $E$ or not. Putting them in $E$ models that the
client may delay a while before entering the critical section when allowed,
whereas putting them in $A{\setminus}E$ models that when the protocol for
Client $i$ is in its _entry_ or _exit_ section, the actual client will
patiently wait until granted access to the (non)critical section, and take
advantage of this opportunity as soon as it arises. Taking
$E=E_{l}:=\\{\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{i}$},\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{i}$}\mid i=1,\dots,N\\}$ appears most natural, but taking
$E=A=\\{\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{i}$},\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{i}$},\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{i}$},\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{i}$}\mid i=1,\dots,N\\}$ is a reasonable alternative. The latter leads
to stronger judgements, in the sense that when a protocol $P$ is correct when
taking $E:=A$, it is surely correct when taking $E:=E_{l}$. To model both
options at the same time, in Figure 8 I will draw $E_{l}$-spurious transitions
dashed. Those transitions cannot be taken when choosing $E:=E_{l}$, but they
can be taken when choosing $E:=A$.

###  26\. Modelling Peterson’s Protocol in CCS with Timeouts

My model of Peterson’s algorithm in CCSt differs from the one from Section 19
in only one way: a ${\rm t}$-action is inserted between eci and lci for
$i={\rm A},{\rm B}$, in the two processes ${\rm A}$ and ${\rm B}$. Thus ${\rm
A}\stackrel{{\scriptstyle{\it
def}}}{{=}}\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
ln${}_{A}$}\mathbin{.}\overline{{\it asgn}_{{\it readyA}}^{\,{\it
true}}}\mathbin{.}\overline{{\it asgn}_{{\it turn}}^{\,B}}\mathbin{.}({\it
n}_{{\it readyB}}^{\,{\it false}}\ +\ {\it n}_{{\it
turn}}^{\,A})\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
ec${}_{A}$}\mathbin{.}{\rm
t}\mathbin{.}\mbox{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\it
lc${}_{A}$}\mathbin{.}\overline{{\it asgn}_{{\it readyA}}^{\,{\it
false}}}\mathbin{.}\mbox{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\it
en${}_{A}$}\mathbin{.}{\rm A}.$
This models that a process spends a positive but finite amount of time in its
critical section. The LTS of the resulting CCSt rendering of Peterson’s
protocol is displayed in Figure 8. Exactly as in Section 16/19, it follows
that this model satisfies the requirements ME 1, ME 2, ME 4Pr, ME 5J and ME
6J. Additionally, it satisfies ME 3Pr, as follows immediately from the LTS.

The same result would be obtained by letting time pass in the noncritical
section, instead of, or in addition to, the critical section. It can argued
that it is not realistic to assume that assignments like $\ell_{2}$ and
$\ell_{3}$ occur instantaneously. However, this part of the modelling in CCSt
is merely an abstraction, and can be taken to mean that the time needed to
execute such an assignment is significantly smaller than the time a process
spends in its critical and/or noncritical section. Using CCSt, one can also
make a model in which time is spend between each two instructions. In such a
rendering one would obtain ME 3J, thus needing justness for starvation-
freedom.

### References

  * [1]
  * [AFK88] K.R. Apt, N. Francez & S. Katz (1988): _Appraising fairness in languages for distributed programming_.  Distributed Computing 2(4), pp. 226–241, 10.1007/BF01872848.
  * [Ara11] A.A. Aravind (2011): _Yet Another Simple Solution for the Concurrent Programming Control Problem_.  IEEE Transactions on Parallel and Distributed Systems 22(6), pp. 1056–1063, 10.1109/TPDS.2010.172.
  * [BC87] G. Boudol & I. Castellani (1987): _On the semantics of concurrency: partial orders and transition systems_.  In H. Ehrig, R. Kowalski, G. Levi & U. Montanari, editors: Proc. TAPSOFT’87, Vol. 1, LNCS 249, Springer, pp. 123–137, 10.1007/3-540-17660-8_52.
  * [BCC+11] F. Buti, M. Callisto De Donato, F. Corradini, M.R. Di Berardini & W. Vogler (2011): _Automated Analysis of MUTEX Algorithms with FASE_.  In G. D’Agostino & S. La Torre, editors: Proc. GandALF’11, Electronic Proceedings in Computer Science 54, Open Publishing Association, pp. 45–59, 10.4204/EPTCS.54.4.
  * [Ber88] J.A. Bergstra (1988): _ACP with signals_.  In J. Grabowski, P. Lescanne & W. Wechler, editors: Proc. International Workshop on Algebraic and Logic Programming, LNCS 343, Springer, pp. 11–20, 10.1007/3-540-50667-5_53.
  * [BGK+19] O. Bunte, J.F. Groote, J.J.A. Keiren, M. Laveaux, T. Neele, E.P. de Vink, W. Wesselink, A. Wijs & T.A.C. Willemse (2019): _The mCRL2 Toolset for Analysing Concurrent Systems—Improvements in Expressivity and Usability_.  In T. Vojnar & L. Zhang, editors: Proc. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’19, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’19, Prague, Czech Republic, LNCS 11428, Springer, pp. 21–39, 10.1007/978-3-030-17465-1_2.
  * [BHR84] S.D. Brookes, C.A.R. Hoare & A.W. Roscoe (1984): _A theory of communicating sequential processes_.  Journal of the ACM 31(3), pp. 560–599, 10.1145/828.833.
  * [BLW20] M.S. Bouwman, B. Luttik & T.A.C. Willemse (2020): _Off-the-shelf automated analysis of liveness properties for just paths_.  Acta Informatica 57(3-5), pp. 551–590, 10.1007/s00236-020-00371-w.
  * [Bou18] M.S. Bouwman (2018): _Liveness analysis in process algebra: simpler techniques to model mutex algorithms_.  Technical Report, Eindhoven University of Technology.  Available at http://www.win.tue.nl/~timw/downloads/bouwman_seminar.pdf.
  * [BW90] J.C.M. Baeten & W.P. Weijland (1990): _Process Algebra_.  Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 10.1017/CBO9780511624193.
  * [CDV06] F. Corradini, M.R. Di Berardini & W. Vogler (2006): _Fairness of Actions in System Computations_.  Artificial Intelligence 43(2), pp. 73–130, 10.1007/s00236-006-0011-2.
  * [CDV09] F. Corradini, M.R. Di Berardini & W. Vogler (2009): _Time and Fairness in a Process Algebra with Non-blocking Reading_.  In M. Nielsen, A. Kucera, P. Bro Miltersen, C. Palamidessi, P. Tuma & F. D. Valencia, editors: Theory and Practice of Computer Science, SOFSEM’09, LNCS 5404, Springer, pp. 193–204, 10.1007/978-3-540-95891-8_20.
  * [DDM87] P. Degano, R. De Nicola & U. Montanari (1987): _CCS is an (augmented) contact free C/E system_.  In M. Venturini Zilli, editor: Advanced School on Mathematical Models for the Semantics of Parallelism, 1986, LNCS 280, Springer, pp. 144–165, 10.1007/3-540-18419-8_13.
  * [DGH17] V. Dyseryn, R.J. van Glabbeek & P. Höfner (2017): _Analysing Mutual Exclusion using Process Algebra with Signals_.  In K. Peters & S. Tini, editors: Proc. Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics, Berlin, Germany, Electronic Proceedings in Theoretical Computer Science 255, Open Publishing Association, pp. 18–34, 10.4204/EPTCS.255.2.
  * [Dij63] E.W. Dijkstra (1962 or 1963): _Over de sequentialiteit van processbeschrijvingen_.  Available at http://www.cs.utexas.edu/users/EWD/ewd00xx/EWD35.PDF.
  * [Dij65] E.W. Dijkstra (1965): _Solution of a problem in concurrent programming control_.  Communications of the ACM 8(9), p. 569, 10.1145/365559.365617.
  * [DV95] R. De Nicola & F.W. Vaandrager (1995): _Three Logics for Branching Bisimulation_.  Journal of the ACM 42(2), pp. 458–487, 10.1145/201019.201032.
  * [EB96] J. Esparza & G. Bruns (1996): _Trapping Mutual Exclusion in the Box Calculus_.  Theoretical Computer Science 153(1-2), pp. 95–128, 10.1016/0304-3975(95)00119-0.
  * [Fok00] W. J. Fokkink (2000): _Introduction to Process Algebra_.  Texts in Theoretical Computer Science, An EATCS Series, Springer, 10.1007/978-3-662-04293-9.
  * [Fra86] N. Francez (1986): _Fairness_.  Springer, New York, 10.1007/978-1-4612-4886-6.
  * [GGS11] R.J. van Glabbeek, U. Goltz & J.-W. Schicke (2011): _Abstract Processes of Place/Transition Systems_.  Information Processing Letters 111(13), pp. 626–633, 10.1016/j.ipl.2011.03.013.  Available at http://arxiv.org/abs/1103.5916.
  * [GH15a] R.J. van Glabbeek & P. Höfner (2015): _Progress, Fairness and Justness in Process Algebra_.  Technical Report 8501, NICTA, Sydney, Australia.  Available at http://arxiv.org/abs/1501.03268.
  * [GH15b] R.J. van Glabbeek & P. Höfner (2015): _CCS: It’s not fair! - Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions_.  Acta Informatica 52(2-3), pp. 175–205, 10.1007/s00236-015-0221-6.  Available at http://arxiv.org/abs/1505.05964.
  * [GH19] R.J. van Glabbeek & P. Höfner (2019): _Progress, Justness and Fairness_.  ACM Computing Surveys 52(4):69, 10.1145/3329125.  Available at https://arxiv.org/abs/1810.07414.
  * [Gla93] R.J. van Glabbeek (1993): _The Linear Time – Branching Time Spectrum II; The semantics of sequential systems with silent moves_.  In E. Best, editor: Proc. CONCUR’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, LNCS 715, Springer, pp. 66–81, 10.1007/3-540-57208-2_6.
  * [Gla01] R.J. van Glabbeek (2001): _The Linear Time – Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes_.  In J.A. Bergstra, A. Ponse & S.A. Smolka, editors: Handbook of Process Algebra, chapter 1, Elsevier, pp. 3–99, 10.1016/B978-044482830-9/50019-9.
  * [Gla18] R.J. van Glabbeek (2018): _Is Speed-Independent Mutual Exclusion Implementable?_ In S. Schewe & L. Zhang, editors: Proc. 29th International Conference on Concurrency Theory, CONCUR’18, Beijing, China, Leibniz International Proceedings in Informatics (LIPIcs) 118, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 10.4230/LIPIcs.CONCUR.2018.3.
  * [Gla19a] R.J. van Glabbeek (2019): _Justness: A Completeness Criterion for Capturing Liveness Properties (extended abstract)_.  In M. Bojańczyk & A. Simpson, editors: Proc. 22st International Conference on Foundations of Software Science and Computation Structures, FoSSaCS’19; held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS’19, Prague, Czech Republic, LNCS 11425, Springer, pp. 505–522, 10.1007/978-3-030-17127-8_29.
  * [Gla19b] R.J. van Glabbeek (2019): _Ensuring liveness properties of distributed systems: Open problems_.  Journal of Logical and Algebraic Methods in Programming 109:100480, 10.1016/j.jlamp.2019.100480.  Available at http://arxiv.org/abs/1912.05616.
  * [Gla20a] R.J. van Glabbeek (2020): _Reactive Bisimulation Semantics for a Process Algebra with Time-Outs_.  In I. Konnov & L. Kovács, editors: Proceedings 31st International Conference on Concurrency Theory (CONCUR 20), Online, September 2020, Leibniz International Proceedings in Informatics (LIPIcs) 171, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 10.4230/LIPIcs.CONCUR.2020.6.
  * [Gla20b] R.J. van Glabbeek (2020): _Reactive Temporal Logic_.  In O. Dardha & J. Rot, editors: Proc. Combined 27th International Workshop on Expressiveness in Concurrency and 17th Workshop on Structural Operational Semantics, Online, Electronic Proceedings in Theoretical Computer Science 322, Open Publishing Association, pp. 51–68, 10.4204/EPTCS.322.6.
  * [Gla21] R.J. van Glabbeek (2021): _Failure Trace Semantics for a Process Algebra with Time-outs_.  Logical Methods in Computer Science 17(2):11, 10.23638/LMCS-17(2:11)2021.  Available at http://arxiv.org/abs/2002.10814.
  * [GM84] U. Goltz & A. Mycroft (1984): _On the relationship of CCS and Petri nets_.  In J. Paredaens, editor: Proc. $\it 11^{th}$ ICALP, Antwerpen, LNCS 172, Springer, pp. 196–208, 10.1007/3-540-13345-3_18.
  * [GM14] J.F. Groote & M.R. Mousavi (2014): _Modeling and Analysis of Communicating Systems_.  MIT Press.
  * [GPSS80] D.M. Gabbay, A. Pnueli, S. Shelah & J. Stavi (1980): _On the Temporal Analysis of Fairness_.  In P.W. Abrahams, R.J. Lipton & S.R. Bourne, editors: Proc. POPL ’80, ACM Press, pp. 163–173, 10.1145/567446.567462.
  * [GV87] R.J. van Glabbeek & F.W. Vaandrager (1987): _Petri net models for algebraic theories of concurrency (extended abstract)_.  In J.W. de Bakker, A.J. Nijman & P.C. Treleaven, editors: Proc. PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, Vol. II: Parallel Languages, LNCS 259, Springer, pp. 224–242, 10.1007/3-540-17945-3_13.
  * [Hoa85] C.A.R. Hoare (1985): _Communicating Sequential Processes_.  Prentice Hall, Englewood Cliffs.
  * [HR04] M. Huth & M.D. Ryan (2004): _Logic in Computer Science — Modelling and Reasoning about Systems_ , 2nd edition.  Cambridge University Press, 10.1017/CBO9780511810275.
  * [Kle64] L. Kleinrock (1964): _Analysis of A Time-Shared Processor_.  Naval Research Logistics Quarterly 11(1), pp. 59–73, 10.1002/nav.3800110105.
  * [Knu66] D.E. Knuth (1966): _Additional comments on a problem in concurrent programming control_.  Communications of the ACM 9(5), pp. 321–322, 10.1145/355592.365595.
  * [KW97] E. Kindler & R. Walter (1997): _Mutex Needs Fairness_.  Information Processing Letters 62(1), pp. 31–39, 10.1016/S0020-0190(97)00033-1.
  * [Lam74] L. Lamport (1974): _A New Solution of Dijkstra’s Concurrent Programming Problem_.  Communications of the ACM 17(8), pp. 453–455, 10.1145/361082.361093.
  * [Lam77] L. Lamport (1977): _Proving the correctness of multiprocess programs_.  IEEE Transactions on Software Engineering 3(2), pp. 125–143, 10.1109/TSE.1977.229904.
  * [Lam83] L. Lamport (1983): _What good is temporal logic?_ In R.E. Mason, editor: Information Processing 83, North-Holland, pp. 657–668.
  * [Lam86] L. Lamport (1986): _On Interprocess Communication. Part II: Algorithms_.  Distributed Computing 1(2), pp. 86–101, 10.1007/BF01786228.
  * [LPZ85] O. Lichtenstein, A. Pnueli & L.D. Zuck (1985): _The Glory of the Past_.  In R. Parikh, editor: Proc. Workshop on Logics of Programs, Brooklyn College, New York, NY, USA, LNCS 193, Springer, pp. 196–218, 10.1007/3-540-15648-8_16.
  * [Mil90] R. Milner (1990): _Operational and algebraic semantics of concurrent processes_.  In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242.  Alternatively see Communication and Concurrency, Prentice-Hall, Englewood Cliffs, 1989, of which an earlier version appeared as A Calculus of Communicating Systems, LNCS 92, Springer, 1980, doi:10.1007/3-540-10235-3.
  * [Nag85] J. Nagle (1985): _On Packet Switches with Infinite Storage_.  RFC 970, Network Working Group.  Available at http://tools.ietf.org/rfc/rfc970.txt.
  * [Nag87] J. Nagle (1987): _On Packet Switches with Infinite Storage_.  IEEE Trans. Communications 35(4), pp. 435–438, 10.1109/TCOM.1987.1096782.
  * [NPW81] M. Nielsen, G.D. Plotkin & G. Winskel (1981): _Petri nets, event structures and domains, part I_.  Theoretical Computer Science 13(1), pp. 85–108, 10.1016/0304-3975(81)90112-2.
  * [Old87] E.-R. Olderog (1987): _Operational Petri net semantics for CCSP_.  In G. Rozenberg, editor: Advances in Petri Nets 1987, LNCS 266, Springer, pp. 196–223, 10.1007/3-540-18086-9_27.
  * [Pet81] G.L. Peterson (1981): _Myths About the Mutual Exclusion Problem_.  Information Processing Letters 12(3), pp. 115–116, 10.1016/0020-0190(81)90106-X.
  * [Pnu77] Amir Pnueli (1977): _The Temporal Logic of Programs_.  In: Foundations of Computer Science, FOCS’77, IEEE, pp. 46–57, 10.1109/SFCS.1977.32.
  * [Ray13] M. Raynal (2013): _Concurrent Programming - Algorithms, Principles, and Foundations_.  Springer, 10.1007/978-3-642-32027-9.
  * [SGG12] A. Silberschatz, P.B. Galvin & G. Gagne (2012): _Operating System Concepts, 9th Edition_.  Wiley.  Available at http://os-book.com/OS9/index.html.
  * [Spr21] M.S.C. Spronck (2021): _Safe registers and Aravind’s BLRU algorithm for mutual exclusion in mCRL2_.  Technical Report, Eindhoven University of Technology.  Available at https://www.win.tue.nl/~luttik/BRP/Myrthe_Spronck.pdf.
  * [Szy88] B.K. Szymański (1988): _A simple solution to Lamport’s concurrent programming problem with linear wait_.  In J. Lenfant, editor: Proc. 2nd international conference on Supercomputing, ICS’88, Saint Malo, France, ACM, pp. 621–626, 10.1145/55364.55425.
  * [Vog02] W. Vogler (2002): _Efficiency of asynchronous systems, read arcs, and the MUTEX-problem_.  Theoretical Computer Science 275(1-2), pp. 589–631, 10.1016/S0304-3975(01)00300-0.
  * [VS96] A. Valmari & M. Setälä (1996): _Visual Verification of Safety and Liveness_.  In M.-C. Gaudel & J. Woodcock, editors: Industrial Benefit and Advances in Formal Methods, FME’96, LNCS 1051, Springer, pp. 228–247, 10.1007/3-540-60973-3_90.
  * [Wal89] D. J. Walker (1989): _Automated analysis of mutual exclusion algorithms using CCS_.  Formal Aspects of Computing 1(1), pp. 273–292, 10.1007/BF01887209.
  * [Win87] G. Winskel (1987): _Event structures_.  In W. Brauer, W. Reisig & G. Rozenberg, editors: Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255, Springer, pp. 325–392, 10.1007/3-540-17906-2_31.