Experiment with different GC methods

Author: ahelwer

specifications/FiniteMonotonic/MC_ReplicatedLog.cfg

@@ -1,4 +1,4 @@
-SPECIFICATION Spec
+SPECIFICATION SimpleSpec
 CONSTANTS
   Node = {n1, n2, n3}
   Transaction = {tx1, tx2, tx3}

specifications/FiniteMonotonic/MC_ReplicatedLog.tla

@@ -21,7 +21,7 @@ Init ==
   /\ converge = FALSE
 
 \* Experiment with combining the write & garbage collect steps
-WriteTx(n, tx) ==
+GCWriteTx(n, tx) ==
   LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
   LET MinExecuted == SetMin({executed[o] : o \in Node}) IN
   LET NewTxId == Len(log) - MinExecuted + 1 IN
@@ -34,31 +34,80 @@ WriteTx(n, tx) ==
     ]
   /\ executed' = [
       o \in Node |->
-        IF o /= n THEN executed[o] - MinExecuted ELSE NewTxId
+        IF o = n THEN NewTxId ELSE executed[o] - MinExecuted
     ]
   /\ UNCHANGED converge
 
-ExecuteTx(n) ==
+\* Experiment with combining the execute & garbage collect steps
+GCExecuteTx(n) ==
+  LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
+  LET MinExecuted == SetMin({
+    IF o = n THEN executed[o] + 1 ELSE executed[o] : o \in Node
+  }) IN
+  /\ log' = [i \in 1 .. Len(log) - MinExecuted |-> log[i + MinExecuted]]
+  /\ executed' = [
+      o \in Node |->
+        IF o = n
+        THEN executed[o] - MinExecuted + 1
+        ELSE executed[o] - MinExecuted
+    ]
+  /\ UNCHANGED converge
+
+SimpleWriteTx(n, tx) ==
+  /\ ~converge
+  /\ Len(log) < Divergence
+  /\ S!WriteTx(n, tx)
+  /\ UNCHANGED converge
+
+SimpleExecuteTx(n) ==
   /\ S!ExecuteTx(n)
   /\ UNCHANGED converge
 
+GarbageCollect ==
+  LET SetMin(s) == CHOOSE e \in s : \A o \in s : e <= o IN
+  LET MinExecuted == SetMin({executed[o] : o \in Node}) IN
+  /\ log' = [i \in 1 .. Len(log) - MinExecuted |-> log[i + MinExecuted]]
+  /\ executed' = [n \in Node |-> executed[n] - MinExecuted]
+  /\ UNCHANGED converge
+
 Converge ==
   /\ converge' = TRUE
   /\ UNCHANGED <<log, executed>>
 
-Next ==
-  \/ \E n \in Node : \E tx \in Transaction : WriteTx(n, tx)
-  \/ \E n \in Node : ExecuteTx(n)
+GCWriteNext ==
+  \/ \E n \in Node : \E tx \in Transaction : GCWriteTx(n, tx)
+  \/ \E n \in Node : SimpleExecuteTx(n)
+  \/ Converge
+
+SimpleFairness == \A n \in Node : WF_vars(SimpleExecuteTx(n))
+
+GCWriteSpec ==
+  /\ Init
+  /\ [][GCWriteNext]_vars
+  /\ SimpleFairness
+
+GCExecuteNext ==
+  \/ \E n \in Node : \E tx \in Transaction : GCWriteTx(n, tx)
+  \/ \E n \in Node : SimpleExecuteTx(n)
   \/ Converge
 
-Fairness == \A n \in Node : WF_vars(ExecuteTx(n))
+GCFairness == \A n \in Node : WF_vars(GCExecuteTx(n))
 
-Test == Len(log) /= Divergence
+GCExecuteSpec ==
+  /\ Init
+  /\ [][GCExecuteNext]_vars
+  /\ GCFairness
+
+SimpleNext ==
+  \/ \E n \in Node : \E tx \in Transaction : SimpleWriteTx(n, tx)
+  \/ \E n \in Node : SimpleExecuteTx(n)
+  \/ GarbageCollect
+  \/ Converge
 
-Spec ==
+SimpleSpec ==
   /\ Init
-  /\ [][Next]_vars
-  /\ Fairness
+  /\ [][SimpleNext]_vars
+  /\ SimpleFairness
 
 =============================================================================