Fairness conditions can be specified in PlusCal adding the
`PlusCal options`

comment immediately before the definition
of the algorithm:

`(* PlusCal options (-sf) *)`

PlusCal proposes three fairness conditions:

`-sf`

for strong fairness`-wf`

for weak fairness`-wfNext`

for weak fairness on the Next relation: processes cannot stay idle forever if the Next action is continuously enabled.

Model-check the following PlusCal model, and explain why it does not satisfy the liveness property

`NoStarvation`

without fairness hypothesis.Is

`NoStarvation`

satisfied under weak fairness assumptions? Justify.Is the property

`NoStarvation`

satisfied under strong fairness assumptions? Justify.

```
EXTENDS Naturals, TLC
CONSTANTS N (* Number of processes *)
(*
--algorithm Semaphore {
variables s = 1; (* Shared semaphore counter *)
macro P(sem) { await sem > 0; sem := sem - 1 }
macro V(sem) { sem := sem + 1 }
process (P \in 1..N)
{
loop: while (TRUE) {
lock: P(s);
cs: skip; (* In the critical section *)
unlock: V(s)
}
}
}
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
(* Atomic propositions *)
CS(p) == (pc[p] = "cs")
REQ(p) == (pc[p] = "lock")
(* In every state, there is at most one process in the critical section *)
Mutex == [](\A p \in 1..N: \A q \in (1..N \{p}): ~(CS(p) /\ CS(q)))
(* Every process that tries to enter the critical section is eventually granted the
access to the critical section
*)
NoStarvation == \A p \in 1..N: [](REQ(p) => <>CS(p))
```

- Explain why the model below does not guarantee requirement
`NoStarvation`

, even under strong fairness hypothesis.

```
EXTENDS Naturals, TLC
CONSTANTS N (* Number of processes *)
(* PlusCal options (-sf) *)
(*
--algorithm Semaphore {
variables s = 1; (* Shared semaphore counter *)
process (P \in 1..N)
variables go = FALSE; (* Clearing flag *)
{
loop: while (TRUE) {
lock: if (s > 0) { (* Atomic test-and-set *)
s := s-1;
go := TRUE
};
testing: if (go = FALSE) {
goto lock
};
cs: skip; (* In the critical section *)
unlock: s := s+1;
go := FALSE
}
}
}
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
(* Atomic propositions *)
CS(p) == (pc[p] = "cs")
REQ(p) == (pc[p] = "lock")
(* In every state, there is at most one process in the critical section *)
Mutex == [](\A p \in 1..N: \A q \in (1..N \{p}): ~(CS(p) /\ CS(q)))
(* Every process that tries to enter the critical section is eventually granted the
access to the critical section *)
NoStarvation == \A p \in 1..N: [](REQ(p) => <>CS(p))
```

In real life implementations, semaphores have to guarantee fairness. Hence semaphores are not implemented as simple integer variables. One solution is to implement the semaphore as the FIFO queue of processes blocked on instruction P.

Define the macros P and V in the algorithm below, for a semaphore implemented by a sequence. Recall the operations on sequences:

`<<>>`

is the empty sequence,`Append(s,e)`

returns the sequence obtained by adding`e`

to the tail of sequence`s`

,`Head(s)`

returns the head of non-empty sequence`s`

,`Tail(s)`

returns the tail of non-empty sequence`s`

, and`Len(s)`

returns the length of sequence`s`

.Explain why your model satisfies property

`NoStarvation`

under strong fairness assumption, but not under weak fairness assumption.

```
EXTENDS Naturals, Sequences, TLC
CONSTANTS N (* Number of processes *)
(* PlusCal options (-sf) *)
(*
--algorithm Semaphore {
variables s = <<>>; (* Shared semaphore counter *)
macro P(sem) { ... }
macro V(sem) { ... }
process (P \in 1..N)
{
loop: while (TRUE) {
lock: P(s);
cs: skip; (* In the critical section *)
unlock: V(s)
}
}
}
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
(* Atomic propositions *)
CS(p) == (pc[p] = "cs")
REQ(p) == (pc[p] = "lock")
(* In every state, there is at most one process in the critical section *)
Mutex == [](\A p \in 1..N: \A q \in (1..N \{p}): ~(CS(p) /\ CS(q)))
(* Every process that tries to enter the critical section is eventually granted the
access to the critical section
*)
NoStarvation == \A p \in 1..N: [](REQ(p) => <>CS(p))
```

Fix the implementation above in order to obtain an implementation that satisfies all requirements under weak fairness assumption.