diff --git a/.ciignore b/.ciignore index efb4c0f9..c625645d 100644 --- a/.ciignore +++ b/.ciignore @@ -11,3 +11,6 @@ specifications/CCF specifications/azure-cosmos-tla specifications/microwave +# Basic contribution only +specifications/barriers +specifications/locks_auxiliary_vars \ No newline at end of file diff --git a/specifications/barriers/Barrier.cfg b/specifications/barriers/Barrier.cfg new file mode 100644 index 00000000..9cd85b6e --- /dev/null +++ b/specifications/barriers/Barrier.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 6 +SPECIFICATION Spec +INVARIANT TypeOK +PROPERTY BarrierProperty \ No newline at end of file diff --git a/specifications/barriers/Barrier.tla b/specifications/barriers/Barrier.tla new file mode 100644 index 00000000..71b30076 --- /dev/null +++ b/specifications/barriers/Barrier.tla @@ -0,0 +1,40 @@ +------------------------------- MODULE Barrier -------------------------------- +EXTENDS Integers + +CONSTANTS + N + +VARIABLES pc + +vars == << pc >> + +ProcSet == (1..N) + +Init == + /\ pc = [p \in ProcSet |-> "b0"] + +b0(self) == + /\ pc[self] = "b0" + /\ pc' = [pc EXCEPT ![self] = "b1"] + +b1 == + /\ \A p \in ProcSet : pc[p] = "b1" + /\ pc' = [p \in ProcSet |-> "b0"] + +Next == + \/ \E p \in ProcSet : b0(p) + \/ b1 + +Spec == Init /\ [][Next]_vars + +------------------------------------------------------------------------------- + +TypeOK == + /\ pc \in [ProcSet -> {"b0", "b1"}] + +\* A process cannot leave the barrier if there are still other processes +\* that need to enter it +BarrierProperty == + /\ [][\A p,q \in ProcSet : pc[p] = "b0" /\ pc[q] = "b1" => pc'[q] = "b1"]_vars + +=============================================================================== \ No newline at end of file diff --git a/specifications/barriers/Barriers.cfg b/specifications/barriers/Barriers.cfg new file mode 100644 index 00000000..47ce272a --- /dev/null +++ b/specifications/barriers/Barriers.cfg @@ -0,0 +1,4 @@ +CONSTANT N = 6 +SPECIFICATION Spec +INVARIANTS TypeOK LockInv Inv FlushInv +PROPERTY BSpec \ No newline at end of file diff --git a/specifications/barriers/Barriers.tla b/specifications/barriers/Barriers.tla new file mode 100644 index 00000000..0ee8d9b9 --- /dev/null +++ b/specifications/barriers/Barriers.tla @@ -0,0 +1,1311 @@ +------------------------------- MODULE Barriers ------------------------------- + +EXTENDS TLAPS, Integers, FiniteSets, FiniteSetTheorems + +CONSTANTS + N + +(** +--algorithm Barriers { + variables + lock = 1, \* lock variable used for critical sections + gate_1 = 0, \* semaphore for the first chamber + gate_2 = 0, \* semaphore for the second chamber + rdv = 0; \* counts the processes entering/leaving the barrier + + macro Lock(l) { + await l = 1; + l := 0; + } + + macro Unlock(l) { + l := 1; + } + + macro Wait(s) { + await s > 0; + s := s - 1; + } + + macro Signal(s) { + s := s + N; + } + + \* The algorithm uses two waiting chambers which wait for all processes to + \* to enter before allowing them to continue. + \* The usage of two chambers ensures no process can leave the barrier and + \* pass through the whole barrier again while blocking others inside. + process (proc \in 1..N) { +a0: while (TRUE) { + skip; \* Some code + \* first waiting chamber a1-a6 +a1: Lock(lock); +a2: rdv := rdv + 1; \* protect read/write of shared variable with a lock +a3: if (rdv = N) { + \* when all processes are in the first chamber +a4: Signal(gate_1); + \* open the chamber + }; +a5: Unlock(lock); +a6: Wait(gate_1); + \* second waiting chamber a7-a12 +a7: Lock(lock); +a8: rdv := rdv - 1; \* protect read/write of shared variable with a lock +a9: if (rdv = 0) { + \* when all processes are in the second chamber +a10: Signal(gate_2); + \* open the chamber + }; +a11: Unlock(lock); +a12: Wait(gate_2); + } + } +} +**) +\* BEGIN TRANSLATION (chksum(pcal) = "7a2331f4" /\ chksum(tla) = "4cd2e9fd") +VARIABLES pc, lock, gate_1, gate_2, rdv + +vars == << pc, lock, gate_1, gate_2, rdv >> + +ProcSet == (1..N) + +Init == (* Global variables *) + /\ lock = 1 + /\ gate_1 = 0 + /\ gate_2 = 0 + /\ rdv = 0 + /\ pc = [self \in ProcSet |-> "a0"] + +a0(self) == /\ pc[self] = "a0" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "a1"] + /\ UNCHANGED << lock, gate_1, gate_2, rdv >> + +a1(self) == /\ pc[self] = "a1" + /\ lock = 1 + /\ lock' = 0 + /\ pc' = [pc EXCEPT ![self] = "a2"] + /\ UNCHANGED << gate_1, gate_2, rdv >> + +a2(self) == /\ pc[self] = "a2" + /\ rdv' = rdv + 1 + /\ pc' = [pc EXCEPT ![self] = "a3"] + /\ UNCHANGED << lock, gate_1, gate_2 >> + +a3(self) == /\ pc[self] = "a3" + /\ IF rdv = N + THEN /\ pc' = [pc EXCEPT ![self] = "a4"] + ELSE /\ pc' = [pc EXCEPT ![self] = "a5"] + /\ UNCHANGED << lock, gate_1, gate_2, rdv >> + +a4(self) == /\ pc[self] = "a4" + /\ gate_1' = gate_1 + N + /\ pc' = [pc EXCEPT ![self] = "a5"] + /\ UNCHANGED << lock, gate_2, rdv >> + +a5(self) == /\ pc[self] = "a5" + /\ lock' = 1 + /\ pc' = [pc EXCEPT ![self] = "a6"] + /\ UNCHANGED << gate_1, gate_2, rdv >> + +a6(self) == /\ pc[self] = "a6" + /\ gate_1 > 0 + /\ gate_1' = gate_1 - 1 + /\ pc' = [pc EXCEPT ![self] = "a7"] + /\ UNCHANGED << lock, gate_2, rdv >> + +a7(self) == /\ pc[self] = "a7" + /\ lock = 1 + /\ lock' = 0 + /\ pc' = [pc EXCEPT ![self] = "a8"] + /\ UNCHANGED << gate_1, gate_2, rdv >> + +a8(self) == /\ pc[self] = "a8" + /\ rdv' = rdv - 1 + /\ pc' = [pc EXCEPT ![self] = "a9"] + /\ UNCHANGED << lock, gate_1, gate_2 >> + +a9(self) == /\ pc[self] = "a9" + /\ IF rdv = 0 + THEN /\ pc' = [pc EXCEPT ![self] = "a10"] + ELSE /\ pc' = [pc EXCEPT ![self] = "a11"] + /\ UNCHANGED << lock, gate_1, gate_2, rdv >> + +a10(self) == /\ pc[self] = "a10" + /\ gate_2' = gate_2 + N + /\ pc' = [pc EXCEPT ![self] = "a11"] + /\ UNCHANGED << lock, gate_1, rdv >> + +a11(self) == /\ pc[self] = "a11" + /\ lock' = 1 + /\ pc' = [pc EXCEPT ![self] = "a12"] + /\ UNCHANGED << gate_1, gate_2, rdv >> + +a12(self) == /\ pc[self] = "a12" + /\ gate_2 > 0 + /\ gate_2' = gate_2 - 1 + /\ pc' = [pc EXCEPT ![self] = "a0"] + /\ UNCHANGED << lock, gate_1, rdv >> + +proc(self) == a0(self) \/ a1(self) \/ a2(self) \/ a3(self) \/ a4(self) + \/ a5(self) \/ a6(self) \/ a7(self) \/ a8(self) + \/ a9(self) \/ a10(self) \/ a11(self) \/ a12(self) + +Next == (\E self \in 1..N: proc(self)) + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION + +------------------------------------------------------------------------------- + +TypeOK == + /\ lock \in {0, 1} + /\ gate_1 \in Nat + /\ gate_2 \in Nat + /\ rdv \in Int + /\ pc \in [ProcSet -> {"a0", "a1", "a2", "a3", "a4", "a5", "a6", + "a7", "a8", "a9", "a10", "a11", "a12"}] + +lockcs(p) == + pc[p] \in {"a2", "a3", "a4", "a5", "a8", "a9", "a10", "a11"} +ProcsInLockCS == + {p \in ProcSet: lockcs(p)} + +LockInv == + /\ \A i, j \in ProcSet: (i # j) => ~(lockcs(i) /\ lockcs(j)) + /\ (\E p \in ProcSet: lockcs(p)) => lock = 0 + +rdvsection(p) == + pc[p] \in {"a3", "a4", "a5", "a6", "a7", "a8"} +ProcsInRdv == + {p \in ProcSet : rdvsection(p)} + +barrier1(p) == + pc[p] \in {"a0", "a1", "a2", "a3", "a4", "a5", "a6"} +ProcsInB1 == + {p \in ProcSet : barrier1(p)} + +barrier2(p) == + pc[p] \in {"a7", "a8", "a9", "a10", "a11", "a12"} +ProcsInB2 == + {p \in ProcSet : barrier2(p)} + +Inv == + \* the semaphore values are kept between 0 and N + /\ gate_1 \in 0..N + /\ gate_2 \in 0..N + \* rdv is the amount of processes in ]a2 ; a8] + /\ rdv = Cardinality(ProcsInRdv) \* proves that rdv \in 0..N + \* open gates mean that at least one process must be in the correct + \* waiting section + /\ gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"} + /\ gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"} + \* at least one gate must be closed + /\ (gate_1 = 0) \/ (gate_2 = 0) + \* if one process in the first barrier (or about to enter), + \* then second barrier must be empty + /\ (\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + \* if one process in second barrier, then first barrier must be empty + /\ (\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + \* The value of gate_1 is bounded by the count of processes + \* in the first barrier + /\ gate_1 =< Cardinality(ProcsInB1) + \* if one process arrives at the first barrier, the first gate is locked + /\ (\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0 + \* if one process is in a4, that means rdv is equal to N and + \* all other processes are waiting on gate_1 + /\ \A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ) + \* The value of gate_2 is bounded by the count of processes + \* in the second barrier + /\ gate_2 =< Cardinality(ProcsInB2) + \* if one process arrives at the second barrier, the second gate is locked + /\ (\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0 + \* if one process is in a10, that means rdv is equal to 0 and + \* all other processes are waiting on gate_2 + /\ \A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ) + +FlushInv == + /\ gate_1 > 0 => gate_1 = Cardinality(ProcsInB1) + /\ gate_2 > 0 => gate_2 = Cardinality(ProcsInB2) + +pc_translation(self) == + IF pc[self] \in {"a1", "a2", "a3", "a4", "a5", "a6", "a7", "a8", "a9", "a10"} + THEN "b1" + ELSE IF pc[self] = "a0" + THEN "b0" + ELSE IF gate_2 > 0 + THEN "b0" + ELSE "b1" + +B == INSTANCE Barrier WITH pc <- [p \in ProcSet |-> pc_translation(p)] +BSpec == B!Spec + +------------------------------------------------------------------------------- + +ASSUME N_Assumption == N \in Nat \ {0} + +LEMMA Typing == Spec => []TypeOK + <1> USE N_Assumption DEF TypeOK + <1>1. Init => TypeOK + BY DEF Init + <1>2. TypeOK /\ [Next]_vars => TypeOK' + BY DEF Next, proc, vars, + a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12 + <1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +LEMMA LockExclusion == Spec => []LockInv + <1> USE DEF LockInv, lockcs, TypeOK + <1>1. Init => LockInv + BY DEF Init + <1>2. LockInv /\ TypeOK /\ [Next]_vars => LockInv' + <2> SUFFICES ASSUME LockInv /\ TypeOK /\ [Next]_vars + PROVE LockInv' + OBVIOUS + <2>1. ASSUME NEW self \in 1..N, a0(self) + PROVE LockInv' + BY <2>1 DEF a0 + <2>2. ASSUME NEW self \in 1..N, a1(self) + PROVE LockInv' + BY <2>2 DEF a1 + <2>3. ASSUME NEW self \in 1..N, a2(self) + PROVE LockInv' + BY <2>3 DEF a2 + <2>4. ASSUME NEW self \in 1..N, a3(self) + PROVE LockInv' + BY <2>4 DEF a3 + <2>5. ASSUME NEW self \in 1..N, a4(self) + PROVE LockInv' + BY <2>5 DEF a4 + <2>6. ASSUME NEW self \in 1..N, a5(self) + PROVE LockInv' + BY <2>6 DEF a5, ProcSet + <2>7. ASSUME NEW self \in 1..N, a6(self) + PROVE LockInv' + BY <2>7 DEF a6 + <2>8. ASSUME NEW self \in 1..N, a7(self) + PROVE LockInv' + BY <2>8 DEF a7 + <2>9. ASSUME NEW self \in 1..N, a8(self) + PROVE LockInv' + BY <2>9 DEF a8 + <2>10. ASSUME NEW self \in 1..N, a9(self) + PROVE LockInv' + BY <2>10 DEF a9 + <2>11. ASSUME NEW self \in 1..N, a10(self) + PROVE LockInv' + BY <2>11 DEF a10 + <2>12. ASSUME NEW self \in 1..N, a11(self) + PROVE LockInv' + BY <2>12 DEF a11, ProcSet + <2>13. ASSUME NEW self \in 1..N, a12(self) + PROVE LockInv' + BY <2>13 DEF a12 + <2>14. CASE UNCHANGED vars + BY <2>14 DEF vars + <2>15. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, + <2>8, <2>9, <2>10, <2>11, <2>12, <2>13, <2>14 + DEF Next, proc, ProcSet + <1>3. QED + BY <1>1, <1>2, PTL, Typing DEF Spec + +LEMMA ProcSetSubSetsBound == + /\ IsFiniteSet(ProcsInRdv) /\ Cardinality(ProcsInRdv) \in 0..N + /\ IsFiniteSet(ProcsInB1) /\ Cardinality(ProcsInB1) \in 0..N + /\ IsFiniteSet(ProcsInB1)' /\ Cardinality(ProcsInB1)' \in 0..N + /\ IsFiniteSet(ProcsInB2) /\ Cardinality(ProcsInB2) \in 0..N + /\ IsFiniteSet(ProcsInB2)' /\ Cardinality(ProcsInB2)' \in 0..N + <1> USE N_Assumption + <1>1. /\ ProcsInRdv \subseteq ProcSet + /\ ProcsInB1 \subseteq ProcSet + /\ ProcsInB1' \subseteq ProcSet + /\ ProcsInB2 \subseteq ProcSet + /\ ProcsInB2' \subseteq ProcSet + BY DEF ProcSet, ProcsInRdv, ProcsInB1, ProcsInB2 + <1>2. /\ IsFiniteSet(ProcSet) + /\ Cardinality(ProcSet) = N + BY FS_Interval DEF ProcSet + <1>3. /\ IsFiniteSet(ProcsInRdv) /\ Cardinality(ProcsInRdv) <= N + /\ IsFiniteSet(ProcsInB1) /\ Cardinality(ProcsInB1) <= N + /\ IsFiniteSet(ProcsInB1)' /\ Cardinality(ProcsInB1)' <= N + /\ IsFiniteSet(ProcsInB2) /\ Cardinality(ProcsInB2) <= N + /\ IsFiniteSet(ProcsInB2)' /\ Cardinality(ProcsInB2)' <= N + BY FS_Subset, <1>1, <1>2 + <1>4. /\ Cardinality(ProcsInRdv) \in 0..N + /\ Cardinality(ProcsInB1) \in 0..N + /\ Cardinality(ProcsInB1)' \in 0..N + /\ Cardinality(ProcsInB2) \in 0..N + /\ Cardinality(ProcsInB2)' \in 0..N + BY <1>3, FS_CardinalityType + <1>5. QED + BY <1>3, <1>4 + +LEMMA AllProcsInRdv == + (Cardinality(ProcsInRdv) = N) => (\A p \in ProcSet : rdvsection(p)) + <1> USE N_Assumption + <1>1. ProcsInRdv \subseteq ProcSet + BY DEF ProcSet, ProcsInRdv + <1>2. /\ IsFiniteSet(ProcSet) + /\ Cardinality(ProcSet) = N + BY FS_Interval DEF ProcSet + <1>3. (Cardinality(ProcsInRdv) = N) => ProcsInRdv = ProcSet + BY <1>1, <1>2, FS_Subset + <1>4. (Cardinality(ProcsInRdv) = N) => (\A p \in ProcSet : rdvsection(p)) + BY <1>3 DEF ProcsInRdv + <1>5. QED + BY <1>4 + +LEMMA AllProcsNotInRdv == + (Cardinality(ProcsInRdv) = 0) => ~(\E p \in ProcSet : rdvsection(p)) + <1> USE N_Assumption + <1>1. IsFiniteSet(ProcsInRdv) + BY ProcSetSubSetsBound, PTL + <1>2. (Cardinality(ProcsInRdv) = 0) => (ProcsInRdv = {}) + BY <1>1, FS_EmptySet + <1>3. (Cardinality(ProcsInRdv) = 0) => ~(\E p \in ProcSet : rdvsection(p)) + BY <1>2 DEF ProcsInRdv + <1>4. QED + BY <1>3 + +THEOREM FS_NonEmptySet == + ASSUME NEW S, IsFiniteSet(S) + PROVE Cardinality(S) > 0 <=> \E x: x \in S + BY FS_EmptySet, FS_CardinalityType + +THEOREM FS_TwoElements == + ASSUME NEW S, IsFiniteSet(S) + PROVE Cardinality(S) > 1 => \E x, y \in S: x # y + <1> SUFFICES ASSUME Cardinality(S) > 1 + PROVE \E x, y \in S: x # y + OBVIOUS + <1>1. PICK x : x \in S + <2>1. Cardinality(S) > 0 + BY FS_CardinalityType + <2>2. QED + BY <2>1, FS_NonEmptySet + <1>2. PICK y : x # y /\ y \in S + <2> DEFINE T == S \ {x} + <2>1. /\ IsFiniteSet(T) + /\ Cardinality(T) = Cardinality(S) - 1 + BY <1>1, FS_RemoveElement + <2>2. Cardinality(T) > 0 + BY <2>1, FS_CardinalityType + <2>3. \E y : y \in T + BY <2>1, <2>2, FS_NonEmptySet + <2>4. QED + BY <2>3 + <1>3. QED + BY <1>1, <1>2 + +THEOREM Invariant == Spec => []Inv + <1> USE N_Assumption + DEF Inv, lockcs, rdvsection, ProcsInRdv, + barrier1, ProcsInB1, barrier2, ProcsInB2 + <1>1. Init => Inv + <2> SUFFICES ASSUME Init + PROVE Inv + OBVIOUS + <2>1. gate_1 \in 0..N + BY DEF Init + <2>2. gate_2 \in 0..N + BY DEF Init + <2>3. rdv = Cardinality(ProcsInRdv) + BY FS_EmptySet DEF Init + <2>4. gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"} + BY DEF Init + <2>5. gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"} + BY DEF Init + <2>6. (gate_1 = 0) \/ (gate_2 = 0) + BY DEF Init + <2>7. (\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + BY DEF Init + <2>8. (\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + BY DEF Init + <2>9. gate_1 =< Cardinality(ProcsInB1) + BY FS_Subset, FS_Interval DEF Init, ProcSet + <2>10. (\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0 + BY DEF Init + <2>11. \A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ) + BY DEF Init + <2>12. gate_2 =< Cardinality(ProcsInB2) + BY FS_EmptySet DEF Init + <2>13. (\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0 + BY DEF Init + <2>14. \A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ) + BY DEF Init + <2>15. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, + <2>8, <2>9, <2>10, <2>11, <2>12, <2>13, <2>14 + <1>2. Inv /\ TypeOK /\ LockInv /\ [Next]_vars => Inv' + <2> SUFFICES ASSUME Inv, + TypeOK, + LockInv, + [Next]_vars + PROVE Inv' + OBVIOUS + <2>1. ASSUME NEW self \in 1..N, + a0(self) + PROVE Inv' + BY <2>1 DEF a0, TypeOK + <2>2. ASSUME NEW self \in 1..N, + a1(self) + PROVE Inv' + BY <2>2 DEF a1, TypeOK, LockInv + <2>3. ASSUME NEW self \in 1..N, + a2(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>3 DEF a2 + <3>2. (gate_2 \in 0..N)' + BY <2>3 DEF a2 + <3>3. (rdv = Cardinality(ProcsInRdv))' + <4>1. /\ ProcsInRdv \union {self} = ProcsInRdv' + /\ self \notin ProcsInRdv + BY <2>3 DEF a2, ProcSet, TypeOK + <4> HIDE DEF ProcsInRdv + <4>2. /\ IsFiniteSet(ProcsInRdv') + /\ Cardinality(ProcsInRdv') = Cardinality(ProcsInRdv) + 1 + BY <4>1, FS_AddElement, ProcSetSubSetsBound + <4>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>3, <4>2 DEF a2 + <4>4. QED + BY <4>3 + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>3 DEF a2, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>3 DEF a2, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>3 DEF a2 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>3 DEF a2, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>3 DEF a2, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + BY <2>3 DEF a2, TypeOK + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>3 DEF a2, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>3 DEF a2, ProcSet, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + BY <2>3 DEF a2, TypeOK + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>3 DEF a2, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>3 DEF a2, ProcSet, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + + <2>4. ASSUME NEW self \in 1..N, + a3(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>4 DEF a3 + <3>2. (gate_2 \in 0..N)' + BY <2>4 DEF a3 + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>4 DEF a3, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>4 DEF a3, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>4 DEF a3, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>4 DEF a3 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>4 DEF a3, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>4 DEF a3, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + BY <2>4 DEF a3, TypeOK + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>4 DEF a3, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + <4>1. rdv \in 0..N + BY ProcSetSubSetsBound + <4>2. CASE rdv = N + (* + prove that if rdv = N, every other process must be in a6 since + - there cannot be another process except self in the critical sections + - they must be in the rdv section + - cannot be in a7 since self is in a3 (7th invariant item) + *) + <5>1. (pc[self] = "a4")' + BY <2>4, <4>2 DEF a3, ProcSet, TypeOK + <5>2. \A p \in ProcSet : (self # p) => ~lockcs(p) + BY <2>4, <4>2, <5>1 DEF a3, ProcSet, TypeOK, LockInv + <5>3. \A p \in ProcSet : p#self => rdvsection(p) + BY <4>2, AllProcsInRdv + <5>4. ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + BY <2>4 DEF a3, ProcSet + <5>5. \A p \in ProcSet : (self # p) => pc[p] = "a6" + BY <5>2, <5>3, <5>4 DEF ProcSet + <5>6. (\A p \in ProcSet : (self # p) => pc[p] = "a6")' + BY <2>4, <4>2, <5>1, <5>5 DEF a3, ProcSet, TypeOK + <5>7. QED + BY <2>4, <4>2, <5>1, <5>6 DEF a3 + <4>3. CASE rdv < N + (* + prove that if rdv is not N, we cannot have a process in a4 + - self will move to a5 (and others will not change) + - currently none can be there (lock exclusion) + *) + <5>1. (pc[self] = "a5")' + BY <2>4, <4>3 DEF a3, ProcSet, TypeOK + <5>2. ~(\E p \in ProcSet: pc[p] = "a4") + BY <2>4, <4>3 DEF a3, ProcSet, LockInv + <5>3. ~(\E p \in ProcSet: pc[p] = "a4")' + BY <2>4, <4>3, <5>1, <5>2 DEF a3, ProcSet, TypeOK + <5>4. QED + BY <5>3 + <4>5. QED + BY <4>1, <4>2, <4>3 + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + BY <2>4 DEF a3, TypeOK + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>4 DEF a3, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>4 DEF a3, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>5. ASSUME NEW self \in 1..N, + a4(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>5 DEF a4, ProcSet, TypeOK + <3>2. (gate_2 \in 0..N)' + BY <2>5 DEF a4 + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>5 DEF a4, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>5 DEF a4, ProcSet, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>5 DEF a4, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>5 DEF a4, ProcSet, TypeOK + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>5 DEF a4, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>5 DEF a4, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + (* + This part is still true as + - gate_1 will be set to N + - ProcsInB1 must be equal to ProcSet + *) + <4>1. (\A p \in ProcSet : (self # p) => pc[p] = "a6") + BY <2>5 DEF a4, ProcSet + <4>2. (\A p \in ProcSet : (self # p) => pc[p] = "a6")' + BY <2>5, <4>1 DEF a4, ProcSet, TypeOK + <4>3. pc'[self] = "a5" + BY <2>5 DEF a4, ProcSet, TypeOK + <4>4. (\A p \in ProcSet : pc[p] \in {"a5","a6"})' + BY <2>5, <4>2, <4>3 DEF ProcSet + <4>5. ProcsInB1' = ProcSet + BY <4>4 + <4> HIDE DEF ProcsInB1 + <4>6. Cardinality(ProcsInB1)' = N + BY <4>5, FS_Interval DEF ProcSet + <4>7. gate_1' = N + BY <2>5 DEF a4, ProcSet + <4>8. QED + BY <4>6, <4>7 + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>5 DEF a4, ProcSet, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>5 DEF a4, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + BY <2>5 DEF a4, TypeOK + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>5 DEF a4, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>5 DEF a4, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>6. ASSUME NEW self \in 1..N, + a5(self) + PROVE Inv' + BY <2>6 DEF a5, TypeOK + <2>7. ASSUME NEW self \in 1..N, + a6(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>7 DEF a6 + <3>2. (gate_2 \in 0..N)' + BY <2>7 DEF a6 + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>7 DEF a6, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + (* + This stays true since : + - Either gate_1 becomes 0 (the last process leaves the wait) + - Either gate_1 stays > 0 + + In this case there must be at least two processes inside B1 + and they cannot be between a0-a4 (reciprocal of 10th item of Invariant) + so if self moves to a7, there still is a process between a5-a6 + *) + <4>1. CASE gate_1' = 0 + <5>1. QED + BY <4>1 + <4>2. CASE gate_1' > 0 + <5>1. gate_1 >= 2 + BY <2>7, <4>2 DEF a6 + <5>2. Cardinality(ProcsInB1) >= 2 + BY <5>1, ProcSetSubSetsBound + <5>3. \E p, q \in ProcSet : (p # q) /\ p \in ProcsInB1 /\ q \in ProcsInB1 + BY <5>2, ProcSetSubSetsBound, FS_TwoElements + <5>4. ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + BY <5>1 + <5>5. \E p \in ProcSet: (p # self) /\ pc[p] \in {"a5", "a6"} + BY <5>3, <5>4 + <5>6. (\E p \in ProcSet: pc[p] \in {"a5", "a6"})' + BY <2>7, <5>5 DEF a6, ProcSet, TypeOK + <5>7. QED + BY <4>2, <5>6 + <4>3. QED + BY <4>1, <4>2 + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>7 DEF a6 + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>7 DEF a6 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>7 DEF a6, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>7 DEF a6, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + (* + when self goes to a7 + - ProcsInB1 loses one element + - gate_1 decreased by 1 + + so comparision stays true + *) + <4>1. /\ gate_1' + 1 = gate_1 + /\ gate_1 \in Nat /\ gate_1' \in Nat + BY <2>7 DEF a6 + <4>2. /\ ProcsInB1' = ProcsInB1 \ {self} + /\ self \in ProcsInB1 + BY <2>7 DEF a6, ProcSet, TypeOK + <4> HIDE DEF ProcsInB1 + <4>3. /\ Cardinality(ProcsInB1)' + 1 = Cardinality(ProcsInB1) + /\ Cardinality(ProcsInB1)' \in Nat /\ Cardinality(ProcsInB1) \in Nat + BY <4>2, ProcSetSubSetsBound, FS_RemoveElement + <4>4. QED + BY <4>1, <4>3 + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>7 DEF a6, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>7 DEF a6, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + \* gate_2 is and stays 0 and Cardinality is in 0..N + BY <2>7, ProcSetSubSetsBound DEF a6 + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>7 DEF a6 + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>7 DEF a6, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>8. ASSUME NEW self \in 1..N, + a7(self) + PROVE Inv' + BY <2>8 DEF a7, TypeOK, LockInv, ProcSet + <2>9. ASSUME NEW self \in 1..N, + a8(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>9 DEF a8 + <3>2. (gate_2 \in 0..N)' + BY <2>9 DEF a8 + <3>3. (rdv = Cardinality(ProcsInRdv))' + <4>1. /\ ProcsInRdv \ {self} = ProcsInRdv' + /\ self \in ProcsInRdv + BY <2>9 DEF a8, ProcSet, TypeOK + <4> HIDE DEF ProcsInRdv + <4>2. /\ IsFiniteSet(ProcsInRdv') + /\ Cardinality(ProcsInRdv') = Cardinality(ProcsInRdv) - 1 + BY <4>1, FS_RemoveElement, ProcSetSubSetsBound + <4>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>9, <4>2 DEF a8 + <4>4. QED + BY <4>3 + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>9 DEF a8, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>9 DEF a8, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>9 DEF a8 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>9 DEF a8, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>9 DEF a8, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + BY <2>9 DEF a8, TypeOK + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>9 DEF a8, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>9 DEF a8, ProcSet, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + BY <2>9 DEF a8, TypeOK + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>9 DEF a8, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>9 DEF a8, ProcSet, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>10. ASSUME NEW self \in 1..N, + a9(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>10 DEF a9 + <3>2. (gate_2 \in 0..N)' + BY <2>10 DEF a9 + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>10 DEF a9, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>10 DEF a9, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>10 DEF a9, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>10 DEF a9 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>10 DEF a9, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>10 DEF a9, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + BY <2>10 DEF a9, TypeOK + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>10 DEF a9, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>10 DEF a9, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + BY <2>10 DEF a9, TypeOK + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>10 DEF a9, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + <4>1. rdv \in 0..N + BY ProcSetSubSetsBound + <4>2. CASE rdv = 0 + (* + prove that if rdv = 0, every other process must be in a12 since : + - there cannot be another process except self in the critical sections + - they must be outside the rdv section + - cannot be in a0/a1 since self is in a9 (8th invariant item) + *) + <5>1. (pc[self] = "a10")' + BY <2>10, <4>2 DEF a9, ProcSet, TypeOK + <5>2. \A p \in ProcSet : (self # p) => ~lockcs(p) + BY <2>10, <4>2, <5>1 DEF a9, ProcSet, TypeOK, LockInv + <5>3. \A p \in ProcSet : p#self => ~rdvsection(p) + BY <4>2, AllProcsNotInRdv + <5>4. ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + BY <2>10 DEF a9, ProcSet + <5>5. \A p \in ProcSet : (self # p) => pc[p] = "a12" + BY <5>2, <5>3, <5>4 DEF ProcSet, TypeOK + <5>6. (\A p \in ProcSet : (self # p) => pc[p] = "a12")' + BY <2>10, <4>2, <5>1, <5>5 DEF a9, ProcSet, TypeOK + <5>7. QED + BY <2>10, <4>2, <5>1, <5>6 DEF a9 + <4>3. CASE rdv > 0 + (* + prove that if rdv is not 0, we cannot have a process in a10 + - self will move to a11 (and others will not change) + - currently none can be there (lock exclusion) + *) + <5>1. (pc[self] = "a11")' + BY <2>10, <4>3 DEF a9, ProcSet, TypeOK + <5>2. ~(\E p \in ProcSet: pc[p] = "a10") + BY <2>10, <4>3 DEF a9, ProcSet, LockInv + <5>3. ~(\E p \in ProcSet: pc[p] = "a10")' + BY <2>10, <4>3, <5>1, <5>2 DEF a9, ProcSet, TypeOK + <5>4. QED + BY <5>3 + <4>5. QED + BY <4>1, <4>2, <4>3 + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>11. ASSUME NEW self \in 1..N, + a10(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>11 DEF a10 + <3>2. (gate_2 \in 0..N)' + BY <2>11 DEF a10, ProcSet, TypeOK + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>11 DEF a10, ProcSet, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>11 DEF a10, TypeOK + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + BY <2>11 DEF a10, ProcSet, TypeOK + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>11 DEF a10, ProcSet + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>11 DEF a10, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>11 DEF a10, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + BY <2>11 DEF a10, ProcSet, TypeOK + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>11 DEF a10, TypeOK + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>11 DEF a10, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + (* + This part is still true as : + - gate_2 will be set to N + - ProcsInB2 must be equal to ProcSet + *) + <4>1. (\A p \in ProcSet : (self # p) => pc[p] = "a12") + BY <2>11 DEF a10, ProcSet + <4>2. (\A p \in ProcSet : (self # p) => pc[p] = "a12")' + BY <2>11, <4>1 DEF a10, ProcSet, TypeOK + <4>3. pc'[self] = "a11" + BY <2>11 DEF a10, ProcSet, TypeOK + <4>4. (\A p \in ProcSet : pc[p] \in {"a11","a12"})' + BY <2>11, <4>2, <4>3 DEF ProcSet + <4>5. ProcsInB2' = ProcSet + BY <4>4 + <4> HIDE DEF ProcsInB2 + <4>6. Cardinality(ProcsInB2)' = N + BY <4>5, FS_Interval DEF ProcSet + <4>7. gate_2' = N + BY <2>11 DEF a10, ProcSet + <4>8. QED + BY <4>6, <4>7 + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>11 DEF a10, ProcSet, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>11 DEF a10, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>12. ASSUME NEW self \in 1..N, + a11(self) + PROVE Inv' + BY <2>12 DEF a11, TypeOK + <2>13. ASSUME NEW self \in 1..N, + a12(self) + PROVE Inv' + <3>1. (gate_1 \in 0..N)' + BY <2>13 DEF a12 + <3>2. (gate_2 \in 0..N)' + BY <2>13 DEF a12 + <3>3. (rdv = Cardinality(ProcsInRdv))' + BY <2>13 DEF a12, TypeOK + <3>4. (gate_1 > 0 => \E p \in ProcSet : pc[p] \in {"a5", "a6"})' + BY <2>13 DEF a12 + <3>5. (gate_2 > 0 => \E p \in ProcSet : pc[p] \in {"a11", "a12"})' + (* + This stays true since : + - Either gate_2 becomes 0 (the last process leaves the wait) + - Either gate_2 stays > 0 + + In this case there must be at least two processes inside B2 + and they cannot be between a7-a10 (reciprocal of 13th item of Invariant) + so if self moves to a0, there still is a process between a11-a12 + *) + <4>1. CASE gate_2' = 0 + <5>1. QED + BY <4>1 + <4>2. CASE gate_2' > 0 + <5>1. gate_2 >= 2 + BY <2>13, <4>2 DEF a12 + <5>2. Cardinality(ProcsInB2) >= 2 + BY <5>1, ProcSetSubSetsBound + <5>3. \E p, q \in ProcSet : (p # q) /\ p \in ProcsInB2 /\ q \in ProcsInB2 + BY <5>2, ProcSetSubSetsBound, FS_TwoElements + <5>4. ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + BY <5>1 + <5>5. \E p \in ProcSet: (p # self) /\ pc[p] \in {"a11", "a12"} + BY <5>3, <5>4 + <5>6. (\E p \in ProcSet: pc[p] \in {"a11", "a12"})' + BY <2>13, <5>5 DEF a12, ProcSet, TypeOK + <5>7. QED + BY <4>2, <5>6 + <4>3. QED + BY <4>1, <4>2 + <3>6. ((gate_1 = 0) \/ (gate_2 = 0))' + BY <2>13 DEF a12 + <3>7. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}))' + BY <2>13 DEF a12, TypeOK + <3>8. ((\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + => ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}))' + BY <2>13 DEF a12, TypeOK + <3>9. (gate_1 =< Cardinality(ProcsInB1))' + \* gate_1 is and stays 0 and Cardinality is in 0..N + BY <2>13, ProcSetSubSetsBound DEF a12 + <3>10. ((\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + => gate_1 = 0)' + BY <2>13 DEF a12 + <3>11. (\A p \in ProcSet: pc[p] = "a4" => ( + /\ rdv = N + /\ \A q \in ProcSet : (p # q) => pc[q] = "a6" + ))' + BY <2>13 DEF a12, TypeOK + <3>12. (gate_2 =< Cardinality(ProcsInB2))' + (* + when self goes to a0 : + - ProcsInB2 loses one element + - gate_2 decreased by 1 + + so comparision stays true + *) + <4>1. /\ gate_2' + 1 = gate_2 + /\ gate_2 \in Nat /\ gate_2' \in Nat + BY <2>13 DEF a12 + <4>2. /\ ProcsInB2' = ProcsInB2 \ {self} + /\ self \in ProcsInB2 + BY <2>13 DEF a12, ProcSet, TypeOK + <4> HIDE DEF ProcsInB2 + <4>3. /\ Cardinality(ProcsInB2)' + 1 = Cardinality(ProcsInB2) + /\ Cardinality(ProcsInB2)' \in Nat + BY <4>2, ProcSetSubSetsBound, FS_RemoveElement + <4>4. QED + BY <4>1, <4>3 + <3>13. ((\E p \in ProcSet: pc[p] \in{"a7", "a8", "a9", "a10"}) + => gate_2 = 0)' + BY <2>13 DEF a12, TypeOK + <3>14. (\A p \in ProcSet: pc[p] = "a10" => ( + /\ rdv = 0 + /\ \A q \in ProcSet : (p # q) => pc[q] = "a12" + ))' + BY <2>13 DEF a12, TypeOK + <3>15. QED + BY <3>1, <3>2, <3>3, <3>4, <3>5, <3>6, <3>7, + <3>8, <3>9, <3>10, <3>11, <3>12, <3>13, <3>14 + <2>14. CASE UNCHANGED vars + BY <2>14 DEF vars + <2>15. QED + BY <2>1, <2>10, <2>11, <2>12, <2>13, <2>14, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Next, proc + <1>3. QED + BY <1>1, <1>2, PTL, Typing, LockExclusion DEF Spec + +THEOREM BarrierExclusion == + Inv => \/ ~(\E p \in ProcSet: pc[p] \in {"a0", "a1", "a2", "a3", "a4"}) + \/ ~(\E p \in ProcSet: pc[p] \in {"a7", "a8", "a9", "a10"}) + BY N_Assumption DEF Inv + +THEOREM BarrierExclusion2 == + TypeOK /\ Inv => + \/ (\A p \in ProcSet: pc[p] \in + {"a5", "a6", "a7", "a8", "a9", "a10", "a11", "a12"}) + \/ (\A p \in ProcSet: pc[p] \in + {"a11", "a12", "a0", "a1", "a2", "a3", "a4", "a5", "a6"}) + BY N_Assumption DEF TypeOK, Inv + +THEOREM FlushInvariant == Spec => []FlushInv + <1> USE N_Assumption DEF FlushInv, ProcSet, + ProcsInB1, barrier1, ProcsInB2, barrier2 + <1>1. Init => FlushInv + BY FS_EmptySet DEF Init + <1>2. /\ [Next]_vars + /\ TypeOK + /\ LockInv + /\ Inv + /\ FlushInv + => FlushInv' + <2> SUFFICES ASSUME [Next]_vars, TypeOK, LockInv, Inv, FlushInv + PROVE FlushInv' + OBVIOUS + <2>1. ASSUME NEW self \in 1..N, a0(self) + PROVE FlushInv' + BY <2>1 DEF a0, TypeOK, Inv + <2>2. ASSUME NEW self \in 1..N, a1(self) + PROVE FlushInv' + BY <2>2 DEF a1, TypeOK, Inv + <2>3. ASSUME NEW self \in 1..N, a2(self) + PROVE FlushInv' + BY <2>3 DEF a2, TypeOK, Inv + <2>4. ASSUME NEW self \in 1..N, a3(self) + PROVE FlushInv' + BY <2>4 DEF a3, TypeOK, Inv, LockInv + <2>5. ASSUME NEW self \in 1..N, a4(self) + PROVE FlushInv' + <3>1. (gate_1 > 0 => gate_1 = Cardinality(ProcsInB1))' + <4>1. (\A p \in ProcSet : (self # p) => pc[p] = "a6") + BY <2>5 DEF a4, Inv + <4>2. (\A p \in ProcSet : (self # p) => pc[p] = "a6")' + BY <2>5, <4>1 DEF a4, ProcSet, TypeOK + <4>3. pc'[self] = "a5" + BY <2>5 DEF a4, ProcSet, TypeOK + <4>4. (\A p \in ProcSet : pc[p] \in {"a5","a6"})' + BY <2>5, <4>2, <4>3 DEF ProcSet + <4>5. ProcsInB1' = ProcSet + BY <4>4 + <4> HIDE DEF ProcsInB1 + <4>6. Cardinality(ProcsInB1)' = N + BY <4>5, FS_Interval DEF ProcSet + <4>7. gate_1' = N + BY <2>5 DEF a4, Inv + <4>8. QED + BY <4>6, <4>7 + <3>2. (gate_2 > 0 => gate_2 = Cardinality(ProcsInB2))' + BY <2>5 DEF a4, TypeOK, Inv + <3>3. QED + BY <3>1, <3>2 + <2>6. ASSUME NEW self \in 1..N, a5(self) + PROVE FlushInv' + BY <2>6 DEF a5, TypeOK, Inv + <2>7. ASSUME NEW self \in 1..N, a6(self) + PROVE FlushInv' + <3>1. (gate_1 > 0 => gate_1 = Cardinality(ProcsInB1))' + <4>1. /\ gate_1' + 1 = gate_1 + /\ gate_1 \in Nat /\ gate_1' \in Nat + BY <2>7 DEF a6, TypeOK + <4>2. /\ ProcsInB1' = ProcsInB1 \ {self} + /\ self \in ProcsInB1 + BY <2>7 DEF a6, TypeOK + <4> HIDE DEF ProcsInB1 + <4>3. /\ Cardinality(ProcsInB1)' + 1 = Cardinality(ProcsInB1) + /\ Cardinality(ProcsInB1)' \in Nat /\ Cardinality(ProcsInB1) \in Nat + BY <4>2, ProcSetSubSetsBound, FS_RemoveElement + <4>4. QED + BY <4>1, <4>3 + <3>2. (gate_2 > 0 => gate_2 = Cardinality(ProcsInB2))' + BY <2>7 DEF a6, TypeOK, Inv + <3>3. QED + BY <3>1, <3>2 + <2>8. ASSUME NEW self \in 1..N, a7(self) + PROVE FlushInv' + BY <2>8 DEF a7, TypeOK, Inv + <2>9. ASSUME NEW self \in 1..N, a8(self) + PROVE FlushInv' + BY <2>9 DEF a8, TypeOK, Inv + <2>10. ASSUME NEW self \in 1..N, a9(self) + PROVE FlushInv' + BY <2>10 DEF a9, TypeOK, Inv, LockInv + <2>11. ASSUME NEW self \in 1..N, a10(self) + PROVE FlushInv' + <3>1. (gate_1 > 0 => gate_1 = Cardinality(ProcsInB1))' + BY <2>11 DEF a10, TypeOK, Inv + <3>2. (gate_2 > 0 => gate_2 = Cardinality(ProcsInB2))' + <4>1. (\A p \in ProcSet : (self # p) => pc[p] = "a12") + BY <2>11 DEF a10, Inv + <4>2. (\A p \in ProcSet : (self # p) => pc[p] = "a12")' + BY <2>11, <4>1 DEF a10, ProcSet, TypeOK + <4>3. pc'[self] = "a11" + BY <2>11 DEF a10, ProcSet, TypeOK + <4>4. (\A p \in ProcSet : pc[p] \in {"a11","a12"})' + BY <2>11, <4>2, <4>3 DEF ProcSet + <4>5. ProcsInB2' = ProcSet + BY <4>4 + <4> HIDE DEF ProcsInB2 + <4>6. Cardinality(ProcsInB2)' = N + BY <4>5, FS_Interval DEF ProcSet + <4>7. gate_2' = N + BY <2>11 DEF a10, Inv + <4>8. QED + BY <4>6, <4>7 + <3>3. QED + BY <3>1, <3>2 + <2>12. ASSUME NEW self \in 1..N, a11(self) + PROVE FlushInv' + BY <2>12 DEF a11, TypeOK, Inv + <2>13. ASSUME NEW self \in 1..N, a12(self) + PROVE FlushInv' + <3>1. (gate_1 > 0 => gate_1 = Cardinality(ProcsInB1))' + BY <2>13 DEF a12, TypeOK, Inv + <3>2. (gate_2 > 0 => gate_2 = Cardinality(ProcsInB2))' + <4>1. /\ gate_2' + 1 = gate_2 + /\ gate_2 \in Nat /\ gate_2' \in Nat + BY <2>13 DEF a12, Inv + <4>2. /\ ProcsInB2' = ProcsInB2 \ {self} + /\ self \in ProcsInB2 + BY <2>13 DEF a12, TypeOK + <4> HIDE DEF ProcsInB2 + <4>3. /\ Cardinality(ProcsInB2)' + 1 = Cardinality(ProcsInB2) + /\ Cardinality(ProcsInB2)' \in Nat + BY <4>2, ProcSetSubSetsBound, FS_RemoveElement + <4>4. QED + BY <4>1, <4>3 + <3>3. QED + BY <3>1, <3>2 + <2>14. CASE UNCHANGED vars + BY <2>14 DEF vars + <2>15. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, + <2>8, <2>9, <2>10, <2>11, <2>12, <2>13, <2>14 + DEF Next, proc, ProcSet + <1>3. QED + BY <1>1, <1>2, Typing, LockExclusion, Invariant, PTL DEF Spec + +THEOREM Spec => B!Spec + <1> USE DEF ProcSet, B!ProcSet, pc_translation + <1>1. Init => B!Init + BY DEF Init, B!Init + <1>2. /\ [Next]_vars + /\ TypeOK /\ TypeOK' + /\ LockInv /\ LockInv' + /\ Inv /\ Inv' + /\ FlushInv /\ FlushInv' + => [B!Next]_B!vars + <2> USE DEF Next, vars, B!Next, B!vars, B!b0, B!b1 + <2> SUFFICES ASSUME [Next]_vars, + TypeOK, TypeOK', + LockInv, LockInv', + Inv, Inv', + FlushInv, FlushInv' + PROVE [B!Next]_B!vars + OBVIOUS + <2>1. ASSUME NEW self \in 1..N, a0(self) + PROVE [B!Next]_B!vars + BY <2>1 DEF a0, TypeOK + <2>2. ASSUME NEW self \in 1..N, a1(self) + PROVE UNCHANGED B!vars + BY <2>2 DEF a1, TypeOK + <2>3. ASSUME NEW self \in 1..N, a2(self) + PROVE UNCHANGED B!vars + BY <2>3 DEF a2, TypeOK + <2>4. ASSUME NEW self \in 1..N, a3(self) + PROVE UNCHANGED B!vars + BY <2>4 DEF a3, TypeOK + <2>5. ASSUME NEW self \in 1..N, a4(self) + PROVE UNCHANGED B!vars + BY <2>5 DEF a4, TypeOK, Inv + <2>6. ASSUME NEW self \in 1..N, a5(self) + PROVE UNCHANGED B!vars + BY <2>6 DEF a5, TypeOK + <2>7. ASSUME NEW self \in 1..N, a6(self) + PROVE UNCHANGED B!vars + BY <2>7 DEF a6, TypeOK + <2>8. ASSUME NEW self \in 1..N, a7(self) + PROVE UNCHANGED B!vars + BY <2>8 DEF a7, TypeOK + <2>9. ASSUME NEW self \in 1..N, a8(self) + PROVE UNCHANGED B!vars + BY <2>9 DEF a8, TypeOK + <2>10. ASSUME NEW self \in 1..N, a9(self) + PROVE UNCHANGED B!vars + BY <2>10 DEF a9, TypeOK, LockInv, Inv + <2>11. ASSUME NEW self \in 1..N, a10(self) + PROVE [B!Next]_B!vars + BY <2>11 DEF a10, TypeOK, LockInv, Inv + <2>12. ASSUME NEW self \in 1..N, a11(self) + PROVE UNCHANGED B!vars + BY <2>12 DEF a11, TypeOK + <2>13. ASSUME NEW self \in 1..N, a12(self) + PROVE UNCHANGED B!vars + <3>1. CASE gate_2' = 0 + <4>1. /\ gate_2 = 1 + /\ Cardinality(ProcsInB2) = 1 + BY <2>13, <3>1 DEF a12, TypeOK, FlushInv + <4>2. /\ ProcsInB2' = ProcsInB2 \ {self} + /\ self \in ProcsInB2 + BY <2>13 DEF a12, TypeOK, ProcsInB2, barrier2 + <4>3. /\ Cardinality(ProcsInB2)' = 0 + BY <4>1, <4>2, ProcSetSubSetsBound, FS_RemoveElement + <4>4. ~(\E p \in ProcSet : barrier2(p))' + BY <4>3, ProcSetSubSetsBound, FS_EmptySet DEF ProcsInB2 + <4>5. QED + BY <2>13, <4>1, <4>4 DEF a12, barrier2, TypeOK + <3>2. CASE gate_2' > 0 + BY <2>13, <3>2 DEF a12, TypeOK, Inv + <3>3. QED + BY <3>1, <3>2 DEF TypeOK + <2>14. CASE UNCHANGED vars + BY <2>14 DEF vars + <2>15. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, + <2>8, <2>9, <2>10, <2>11, <2>12, <2>13, <2>14 + DEF Next, proc + <1>3. QED + BY <1>1, <1>2, Typing, LockExclusion, Invariant, FlushInvariant, PTL + DEF Spec, B!Spec +=============================================================================== diff --git a/specifications/barriers/README.md b/specifications/barriers/README.md new file mode 100644 index 00000000..d1f0d38b --- /dev/null +++ b/specifications/barriers/README.md @@ -0,0 +1,68 @@ +# Barrier synchronization + +*This specification comes from a +[Master's thesis](http://hdl.handle.net/2268.2/23374)* + +A barrier +([Wikipedia](https://en.wikipedia.org/wiki/Barrier_(computer_science))) +is a synchronization facility which ensures that a group of threads all reach +the barrier before they can advance. + +Such a barrier is useful when parallel computations are done in two or more +steps and results from all threads are needed to continue. + +## Barrier.tla + +A specification of an abstract Barrier. + +The usual typing `TypeOK` invariant is defined. + +Another property to show that processes cannot leave the barrier as long as +there are others outside of it is also given. (see `BarrierProperty`) + +A model with $N = 6$ that verifies both properties is provided. + +## Barriers.tla + +A specification of a Reusable Barrier synchronization facility using as +presented in the INFO09012 Parallel Programming course in ULiège by +Prof. Pascal Fontaine. + +The barrier consists of two waiting chambers `a1-a6` and `a7-a12`. +The last process entering a waiting chamber signals the appropriate semaphore +and allows processes to pass to the next section. +Using two such waiting chambers makes sure a process leaving the barrier cannot +reenter and pass through the whole barrier again and possibly blocking a +process inside. + +## Invariants + +- `TypeOK` is the usual typing invariant. The typing invariant alone cannot + determine the range of values the semaphores can take. +- `LockInv` is used to represent the mutual exclusion inside critical sections + present in the specification. +- `Inv` is the main invariant representing most properties of this double + barrier construction. + Each clause is explained with a comment inside the specification. + Due to the symmetry between the two waiting rooms, there are pairs of clauses + that represent the same property for each section. +- `FlushInv` are two additional clauses needed to prove the refinement. + It shows that once a waiting section is opened, all processes can pass. + +A model `Barriers.cfg` with $N = 6$ that verifies these four invariants is +provided. + +The invariants are also proven correct using TLAPS. + +## Refinement + +A refinement towards an abstract Barrier specification is given by translating +the program counter. +This translation must take into account the simultaneous movement of all +processes done by action `b1` of `Barrier.tla`. +In the refinement, processes at `a11-a12` while the second waiting chamber is +opened are already considered outside the barrier. +This emulates a simultaneous movement of all process for the refinement. + +The correctness of the refinement is checked in `Barriers.cfg` and proven with +TLAPS. diff --git a/specifications/locks_auxiliary_vars/Lock.cfg b/specifications/locks_auxiliary_vars/Lock.cfg new file mode 100644 index 00000000..edc71178 --- /dev/null +++ b/specifications/locks_auxiliary_vars/Lock.cfg @@ -0,0 +1,2 @@ +SPECIFICATION Spec +INVARIANTS TypeOK LockInv \ No newline at end of file diff --git a/specifications/locks_auxiliary_vars/Lock.tla b/specifications/locks_auxiliary_vars/Lock.tla new file mode 100644 index 00000000..d8ce7721 --- /dev/null +++ b/specifications/locks_auxiliary_vars/Lock.tla @@ -0,0 +1,119 @@ +--------------------------------- MODULE Lock --------------------------------- + +(*****************************************************************************) +(* This module contains the specification of an abstract lock. *) +(* The proof for mutual exclusion is also detailed. *) +(*****************************************************************************) + +EXTENDS Integers, TLAPS + +(* +--algorithm Lock{ + variables lock = 1; + + macro Lock(l){ + await l = 1; + l := 0; + } + + macro Unlock(l){ + l := 1; + } + + process(proc \in 1..2){ +l0: while(TRUE){ + skip; \* non-critical section +l1: Lock(lock); +cs: skip; \* critical section +l2: Unlock(lock); + } + } +} +*) +\* BEGIN TRANSLATION (chksum(pcal) = "f820ffbb" /\ chksum(tla) = "24b4f3dd") +VARIABLES pc, lock + +vars == << pc, lock >> + +ProcSet == (1..2) + +Init == (* Global variables *) + /\ lock = 1 + /\ pc = [self \in ProcSet |-> "l0"] + +l0(self) == /\ pc[self] = "l0" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "l1"] + /\ lock' = lock + +l1(self) == /\ pc[self] = "l1" + /\ lock = 1 + /\ lock' = 0 + /\ pc' = [pc EXCEPT ![self] = "cs"] + +cs(self) == /\ pc[self] = "cs" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "l2"] + /\ lock' = lock + +l2(self) == /\ pc[self] = "l2" + /\ lock' = 1 + /\ pc' = [pc EXCEPT ![self] = "l0"] + +proc(self) == l0(self) \/ l1(self) \/ cs(self) \/ l2(self) + +Next == (\E self \in 1..2: proc(self)) + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION + +TypeOK == + /\ lock \in {0, 1} + /\ pc \in [ProcSet -> {"l0", "l1", "cs", "l2"}] + +lockcs(i) == + pc[i] \in {"cs", "l2"} + +LockInv == + /\ \A i, j \in ProcSet: (i # j) => ~(lockcs(i) /\ lockcs(j)) + /\ (\E p \in ProcSet: lockcs(p)) => lock = 0 + +------------------------------------------------------------------------------- + +LEMMA Typing == Spec => []TypeOK + <1>1. Init => TypeOK + BY DEF Init, TypeOK + <1>2. [Next]_vars /\ TypeOK => TypeOK' + BY DEF TypeOK, vars, Next, proc, l0, l1, cs, l2 + <1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +THEOREM MutualExclusion == Spec => []LockInv + <1> USE DEF LockInv, lockcs + <1>1. Init => LockInv + BY DEF Init, ProcSet + <1>2. [Next]_vars /\ TypeOK /\ LockInv => LockInv' + <2> SUFFICES ASSUME [Next]_vars /\ TypeOK /\ LockInv + PROVE LockInv' + OBVIOUS + <2>1. ASSUME NEW self \in 1..2, l0(self) + PROVE LockInv' + BY <2>1 DEF l0, ProcSet, TypeOK + <2>2. ASSUME NEW self \in 1..2, l1(self) + PROVE LockInv' + BY <2>2 DEF l1, ProcSet, TypeOK + <2>3. ASSUME NEW self \in 1..2, cs(self) + PROVE LockInv' + BY <2>3 DEF cs, ProcSet, TypeOK + <2>4. ASSUME NEW self \in 1..2, l2(self) + PROVE LockInv' + BY <2>4 DEF l2, ProcSet, TypeOK + <2>5. CASE UNCHANGED vars + BY <2>5 DEF vars + <2>6. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF Next, vars, proc + <1>3. QED + BY <1>1, <1>2, Typing, PTL DEF Spec + +=============================================================================== diff --git a/specifications/locks_auxiliary_vars/LockHS.cfg b/specifications/locks_auxiliary_vars/LockHS.cfg new file mode 100644 index 00000000..4d7b91ba --- /dev/null +++ b/specifications/locks_auxiliary_vars/LockHS.cfg @@ -0,0 +1,3 @@ +SPECIFICATION SpecHS +INVARIANTS TypeOKHS InvHS LockInv +PROPERTIES Spec PSpec \ No newline at end of file diff --git a/specifications/locks_auxiliary_vars/LockHS.tla b/specifications/locks_auxiliary_vars/LockHS.tla new file mode 100644 index 00000000..0143a31f --- /dev/null +++ b/specifications/locks_auxiliary_vars/LockHS.tla @@ -0,0 +1,403 @@ +-------------------------------- MODULE LockHS -------------------------------- + +(*****************************************************************************) +(* This module contains the specification of a lock with auxiliary variables.*) +(* 1. A history variable `h_turn` is needed to remember the assignement of *) +(* the turn variable used inside the Peterson specification. *) +(* 2. A stuttering variable `s` is added to force the stuttering of the Lock *) +(* specification to mimick the 3 steps taken by Peterson to enter the *) +(* critical section. *) +(* With these variables, one can finally refine LockHS to Peterson, giving *) +(* an equivalence between the Lock and Peterson specifications. *) +(* *) +(* The stuttering is achieved using the Stuttering module created by Leslie *) +(* Lamport and comes from to the paper "Auxiliary Variables in TLA+". *) +(* The module used here has been modified, see explanations at the end of *) +(* the Stuttering module. *) +(*****************************************************************************) + +EXTENDS Lock, NaturalsInduction + +\* History variable to remember the turn variable +VARIABLE h_turn +NoHistoryChange(A) == A /\ UNCHANGED h_turn + +\* Stuttering variable +VARIABLE s +INSTANCE Stuttering + +\* This theorem justifies the validity of the introduced stuttering variable +\* in definition l1HS +THEOREM StutterConstantCondition(1..2, 1, LAMBDA j : j-1) +<1>. DEFINE InvD(S) == {sig \in (1..2) \ S : sig-1 \in S} + R[n \in Nat] == IF n = 0 THEN {1} + ELSE R[n-1] \cup InvD(R[n-1]) +<1>. SUFFICES (1..2) = UNION {R[n] : n \in Nat} + BY Zenon DEF StutterConstantCondition +<1>. HIDE DEF R +<1>1. \A n \in Nat : R[n] = IF n = 0 THEN {1} + ELSE R[n-1] \cup InvD(R[n-1]) + <2>. DEFINE RDef(g,n) == g \cup InvD(g) + <2>1. NatInductiveDefHypothesis(R, {1}, RDef) + BY Zenon DEF R, NatInductiveDefHypothesis + <2>2. NatInductiveDefConclusion(R, {1}, RDef) + BY <2>1, NatInductiveDef, Zenon + <2>. QED BY <2>2 DEF NatInductiveDefConclusion +<1>2. ASSUME NEW n \in Nat + PROVE R[n] \subseteq 1 .. 2 + <2>. DEFINE P(_n) == R[_n] \subseteq 1 .. 2 + <2>1. P(0) + BY <1>1 + <2>2. ASSUME NEW m \in Nat, P(m) + PROVE P(m+1) + <3>1. \A S : InvD(S) \subseteq 1 .. 2 + OBVIOUS + <3> DEFINE _m == m+1 + <3>2. _m \in Nat \ {0} + OBVIOUS + <3> HIDE DEF _m + <3>3. R[_m] = R[_m-1] \cup InvD(R[_m-1]) + BY <1>1, <3>2, Isa + <3> USE DEF _m + <3>4. R[m+1] = R[m] \cup InvD(R[m]) + BY <3>3 + <3>. QED BY <2>2, <3>1, <3>4 + <2>. HIDE DEF P + <2>3. \A m \in Nat : P(m) + BY <2>1, <2>2, NatInduction, Isa + <2>. QED BY <2>3 DEF P +<1>3. R[1] = 1 .. 2 + BY <1>1 +<1>. QED BY <1>2, <1>3 + +------------------------------------------------------------------------------- + +Other(p) == IF p = 1 THEN 2 ELSE 1 + +InitHS == Init /\ (h_turn = 1) /\ (s = top) + +\* Adding 2 stuttering steps after an l1(self) transition +\* Updating the history variable during the right stutter step +l1HS(self) == + /\ PostStutter(l1(self), "l1", self, 1, 2, LAMBDA j : j-1) + /\ h_turn' = IF s' # top THEN IF s'.val = 1 THEN Other(self) + ELSE h_turn + ELSE h_turn + +procHS(self) == + \/ NoStutter(NoHistoryChange(l0(self))) + \/ l1HS(self) + \/ NoStutter(NoHistoryChange(cs(self))) + \/ NoStutter(NoHistoryChange(l2(self))) + +NextHS == (\E self \in 1..2: procHS(self)) + +SpecHS == InitHS /\ [][NextHS]_<> + +------------------------------------------------------------------------------- + +TypeOKHS == + /\ TypeOK + /\ h_turn \in 1..2 + /\ s \in {top} \cup [id : {"l1"}, ctxt : {1, 2}, val : 1..2] + +InvHS == + /\ \A p \in ProcSet : + /\ IF s # top THEN s.ctxt = p ELSE FALSE + => pc[p] = "cs" + /\ \A p \in ProcSet : + \/ pc[p] = "l2" + \/ pc[p] = "cs" /\ s = top + \/ IF s # top THEN s.ctxt = p /\ s.val = 1 ELSE FALSE + => h_turn = Other(p) + +pc_translation(self, label, stutter) == + CASE (label = "l0") -> "a0" + [] (label = "l1") -> "a1" + [] (label = "l2") -> "a4" + [] (label = "cs") -> IF stutter = top THEN "cs" + ELSE IF stutter.ctxt # self THEN "cs" + ELSE IF stutter.val = 2 THEN "a2" + ELSE IF stutter.val = 1 THEN "a3" + ELSE "error" +c_translation(alt_label) == + alt_label \in {"a2", "a3", "cs", "a4"} + +P == INSTANCE Peterson WITH + pc <- [p \in ProcSet |-> pc_translation(p, pc[p], s)], + c <- [p \in ProcSet |-> c_translation(pc_translation(p, pc[p], s))], + turn <- h_turn +PSpec == P!Spec + +------------------------------------------------------------------------------- + +(*****************************************************************************) +(* Proofs using stuttering variables can be quite complicated as the backend *) +(* solvers can be quite overwhelmed by the different transitions made *) +(* possible by the PostStutter clauses. *) +(* The easiest way to complete such proofs seems to be the extraction of *) +(* all relevant information in a first step and then refer to that step *) +(* instead of the expanded PostStutter. *) +(*****************************************************************************) + +LEMMA TypingHS == SpecHS => []TypeOKHS + <1> USE DEF TypeOKHS, TypeOK, Other + <1>1. InitHS => TypeOKHS + BY DEF InitHS, Init + <1>2. [NextHS]_<> /\ TypeOKHS => TypeOKHS' + <2> USE DEF NoStutter, NoHistoryChange + <2> SUFFICES ASSUME [NextHS]_<>, + TypeOKHS + PROVE TypeOKHS' + OBVIOUS + <2>1. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l0(self))) + PROVE TypeOKHS' + BY <2>1 DEF l0 + <2>2. ASSUME NEW self \in 1..2, l1HS(self) + PROVE TypeOKHS' + BY <2>2 DEF l1HS, l1, PostStutter, vars + <2>3. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(cs(self))) + PROVE TypeOKHS' + BY <2>3 DEF cs + <2>4. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l2(self))) + PROVE TypeOKHS' + BY <2>4 DEF l2 + <2>5. CASE UNCHANGED <> + BY <2>5 DEF vars + <2>6. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF NextHS, procHS + <1>3. QED + BY <1>1, <1>2, PTL DEF SpecHS + +LEMMA AddingVariables == SpecHS => Spec + <1> USE DEF Other + <1>1. InitHS => Init + BY DEF InitHS + <1>2. [NextHS]_<> /\ TypeOKHS => [Next]_vars + <2> USE DEF Next, vars, proc, NoStutter, NoHistoryChange + <2> SUFFICES ASSUME [NextHS]_<>, + TypeOKHS + PROVE [Next]_vars + OBVIOUS + <2>1. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l0(self))) + PROVE [Next]_vars + BY <2>1 DEF l0 + <2>2. ASSUME NEW self \in 1..2, l1HS(self) + PROVE [Next]_vars + BY <2>2 DEF l1HS, l1, PostStutter, vars + <2>3. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(cs(self))) + PROVE [Next]_vars + BY <2>3 DEF cs + <2>4. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l2(self))) + PROVE [Next]_vars + BY <2>4 DEF l2 + <2>5. CASE UNCHANGED <> + BY <2>5 DEF vars + <2>6. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF NextHS, procHS + <1>3. QED + BY <1>1, <1>2, TypingHS, PTL DEF SpecHS, Spec + +LEMMA MutualExclusionHS == SpecHS => []LockInv + BY AddingVariables, MutualExclusion + +LEMMA IndInvHS == SpecHS => []InvHS + <1> USE DEF InvHS, Other + <1>1. InitHS => InvHS + BY DEF InitHS, Init + <1>2. /\ [NextHS]_<> + /\ TypeOKHS /\ TypeOKHS' + /\ LockInv /\ LockInv' + /\ InvHS + => InvHS' + <2> USE DEF NoStutter, NoHistoryChange + <2> SUFFICES ASSUME [NextHS]_<>, + TypeOKHS, TypeOKHS', + LockInv, LockInv', + InvHS + PROVE InvHS' + OBVIOUS + <2>1. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l0(self))) + PROVE InvHS' + BY <2>1 DEF l0, ProcSet, TypeOKHS, TypeOK + <2>2. ASSUME NEW self \in 1..2, l1HS(self) + PROVE InvHS' + <3> USE DEF PostStutter + <3>1. CASE s = top + <4>1. s' # top /\ s' = [id|->"l1", ctxt |-> self, val |-> 2] + BY <2>2, <3>1 DEF l1HS, l1, top + <4>2. pc'[self] = "cs" /\ lockcs(self)' + BY <2>2, <3>1 DEF l1HS, l1, ProcSet, TypeOKHS, TypeOK, lockcs + <4>3. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>2 DEF ProcSet, TypeOKHS, TypeOK, lockcs, LockInv + <4>4. QED + BY <4>1, <4>2, <4>3 + <3>2. ASSUME s # top /\ s.ctxt # self PROVE FALSE + BY <2>2, <3>2 DEF l1HS + <3>3. CASE s # top /\ s = [id|->"l1", ctxt |-> self, val |-> 2] + <4>1. s' # top /\ s' = [id|->"l1", ctxt |-> self, val |-> 1] + BY <2>2, <3>3 DEF l1HS, l1, top + <4>2. h_turn' = Other(self) + BY <2>2, <3>3, <4>1 DEF l1HS + <4>3. pc[self] = "cs" /\ pc'[self] = "cs" /\ UNCHANGED pc + BY <2>2, <3>3 DEF l1HS, ProcSet, vars + <4>4. \A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"} + BY <4>3 DEF ProcSet, LockInv, lockcs, TypeOKHS, TypeOK + <4>5. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>3, <4>4 + <4>6. QED + BY <4>1, <4>2, <4>3, <4>5 + <3>4. CASE s # top /\ s = [id|->"l1", ctxt |-> self, val |-> 1] + <4>1. s' = top + BY <2>2, <3>4 DEF l1HS + <4>2. h_turn = Other(self) /\ h_turn' = Other(self) + BY <2>2, <3>4 DEF l1HS, ProcSet + <4>3. pc[self] = "cs" /\ pc'[self] = "cs" /\ UNCHANGED pc + BY <2>2, <3>4 DEF l1HS, ProcSet, vars + <4>4. \A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"} + BY <4>3 DEF ProcSet, LockInv, lockcs, TypeOKHS, TypeOK + <4>5. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>3, <4>4 + <4>6. QED + BY <4>1, <4>2, <4>3, <4>4 + <3>5. QED + BY <3>1, <3>2, <3>3, <3>4 DEF TypeOKHS + <2>3. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(cs(self))) + PROVE InvHS' + BY <2>3 DEF cs, ProcSet, TypeOKHS, TypeOK + <2>4. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l2(self))) + PROVE InvHS' + BY <2>4 DEF l2, ProcSet, TypeOKHS, TypeOK + <2>5. CASE UNCHANGED <> + BY <2>5 DEF vars + <2>6. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5 DEF NextHS, procHS + <1>3. QED + BY <1>1, <1>2, TypingHS, MutualExclusionHS, PTL DEF SpecHS + + +THEOREM SpecHS => P!Spec + <1> USE DEF pc_translation, c_translation, + ProcSet, P!ProcSet, Other, P!Other + <1>1. InitHS => P!Init + BY DEF P!Init, InitHS, Init + <1>2. /\ [NextHS]_<> + /\ TypeOKHS /\ TypeOKHS' + /\ LockInv /\ LockInv' + /\ InvHS /\ InvHS' + => [P!Next]_P!vars + <2> USE DEF P!Next, P!vars, P!proc, NoStutter, NoHistoryChange + <2> SUFFICES ASSUME [NextHS]_<>, + TypeOKHS, TypeOKHS', + LockInv, LockInv', + InvHS, InvHS' + PROVE [P!Next]_P!vars + BY Zenon + <2>1. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l0(self))) + PROVE P!a0(self) + BY <2>1 DEF l0, P!a0, TypeOKHS, TypeOK, vars + <2>2. ASSUME NEW self \in 1..2, l1HS(self) + PROVE P!a1(self) \/ P!a2(self) \/ P!a3(self) + <3> USE DEF PostStutter + <3>1. ASSUME s = top PROVE P!a1(self) + \* extract relevant facts from premises + <4>1. /\ pc[self] = "l1" /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ s' # top /\ s' = [id |-> "l1", ctxt |-> self, val |-> 2] + /\ UNCHANGED h_turn + BY <2>2, <3>1 DEF l1HS, l1, TypeOKHS, top + \* Verify that P!pc[self] = "a1" + <4>2. pc_translation(self, pc[self], s) = "a1" + BY <4>1 + <4>3. pc_translation(self, pc[self], s)' = "a2" + BY <4>1 DEF TypeOKHS, TypeOK + <4>4. \A p \in ProcSet \ {self} : UNCHANGED pc[p] + BY <4>1 DEF TypeOKHS, TypeOK + <4>5. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>1 DEF TypeOKHS, TypeOK, lockcs, LockInv + \* Verify that the P!pc is modified correctly + <4>6. [p \in ProcSet |-> pc_translation(p, pc[p], s)]' + = [[p \in ProcSet |-> pc_translation(p, pc[p], s)] + EXCEPT ![self] = "a2" ] + BY <4>2, <4>3, <4>4, <4>5 DEF TypeOKHS, TypeOK + <4>7. QED + BY <4>1, <4>2, <4>6 DEF P!a1, TypeOKHS, TypeOK + <3>2. ASSUME s # top /\ s.ctxt # self PROVE FALSE + BY <2>2, <3>2 DEF l1HS + <3>3. ASSUME s # top /\ s = [id|->"l1", ctxt |-> self, val |-> 2] + PROVE P!a2(self) + \* extract relevant facts from premises + <4>1. /\ pc[self] = "cs" /\ UNCHANGED pc + /\ s' # top /\ s' = [id |-> "l1", ctxt |-> self, val |-> 1] + BY <2>2, <3>3 DEF l1HS, top, vars, TypeOKHS, InvHS + <4>2. h_turn' = Other(self) + BY <2>2, <4>1 DEF l1HS + \* Verify that P!pc[self] = "a2" + <4>3. pc_translation(self, pc[self], s) = "a2" + BY <3>3, <4>1 + <4>4. pc_translation(self, pc[self], s)' = "a3" + BY <4>1 DEF TypeOKHS, TypeOK + <4>5. \A p \in ProcSet \ {self} : UNCHANGED pc[p] + BY <4>1 DEF TypeOKHS, TypeOK + <4>6. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>1 DEF TypeOKHS, TypeOK, lockcs, LockInv + \* Verify P!pc is modified correctly + <4>7. [p \in ProcSet |-> pc_translation(p, pc[p], s)]' + = [[p \in ProcSet |-> pc_translation(p, pc[p], s)] + EXCEPT ![self] = "a3" ] + BY <4>3, <4>4, <4>5, <4>6 DEF TypeOKHS, TypeOK + <4>8. QED + BY <4>2, <4>3, <4>7 DEF P!a2, TypeOKHS, TypeOK + <3>4. ASSUME s # top /\ s = [id|->"l1", ctxt |-> self, val |-> 1] + PROVE P!a3(self) + \* extract relevant facts from premises + <4>1. /\ pc[self] = "cs" /\ UNCHANGED pc + /\ s' = top + /\ UNCHANGED h_turn + BY <2>2, <3>4 DEF l1HS, top, vars, TypeOKHS, TypeOK, InvHS + \* Verify that P!pc[self] = "a1" + <4>2. pc_translation(self, pc[self], s) = "a3" + BY <3>4, <4>1 + <4>3. pc_translation(self, pc[self], s)' = "cs" + BY <4>1 DEF TypeOKHS, TypeOK + <4>4. \A p \in ProcSet \ {self} : UNCHANGED pc[p] + BY <4>1 DEF TypeOKHS, TypeOK + <4>5. (\A p \in ProcSet \ {self} : pc[p] \in {"l0", "l1"})' + BY <4>1 DEF TypeOKHS, TypeOK, lockcs, LockInv + \* Verify that the P!pc is modified correctly + <4>6. [p \in ProcSet |-> pc_translation(p, pc[p], s)]' + = [[p \in ProcSet |-> pc_translation(p, pc[p], s)] + EXCEPT ![self] = "cs" ] + BY <4>2, <4>3, <4>4, <4>5 DEF TypeOKHS, TypeOK + \* Verify process can pass barrier + <4>7. c_translation(pc_translation(Other(self), pc[Other(self)], s))' = FALSE + BY <4>5 + <4>8. UNCHANGED c_translation(pc_translation(self, pc[self], s)) + BY <4>1, <4>2, <4>3 + <4>9. UNCHANGED c_translation(pc_translation(Other(self), pc[Other(self)], s)) + BY <4>4, <4>5 + <4>10. UNCHANGED [p \in ProcSet |-> c_translation(pc_translation(p, pc[p], s))] + BY <4>8, <4>9 DEF TypeOKHS, TypeOK + <4> HIDE DEF pc_translation, c_translation + <4>x. QED + BY <4>1, <4>2, <4>4, <4>6, <4>7, <4>10 + DEF P!a3, TypeOKHS, TypeOK + <3>5. QED + BY <3>1, <3>2, <3>3, <3>4 DEF TypeOKHS + <2>3. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(cs(self))) + PROVE P!cs(self) + BY <2>3 DEF cs, P!cs, TypeOKHS, TypeOK + <2>4. ASSUME NEW self \in 1..2, NoStutter(NoHistoryChange(l2(self))) + PROVE P!a4(self) + BY <2>4 DEF l2, P!a4, TypeOKHS, TypeOK + <2>5. CASE UNCHANGED <> + BY <2>5, Isa DEF vars, P!vars + <2>6. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, Zenon DEF NextHS, procHS, P!Next, P!proc + <1>3. QED + BY <1>1, <1>2, PTL, + TypingHS, MutualExclusionHS, IndInvHS + DEF SpecHS, P!Spec + + + +=============================================================================== \ No newline at end of file diff --git a/specifications/locks_auxiliary_vars/Peterson.cfg b/specifications/locks_auxiliary_vars/Peterson.cfg new file mode 100644 index 00000000..ae8a5c6b --- /dev/null +++ b/specifications/locks_auxiliary_vars/Peterson.cfg @@ -0,0 +1,3 @@ +SPECIFICATION Spec +INVARIANTS TypeOK Inv +PROPERTY LSpec \ No newline at end of file diff --git a/specifications/locks_auxiliary_vars/Peterson.tla b/specifications/locks_auxiliary_vars/Peterson.tla new file mode 100644 index 00000000..1c56470b --- /dev/null +++ b/specifications/locks_auxiliary_vars/Peterson.tla @@ -0,0 +1,191 @@ +------------------------------- MODULE Peterson ------------------------------- + +(*****************************************************************************) +(* This module contains the specification for Peterson's Algorithm, taken *) +(* from the "Parallel Programming" course taught at ULiège. *) +(* The invariant `Inv` is the one presented in the course augmented by a *) +(* clause representing mutual exclusion of the critical section *) +(* A proof is given to show that `Inv` is inductive. *) +(* Moreover the refinement from Peterson to the abstract lock is also proven.*) +(*****************************************************************************) + +EXTENDS Integers, TLAPS + +Other(p) == IF p = 1 THEN 2 ELSE 1 + +(* +--algorithm Peterson{ + variables + c = [self \in ProcSet |-> FALSE], + turn = 1; + + process(proc \in 1..2){ +a0: while(TRUE){ + skip; +a1: c[self] := TRUE; +a2: turn := Other(self); +a3: await ~c[Other(self)] \/ turn = self; +cs: skip; +a4: c[self] := FALSE; + } + } +} +*) +\* BEGIN TRANSLATION (chksum(pcal) = "1d547bc3" /\ chksum(tla) = "8de86c82") +VARIABLES pc, c, turn + +vars == << pc, c, turn >> + +ProcSet == (1..2) + +Init == (* Global variables *) + /\ c = [self \in ProcSet |-> FALSE] + /\ turn = 1 + /\ pc = [self \in ProcSet |-> "a0"] + +a0(self) == /\ pc[self] = "a0" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "a1"] + /\ UNCHANGED << c, turn >> + +a1(self) == /\ pc[self] = "a1" + /\ c' = [c EXCEPT ![self] = TRUE] + /\ pc' = [pc EXCEPT ![self] = "a2"] + /\ turn' = turn + +a2(self) == /\ pc[self] = "a2" + /\ turn' = Other(self) + /\ pc' = [pc EXCEPT ![self] = "a3"] + /\ c' = c + +a3(self) == /\ pc[self] = "a3" + /\ ~c[Other(self)] \/ turn = self + /\ pc' = [pc EXCEPT ![self] = "cs"] + /\ UNCHANGED << c, turn >> + +cs(self) == /\ pc[self] = "cs" + /\ TRUE + /\ pc' = [pc EXCEPT ![self] = "a4"] + /\ UNCHANGED << c, turn >> + +a4(self) == /\ pc[self] = "a4" + /\ c' = [c EXCEPT ![self] = FALSE] + /\ pc' = [pc EXCEPT ![self] = "a0"] + /\ turn' = turn + +proc(self) == a0(self) \/ a1(self) \/ a2(self) \/ a3(self) \/ cs(self) + \/ a4(self) + +Next == (\E self \in 1..2: proc(self)) + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION + +TypeOK == + /\ c \in [ProcSet -> BOOLEAN] + /\ turn \in ProcSet + /\ pc \in [ProcSet -> {"a0", "a1", "a2", "a3", "cs", "a4"}] + +lockcs(i) == + pc[i] \in {"cs", "a4"} +Inv == + /\ \A p \in ProcSet : c[p] <=> pc[p] \in {"a2", "a3", "cs", "a4"} + /\ \A p \in ProcSet : pc[p] \in {"cs", "a4"} + => (turn = p \/ pc[Other(p)] \in {"a0", "a1", "a2"}) + /\ \A i, j \in ProcSet: (i # j) => ~(lockcs(i) /\ lockcs(j)) + +pc_translation(label) == + CASE (label = "a0") -> "l0" + [] (label \in {"a1", "a2", "a3"}) -> "l1" + [] (label \in {"cs"}) -> "cs" + [] (label \in {"a4"}) -> "l2" + +lock_translation == IF \E p \in ProcSet : pc[p] \in {"cs", "a4"} THEN 0 ELSE 1 + +L == INSTANCE Lock + WITH pc <- [p \in ProcSet |-> pc_translation(pc[p])], + lock <- lock_translation +LSpec == L!Spec + +------------------------------------------------------------------------------- + +LEMMA Typing == Spec => []TypeOK + <1> USE DEF TypeOK + <1>1. Init => TypeOK + BY DEF ProcSet, Init + <1>2. [Next]_vars /\ TypeOK => TypeOK' + BY DEF ProcSet, Other, Next, vars, proc, a0, a1, a2, a3, cs, a4 + <1>3. QED + BY <1>1, <1>2, PTL DEF Spec + +THEOREM IndInvariant == Spec => []Inv + <1> USE DEF Inv, lockcs + <1>1. Init => Inv + BY DEF Init + <1>2. [Next]_vars /\ TypeOK /\ Inv => Inv' + <2> SUFFICES ASSUME [Next]_vars /\ TypeOK /\ Inv + PROVE Inv' + OBVIOUS + <2> USE DEF ProcSet, Other + <2>1. ASSUME NEW self \in 1..2, a0(self) + PROVE Inv' + BY <2>1 DEF a0, TypeOK + <2>2. ASSUME NEW self \in 1..2, a1(self) + PROVE Inv' + BY <2>2 DEF a1, TypeOK + <2>3. ASSUME NEW self \in 1..2, a2(self) + PROVE Inv' + BY <2>3 DEF a2, TypeOK + <2>4. ASSUME NEW self \in 1..2, a3(self) + PROVE Inv' + BY <2>4 DEF a3, TypeOK + <2>5. ASSUME NEW self \in 1..2, cs(self) + PROVE Inv' + BY <2>5 DEF cs, TypeOK + <2>6. ASSUME NEW self \in 1..2, a4(self) + PROVE Inv' + BY <2>6 DEF a4, TypeOK + <2>7. CASE UNCHANGED vars + BY <2>7 DEF vars + <2>8. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next, proc + <1>3. QED + BY <1>1, <1>2, Typing, PTL DEF Spec + +THEOREM Refinement == Spec => L!Spec + <1> USE DEF pc_translation, lock_translation, ProcSet, L!ProcSet, lockcs + <1>1. Init => L!Init + BY DEF Init, L!Init + <1>2. [Next]_vars /\ TypeOK /\ Inv => [L!Next]_L!vars + <2> USE DEF L!Next, L!vars, L!proc + <2> SUFFICES ASSUME [Next]_vars /\ TypeOK /\ Inv + PROVE [L!Next]_L!vars + OBVIOUS + <2>1. ASSUME NEW self \in 1..2, a0(self) + PROVE [L!Next]_L!vars + BY <2>1 DEF a0, L!l0, ProcSet, TypeOK, Inv + <2>2. ASSUME NEW self \in 1..2, a1(self) + PROVE [L!Next]_L!vars + BY <2>2 DEF a1, ProcSet, TypeOK, Inv + <2>3. ASSUME NEW self \in 1..2, a2(self) + PROVE [L!Next]_L!vars + BY <2>3 DEF a2, ProcSet, TypeOK, Inv + <2>4. ASSUME NEW self \in 1..2, a3(self) + PROVE [L!Next]_L!vars + BY <2>4 DEF a3, L!l1, ProcSet, TypeOK, Inv, Other + <2>5. ASSUME NEW self \in 1..2, cs(self) + PROVE [L!Next]_L!vars + BY <2>5 DEF cs, L!cs, ProcSet, TypeOK, Inv + <2>6. ASSUME NEW self \in 1..2, a4(self) + PROVE L!l2(self) + BY <2>6 DEF a4, L!l2, ProcSet, TypeOK, Inv + <2>7. CASE UNCHANGED vars + BY <2>7 DEF vars + <2>8. QED + BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 + DEF Next, proc, L!Next, L!proc + <1>3. QED + BY <1>1, <1>2, Typing, IndInvariant, PTL DEF Spec, L!Spec + +=============================================================================== diff --git a/specifications/locks_auxiliary_vars/README.md b/specifications/locks_auxiliary_vars/README.md new file mode 100644 index 00000000..4ea0e390 --- /dev/null +++ b/specifications/locks_auxiliary_vars/README.md @@ -0,0 +1,63 @@ +# Two-way refinement using auxiliary variables + +*This specification comes from a +[Master's thesis](http://hdl.handle.net/2268.2/23374)* + +Refinement proves that all behaviors implementation are a valid behavior of +an abstract specification. It is usually not done from the abstract +specification to the implementation. + +This example shows an example of this second, unusual, case using auxiliary +variables, as presented in **Prophecy made simple** by *Lamport and Merz*. + +First a refinement from Peterson's algorithm to an abstract lock is provided +in `Peterson.tla`. Second a refinement from an abstract lock with auxiliary +variables towards Peterson's algorithm is provided in `LockHS.tla` + +## Lock.tla + +The specification of an abstract lock for two processes in PlusCal. +In this abstract lock, lock acquisition is done atomically. + +The usual typing invariant and mutual exclusion are checked within the +`Lock.cfg` model and proven using TLAPS. + +## Peterson.tla + +Peterson's algorithm is a solution for mutual exclusion for 2 processes. +Each process shows its intent to enter the critical section by raising a flag +`c[self]` and can proceed if the other process does not intend to enter the +critical section or it is its turn. + +[Wikipedia](https://en.wikipedia.org/wiki/Peterson%27s_algorithm) + +This module contains the specification of Peterson's algorithm in PlusCal, and +the refinement proof towards `Lock!Spec`. + +A model that checks each invariant presented in the specification and the +refinement is given in `Peterson.cfg`. + +## LockHS.tla + +This module contains the extension of `Lock.tla` using auxiliary variables +to allow a refinement towards Peterson's algorithm. +1. The history variable `h_turn` is used to emulate the `turn` variable of + Peterson. +1. The stutter variable `s`, introduced with the `Stuttering` module, is + used to force 2 stutter steps during lock acquisition. + This allows `LockHS` to take three steps for acquiring the lock, like + `Peterson`. + +A refinement proof towards `Peterson!Spec` is presented within. + +The refinement as well as the invariants used to prove the refinement are +checked within the model `LockHS.cfg`. + +## Stuttering.tla + +This module was written for the **Auxiliary variables in TLA+** paper by +*Lamport and Merz*. (see comment at the top of the module) It eases the +addition of a stutter variable. + +For the specifications above, the module has been slightly modified, see comment +at the end of the file. \ No newline at end of file diff --git a/specifications/locks_auxiliary_vars/Stuttering.tla b/specifications/locks_auxiliary_vars/Stuttering.tla new file mode 100644 index 00000000..a8294d40 --- /dev/null +++ b/specifications/locks_auxiliary_vars/Stuttering.tla @@ -0,0 +1,192 @@ +----------------------------- MODULE Stuttering ---------------------------- +(***************************************************************************) +(* This module is explained in Section 5 of the paper "Auxiliary Variables *) +(* in TLA+". It defines operators used to add a stuttering variable s to *) +(* a specification `Spec' to form a specification SpecS. It is mean to be *) +(* instantiated with s replaced by the stuttering variable to be added and *) +(* vars replaced by the tuple of all variables in the original *) +(* specification. *) +(* *) +(* If Init is the initial predicate of `Spec', then the initial predicate *) +(* of SpecS is Init /\ (s = top) , where top is defined below. *) +(* *) +(* The next-state action of SpecS is obtained by replacing each subaction *) +(* `A' of a disjunctive representation of the next-state action Next of *) +(* `Spec' with an action `AS' written in terms of operators defined below. *) +(* (Disjunctive representations are described in Section 3.2 of "Auxiliary *) +(* Variables in TLA+".) Action `AS' executes `A' and stuttering steps *) +(* added either before or after an `A' step. The basic idea is that s *) +(* equals top except while stuttering steps are being taken, when it is a *) +(* record with the following fields: *) +(* *) +(* id: A value that identifies the action `A'. *) +(* *) +(* ctxt: A value identifying the context under which `A' is executed. *) +(* For example, if `A' appears in a formula `\E i, j \in S : A' , *) +(* this would equal the value of the pair <> for *) +(* which `A' is being executed. *) +(* *) +(* val: A value that is decremented by each stuttering step, until *) +(* it reaches a minimum value. *) +(* *) +(* The arguments of the operators defined in this module have the *) +(* following meanings. *) +(* *) +(* `A' *) +(* The subaction `A' of Next. *) +(* *) +(* id *) +(* A string identifying action `A'. *) +(* *) +(* `Sigma' *) +(* A set of values ordered by some "less-than" relation. This is *) +(* the set of possible values of s.val when executing stuttering *) +(* steps before or after subaction `A'. *) +(* *) +(* bot *) +(* The minimum element of Sigma under its less-than relation. *) +(* *) +(* initVal *) +(* The initial value to which s.val is set for executing stuttering *) +(* steps before or after `A'. *) +(* *) +(* decr *) +(* An operator such that each stuttering step changes s.val to *) +(* decr(s.val). *) +(* *) +(* `context' *) +(* The context in which `A' appears. It is the expression that is *) +(* evaluated to determine the value to which s.ctxt is set. *) +(* *) +(* `enabled' *) +(* A formula equivalent to `ENABLED A'. You can always take it to be *) +(* `ENABLED A', but you can usually find an expression that equals *) +(* `ENABLED A' in every reachable state of `Spec' but is easier for *) +(* TLC to compute. *) +(***************************************************************************) +EXTENDS Naturals, TLC +top == [top |-> "top"] + +VARIABLES s, vars + +(***************************************************************************) +(* Equals `AS' when no stuttering steps are being added before or after *) +(* `A'. *) +(***************************************************************************) +NoStutter(A) == (s = top) /\ A /\ (s' = s) + +(***************************************************************************) +(* The PostStutter and PreStutter operators define actions that perform *) +(* stuttering steps after xecuting `A' and before executing `A', *) +(* respectively. If bot = 1, initVal = 42, and decr(i) = i-1, then the *) +(* actions they define add 42 stuttering steps. They always add at least *) +(* one stuttering step. *) +(***************************************************************************) +PostStutter(A, actionId, context, bot, initVal, decr(_)) == + IF s = top THEN /\ A + /\ s' = [id |-> actionId, ctxt |-> context, val |-> initVal] + ELSE /\ s.id = actionId + /\ s.ctxt = context \* MODIFIED HERE + /\ UNCHANGED vars + /\ s'= IF s.val = bot THEN top + ELSE [s EXCEPT !.val = decr(s.val)] + +PreStutter(A, enabled, actionId, context, bot, initVal, decr(_)) == + IF s = top + THEN /\ enabled + /\ UNCHANGED vars + /\ s' = [id |-> actionId, ctxt |-> context, val |-> initVal] + ELSE /\ s.id = actionId + /\ s.ctxt = context \* MODIFIED HERE + /\ IF s.val = bot THEN /\ s.ctxt = context + /\ A + /\ s' = top + ELSE /\ UNCHANGED vars + /\ s' = [s EXCEPT !.val = decr(s.val)] + +(***************************************************************************) +(* The operators MayPostStutter and MayPreStutter are like PostStutter and *) +(* PreStutter, except they add one fewer stuttering step. For example, if *) +(* bot = 1, initVal = 42, and decr(i) = i-1, then they add 42 steps. If *) +(* initVal = bot, then they simply execute A without any added stuttering *) +(* steps. *) +(***************************************************************************) +MayPostStutter(A, actionId, context, bot, initVal, decr(_)) == + IF s = top THEN /\ A + /\ s' = IF initVal = bot + THEN s + ELSE [id |-> actionId, ctxt |-> context, + val |-> initVal] + ELSE /\ s.id = actionId + /\ s.ctxt = context \* MODIFIED HERE + /\ UNCHANGED vars + /\ s'= IF decr(s.val) = bot + THEN top + ELSE [s EXCEPT !.val = decr(s.val)] + +MayPreStutter(A, enabled, actionId, context, bot, initVal, decr(_)) == + IF s = top + THEN /\ enabled + /\ IF initVal = bot + THEN A /\ (s' = s) + ELSE /\ s' = [id |-> actionId, ctxt |-> context, val |-> initVal] + /\ UNCHANGED vars + ELSE /\ s.id = actionId + /\ s.ctxt = context \* MODIFIED HERE + /\ IF s.val = bot THEN /\ s.ctxt = context + /\ A + /\ s' = top + ELSE /\ UNCHANGED vars + /\ s' = [s EXCEPT !.val = decr(s.val)] +----------------------------------------------------------------------------- +(***************************************************************************) +(* The following operator is true iff repeatedly apply decr to any element *) +(* sig of Sigma produces a sequence sig, decr(sig), decr(decr(sig)), ... *) +(* that eventually arrives at bot. This condition should be satisfied by *) +(* the values of Sigma, bot, and decr used with the operators defined *) +(* above to add stuttering steps to an action. *) +(***************************************************************************) +StutterConstantCondition(Sigma, bot, decr(_)) == + LET InverseDecr(S) == {sig \in Sigma \ S : decr(sig) \in S} + R[n \in Nat] == IF n = 0 THEN {bot} + ELSE LET T == R[n-1] + IN T \cup InverseDecr(T) + + IN Sigma = UNION {R[n] : n \in Nat} + +(***************************************************************************) +(* TLC can evaluate StutterConstantCondition only in a model that replaces *) +(* Nat by the set 0..n for some integer n. The following operator is *) +(* equivalent to StutterConstantCondition when Sigma is a finite set, but *) +(* doesn't require modifying any definitions. *) +(***************************************************************************) +AltStutterConstantCondition(Sigma, bot, decr(_)) == + LET InverseDecr(S) == {sig \in Sigma \ S : decr(sig) \in S} + ReachBot[S \in SUBSET Sigma] == + IF InverseDecr(S) = {} THEN S + ELSE ReachBot[S \cup InverseDecr(S)] + IN ReachBot[{bot}] = Sigma +============================================================================= +\* Modification History +\* Last modified Sat Dec 31 17:47:02 PST 2016 by lamport +\* Created Tue Dec 08 11:51:34 PST 2015 by lamport + +(*****************************************************************************) +(* This module comes from : *) +(* L. Lamport and S. Merz, "Auxiliary variables in TLA+", *) +(* arXiv preprint arXiv:1703.05121, 2017. *) +(* *) +(* It has been modified slightly to ensure correctness whenever actions are *) +(* are taken during a stuttering step (e.g. modifying a history variable) *) +(* Search for the lines containing "MODIFIED HERE". *) +(* Indeed, the context variable is not always verified whenever a stutter *) +(* step is taken. *) +(* Using specifications created from PlusCal and wanting to add stuttering *) +(* to a certain transition, one might to put the label as an actionId and *) +(* the process identifier as a context. Without modifications, and in the *) +(* previously mentioned context, the stuttering does not behave correctly, *) +(* as another process could advance the stuttering and possibly break the *) +(* updating of variables. *) +(* Another solution could be to set the actionId to the <> *) +(* tuple. (this has not been verified) *) +(*****************************************************************************) \ No newline at end of file