--------------------------- MODULE bakery_finite ---------------------------
EXTENDS Naturals,FiniteSets,TLC
CONSTANT N (* Number of processes *)
(* PlusCal options (-wf) *)
(* This model is a finite abstraction of Lamport's bakery algorithm. Ticket numbers
that can grow unboundedly in Lamport's algorithm are abstracted away. Instead of
representing the exact numbers, we keep the ordering over these numbers. This
abstraction is known to be sound and complete. It is also obviously finite.
In this abstraction, we know for each process whether its ticket number is 0 (i.e.
the process is not waiting to access the critical section) or not. We further know
for any two processes how theit ticket numbers compare: <, = or >.
In the following model, we have:
- a set 'zeros' of processes which have number=0
- a circular buffer 'ordering' which stores sets of processes. Assume process P
belongs to ordering[i] and process Q belongs to ordering[j]. Then P and Q have the
same number of i=j. Process P has a smaller number than process Q if i comes before
j in the circular buffer. The first element in the circular buffer is given by
'first'. The number of elements is stored in 'size'.
Operations on the circular buffer 'ordering' and the set 'zeros' are atomic. A
process chooses a number by removing itself from 'zeros' and adding itself into the
first empty set in 'ordering'. Notice that several process may add themselves to the
same set (as in Lamport's algorithm: processes may choose the same number). Thus, the
size of 'ordering' is adjusted by the first process added to a set.
A process sets its number back to 0 by removing itself from the first set and adding
itself to zeros. The circular buffer is updated when the first set became empty.
*)
(*
--algorithm LamportBakery_Finite {
variables choosing = [ i \in 1..N |-> FALSE ]; (* Choosing a number? *)
ordering = [ i \in 0..N-1 |-> {} ]; (* Ordering over processes, circular buffer *)
first = 0; (* Index of first element *)
size = 0; (* Size of circular buffer *)
zeros = (1..N); (* Processes with number 0 *)
define {
HAS_NUMBER_0(p) == (p \in zeros)
HAS_SMALLER_NUMBER(p,q) == /\ ~HAS_NUMBER_0(q)
/\ \/ HAS_NUMBER_0(p)
\/ LET ip == CHOOSE k \in 0..N-1 : p \in ordering[k] IN
LET iq == CHOOSE k \in 0..N-1 : q \in ordering[k] IN
\/ /\ (first <= ip) (* first <= ip < iq *)
/\ (ip < iq)
\/ /\ (iq < first) (* iq < first <= ip *)
/\ (first <= ip)
\/ /\ (ip < iq) (* ip < iq < first *)
/\ (iq < first)
HAS_SAME_NUMBER(p,q) == \/ /\ HAS_NUMBER_0(p)
/\ HAS_NUMBER_0(q)
\/ /\ ~HAS_NUMBER_0(p)
/\ ~HAS_NUMBER_0(q)
/\ LET ip == CHOOSE k \in 0..N-1 : p \in ordering[k] IN
LET iq == CHOOSE k \in 0..N-1 : q \in ordering[k] IN
ip = iq
}
process (P \in 1..N)
variables j;
{
loop: while (TRUE) {
(* Obtaining an access number *)
l01: choosing[self] := TRUE;
l02: j := (first + size) % N; (* first empty set in ordering *)
l05: ordering := [ordering EXCEPT ![j] = (ordering[j] \cup {self})];
if (ordering[j] = {self}) {
size := size + 1;
};
zeros := zeros \ {self};
l07: choosing[self] := FALSE;
(* Waiting my turn *)
l08: j := 1 ;
l09: while (j <= N) {
if (j # self) {
l10: await ~choosing[j];
l11: await (HAS_NUMBER_0(j) \/
HAS_SMALLER_NUMBER(self, j) \/
(HAS_SAME_NUMBER(self, j) /\ (self < j)))
};
l12: j := j+1
};
cs: skip; (* In CS *)
l13: zeros := zeros \cup {self};
assert(self \in ordering[first]);
ordering := [ordering EXCEPT ![first] = (ordering[first] \ {self})];
if (ordering[first] = {}) {
first := (first + 1) % N;
size := size - 1;
}
}
}
}
*)
\* BEGIN TRANSLATION
CONSTANT defaultInitValue
VARIABLES choosing, ordering, first, size, zeros, pc
(* define statement *)
HAS_NUMBER_0(p) == (p \in zeros)
HAS_SMALLER_NUMBER(p,q) == /\ ~HAS_NUMBER_0(q)
/\ \/ HAS_NUMBER_0(p)
\/ LET ip == CHOOSE k \in 0..N-1 : p \in ordering[k] IN
LET iq == CHOOSE k \in 0..N-1 : q \in ordering[k] IN
\/ /\ (first <= ip)
/\ (ip < iq)
\/ /\ (iq < first)
/\ (first <= ip)
\/ /\ (ip < iq)
/\ (iq < first)
HAS_SAME_NUMBER(p,q) == \/ /\ HAS_NUMBER_0(p)
/\ HAS_NUMBER_0(q)
\/ /\ ~HAS_NUMBER_0(p)
/\ ~HAS_NUMBER_0(q)
/\ LET ip == CHOOSE k \in 0..N-1 : p \in ordering[k] IN
LET iq == CHOOSE k \in 0..N-1 : q \in ordering[k] IN
ip = iq
VARIABLE j
vars == << choosing, ordering, first, size, zeros, pc, j >>
ProcSet == (1..N)
Init == (* Global variables *)
/\ choosing = [ i \in 1..N |-> FALSE ]
/\ ordering = [ i \in 0..N-1 |-> {} ]
/\ first = 0
/\ size = 0
/\ zeros = (1..N)
(* Process P *)
/\ j = [self \in 1..N |-> defaultInitValue]
/\ pc = [self \in ProcSet |-> "loop"]
loop(self) == /\ pc[self] = "loop"
/\ pc' = [pc EXCEPT ![self] = "l01"]
/\ UNCHANGED << choosing, ordering, first, size, zeros, j >>
l01(self) == /\ pc[self] = "l01"
/\ choosing' = [choosing EXCEPT ![self] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "l02"]
/\ UNCHANGED << ordering, first, size, zeros, j >>
l02(self) == /\ pc[self] = "l02"
/\ j' = [j EXCEPT ![self] = (first + size) % N]
/\ pc' = [pc EXCEPT ![self] = "l05"]
/\ UNCHANGED << choosing, ordering, first, size, zeros >>
l05(self) == /\ pc[self] = "l05"
/\ ordering' = [ordering EXCEPT ![j[self]] = (ordering[j[self]] \cup {self})]
/\ IF ordering'[j[self]] = {self}
THEN /\ size' = size + 1
ELSE /\ TRUE
/\ size' = size
/\ zeros' = zeros \ {self}
/\ pc' = [pc EXCEPT ![self] = "l07"]
/\ UNCHANGED << choosing, first, j >>
l07(self) == /\ pc[self] = "l07"
/\ choosing' = [choosing EXCEPT ![self] = FALSE]
/\ pc' = [pc EXCEPT ![self] = "l08"]
/\ UNCHANGED << ordering, first, size, zeros, j >>
l08(self) == /\ pc[self] = "l08"
/\ j' = [j EXCEPT ![self] = 1]
/\ pc' = [pc EXCEPT ![self] = "l09"]
/\ UNCHANGED << choosing, ordering, first, size, zeros >>
l09(self) == /\ pc[self] = "l09"
/\ IF j[self] <= N
THEN /\ IF j[self] # self
THEN /\ pc' = [pc EXCEPT ![self] = "l10"]
ELSE /\ pc' = [pc EXCEPT ![self] = "l12"]
ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
/\ UNCHANGED << choosing, ordering, first, size, zeros, j >>
l12(self) == /\ pc[self] = "l12"
/\ j' = [j EXCEPT ![self] = j[self]+1]
/\ pc' = [pc EXCEPT ![self] = "l09"]
/\ UNCHANGED << choosing, ordering, first, size, zeros >>
l10(self) == /\ pc[self] = "l10"
/\ ~choosing[j[self]]
/\ pc' = [pc EXCEPT ![self] = "l11"]
/\ UNCHANGED << choosing, ordering, first, size, zeros, j >>
l11(self) == /\ pc[self] = "l11"
/\ (HAS_NUMBER_0(j[self]) \/
HAS_SMALLER_NUMBER(self, j[self]) \/
(HAS_SAME_NUMBER(self, j[self]) /\ (self < j[self])))
/\ pc' = [pc EXCEPT ![self] = "l12"]
/\ UNCHANGED << choosing, ordering, first, size, zeros, j >>
cs(self) == /\ pc[self] = "cs"
/\ TRUE
/\ pc' = [pc EXCEPT ![self] = "l13"]
/\ UNCHANGED << choosing, ordering, first, size, zeros, j >>
l13(self) == /\ pc[self] = "l13"
/\ zeros' = (zeros \cup {self})
/\ Assert((self \in ordering[first]),
"Failure of assertion at line 96, column 8.")
/\ ordering' = [ordering EXCEPT ![first] = (ordering[first] \ {self})]
/\ IF ordering'[first] = {}
THEN /\ first' = (first + 1) % N
/\ size' = size - 1
ELSE /\ TRUE
/\ UNCHANGED << first, size >>
/\ pc' = [pc EXCEPT ![self] = "loop"]
/\ UNCHANGED << choosing, j >>
P(self) == loop(self) \/ l01(self) \/ l02(self) \/ l05(self) \/ l07(self)
\/ l08(self) \/ l09(self) \/ l12(self) \/ l10(self)
\/ l11(self) \/ cs(self) \/ l13(self)
Next == (\E self \in 1..N: P(self))
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in 1..N : WF_vars(P(self))
\* END TRANSLATION
(* Atomic propositions *)
CS(i) == pc[i] = "cs"
REQ(i) == pc[i] = "l01"
(* 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)))
(* Evry 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))
=============================================================================
\* Modification History
\* Last modified Tue Nov 06 14:07:54 CET 2018 by herbrete
\* Created Mon Nov 05 15:36:27 CET 2018 by herbrete