Model-checking under fairness assumptions

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.

Unfair semaphore

1. Model-check the following PlusCal model, and explain why it does not satisfy the liveness property NoStarvation without fairness hypothesis.

2. Is NoStarvation satisfied under weak fairness assumptions? Justify.

3. 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))

Another unfair semaphore

1. 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))

An unfair semaphore once again

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.

1. Define the macros P and V in the algorithm below, with the semaphore implemented as a FIFO queue of blocked processes, using TLA+ sequences. As a remainder:
   • <<>> 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.
2. 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))

Fair semaphore

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