Unify TLC models for barriers

Adding descriptions

Author: JarodDif

specifications/barriers/Barrier.cfg

@@ -1,3 +1,4 @@
-CONSTANT N = 7
+CONSTANT N = 6
 SPECIFICATION Spec
-INVARIANT TypeOK
+INVARIANT TypeOK 
+PROPERTY BarrierProperty

specifications/barriers/Barrier.tla

@@ -32,4 +32,9 @@ 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
+
 ===============================================================================

specifications/barriers/Barriers.cfg

@@ -1,3 +1,4 @@
-CONSTANT N = 7
+CONSTANT N = 6
 SPECIFICATION Spec
 INVARIANTS TypeOK LockInv Inv FlushInv
+PROPERTY BSpec

specifications/barriers/Barriers.tla

@@ -6,12 +6,12 @@ CONSTANTS
   N
 
 (**
---algorithm Barrier {
+--algorithm Barriers {
     variables
-      lock = 1,
-      gate_1 = 0,
-      gate_2 = 0,
-      rdv = 0;
+      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;
@@ -31,28 +31,38 @@ CONSTANTS
         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;
+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;
+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) = "fa4cafb2" /\ chksum(tla) = "4cd2e9fd")
+\* BEGIN TRANSLATION (chksum(pcal) = "7a2331f4" /\ chksum(tla) = "4cd2e9fd")
 VARIABLES pc, lock, gate_1, gate_2, rdv
 
 vars == << pc, lock, gate_1, gate_2, rdv >>
@@ -239,6 +249,7 @@ pc_translation(self) ==
   ELSE "b1"
 
 B == INSTANCE Barrier WITH pc <- [p \in ProcSet |-> pc_translation(p)]
+BSpec == B!Spec
 
 -------------------------------------------------------------------------------
 

specifications/barriers/MCBarriers.cfg

@@ -1,16 +1,26 @@
 # Barrier synchronization
--
+
+## 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 rooms `a1-a6` and `a7-a12`. 
-The last process entering a waiting room signals the appropriate semaphore
+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 rooms makes sure a process leaving the barrier cannot
+Using two such waiting chambers makes sure a process leaving the barrier cannot
 reenter and pass through the whole barrier again.
 
 ## Invariants
@@ -26,20 +36,12 @@ reenter and pass through the whole barrier again.
 - `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 = 7$ that verifies these four invariants is 
+A model `Barriers.cfg` with $N = 6$ that verifies these four invariants is 
 provided.
 
 ## Refinement
 
 A refinement towards an abstract Barrier specification is proven with TLAPS.
 
 A model `MCBarriers.cfg` and its companion `MCBarriers.tla` verifies if
-`B!Spec` (the abstract Barrier specification) holds for `Spec` 
-
-## Barrier.tla
-
-A specification of an abstract Barrier.
-
-The usual typing invariant is defined.
-
-A model with the same amount of processes as above is provided. 
+`B!Spec` (the abstract Barrier specification) holds for `Spec`