chore(MultiPaxos): separate model from specification (#10)

.github/workflows/tlc.yaml

@@ -21,7 +21,7 @@ jobs:
     strategy:
       matrix:
         file:
-          - multi-paxos-eb0/MultiPaxos.tla
+          - multi-paxos-eb0/MC.tla
           - paxos-eb0/PaxosEb0.tla
           - percolator/Transfer.tla
           - percolator/SnapshotRead.tla

multi-paxos-eb0/MultiPaxos.cfg → multi-paxos-eb0/MC.cfg

@@ -3,7 +3,7 @@ CONSTANTS
   Acceptor = {a1, a2, a3}
   Quorum = {{a1, a2}, {a1, a3}, {a2, a3}}
   Ballot = {0, 1}
-  MaxSeq = 2
+  Seq = {0, 1}
   Proposer = {p1, p2}
   None = None
 INVARIANT Inv

multi-paxos-eb0/MC.tla

@@ -0,0 +1,19 @@
+--------------- MODULE MC ---------------
+
+CONSTANT Value, Acceptor, Quorum, Ballot, Seq, Proposer, None
+
+VARIABLE msgs,
+         proposerStates,
+         acceptorStates,
+         committed
+
+INSTANCE MultiPaxos
+
+Constraint ≜
+    ∧ ∀p ∈ Proposer: proposerStates[p].nextSeq ∈ Seq
+
+Symmetry ≜ Permutations(Acceptor)
+    ∪ Permutations(Proposer)
+    ∪ Permutations(Value)
+
+===============================================

multi-paxos-eb0/MultiPaxos.tla

@@ -1,25 +1,29 @@
 -------------------------------- MODULE MultiPaxos -------------------------------
 EXTENDS Integers, TLC, FiniteSets
 
-CONSTANT Value, Acceptor, Quorum, Ballot, MaxSeq, Proposer, None
+CONSTANT Value, Acceptor, Quorum, Ballot, Seq, Proposer, None
 
 ASSUME QuorumAssumption ≜
     ∧ ∀ Q ∈ Quorum : Q ⊆ Acceptor
     ∧ ∀ Q1, Q2 ∈ Quorum : Q1 ∩ Q2 ≠ {} 
+
+VARIABLE msgs,
+         proposerStates,
+         acceptorStates,
+         committed
+
+vars ≜ ⟨msgs, proposerStates, acceptorStates, committed⟩
+
 
 LEADER ≜ "Leader"
 CANDIDATE ≜ "Candidate"
 
-Seq ≜ (0‥MaxSeq)
-
 Max(S) ≜ CHOOSE x ∈ S: ∀y ∈ S: x ≥ y
 QS ≜ Cardinality(Acceptor) ÷ 2 + 1
 
-\* lss: Last Success Sequence
 ProposerState ≜
     [ id: Proposer
     , role: { LEADER, CANDIDATE }
-    , lss: Seq ∪ { -1 }
     , nextSeq: Seq
     ]
 
@@ -54,31 +58,9 @@ Committed ≜
     , val: Value
     ]
 
-VARIABLE msgs,
-         proposerStates,
-         acceptorStates,
-         committed
-
-vars ≜ ⟨msgs, proposerStates, acceptorStates, committed⟩
-
-TypeOK ≜ 
-    ∧ msgs ⊆ Message
-    ∧ proposerStates ∈ [ Proposer → ProposerState ]
-    ∧ acceptorStates ∈ [ Acceptor → AcceptorState ]
-    ∧ committed ⊆ Committed
-
-Constraint ≜
-    ∧ ∀p ∈ Proposer: proposerStates[p].lss < MaxSeq
-    ∧ ∀p ∈ Proposer: proposerStates[p].nextSeq < MaxSeq
-
-Symmetry ≜ Permutations(Acceptor)
-    ∪ Permutations(Proposer)
-    \* ∪ Permutations(Quorum)
-    ∪ Permutations(Value)
-
 Init ≜ ∧ msgs = {}
        ∧ proposerStates = [ p ∈ Proposer ↦ 
-            [ id ↦ p, role ↦ CANDIDATE, lss ↦ -1, nextSeq ↦ 0 ] ]
+            [ id ↦ p, role ↦ CANDIDATE, nextSeq ↦ 0 ] ]
        ∧ acceptorStates = [ a ∈ Acceptor ↦
             [ id ↦ a, seqs ↦  [ s ∈ Seq ↦ EmptySeqState] ] ]
        ∧ committed = {}
@@ -88,13 +70,10 @@ Send(m) ≜ msgs' = msgs ∪ {m}
 LastCommittedSeq ≜ Max({ c.seq: c ∈ committed })
 
 LearnLastCommitted(p) ≜
-    \* ∧ p.role = CANDIDATE
     ∧ committed ≠ {}
     ∧ LastCommittedSeq ≥ p.nextSeq
     ∧ proposerStates' = [ proposerStates EXCEPT ![p.id] = 
-            [ id ↦ p.id, role ↦ CANDIDATE, lss ↦ p.lss, nextSeq ↦ LastCommittedSeq + 1 ] ]
-    \* ∧ proposerStates' = [ proposerStates EXCEPT ![p.id].role = CANDIDATE ]
-        \* ^ p.nextSeq' = LastCommittedSeq
+            [ id ↦ p.id, role ↦ CANDIDATE, nextSeq ↦ LastCommittedSeq + 1 ] ]
     ∧ UNCHANGED ⟨msgs, acceptorStates, committed⟩
 
 Phase1a(p) ≜ ∃b ∈ Ballot:
@@ -132,7 +111,6 @@ Phase2a(p) ≜ ∃b ∈ Ballot:
 
 FastPhase2a(p) ≜ ∃v ∈ Value:
     ∧ p.role = LEADER
-    ∧ p.nextSeq = p.lss + 1
     ∧ ¬ ∃m ∈ msgs : m.type = "2a" ∧ m.pid = p.id ∧ m.seq = p.nextSeq ∧ m.bal = 0
     ∧ Send([type ↦ "2a", pid ↦ p.id, seq ↦ p.nextSeq, bal ↦ 0, val ↦ v, valSrc ↦ p.id])
     ∧ UNCHANGED ⟨committed, proposerStates, acceptorStates⟩
@@ -146,12 +124,6 @@ Phase2b(a) ≜ ∃ m ∈ msgs:
             val ↦ m.val, valSrc ↦ m.valSrc]) 
     ∧ UNCHANGED ⟨committed, proposerStates⟩
 
-\* votes ≜ [a ∈ Acceptor ↦  
-\*     {⟨m.seq, m.bal, m.val⟩ : m ∈ {mm ∈ msgs: ∧ mm.type = "2b"
-\*                                              ∧ mm.acc = a }}]
-\* 
-\* VotedFor(a, seq, b, v) ≜ ⟨seq, b, v⟩ ∈ votes[a]
-
 Commit(p) ≜ ∃b ∈ Ballot, v ∈ Value, valSrc ∈ Proposer:
     ∧ ∃Q ∈ Quorum: ∀a ∈ Q: ∃m ∈ msgs:
         ∧ m.type = "2b"
@@ -164,7 +136,7 @@ Commit(p) ≜ ∃b ∈ Ballot, v ∈ Value, valSrc ∈ Proposer:
     ∧ committed' = committed ∪ {[ seq ↦ p.nextSeq, pid ↦  p.id, val ↦ v]}
     ∧ LET newRole ≜ IF valSrc = p.id THEN LEADER ELSE CANDIDATE
         IN proposerStates' = [ proposerStates EXCEPT ![p.id] = 
-            [ id ↦ p.id, role ↦ newRole, lss ↦ p.nextSeq, nextSeq ↦ p.nextSeq + 1 ]]
+            [ id ↦ p.id, role ↦ newRole, nextSeq ↦ p.nextSeq + 1 ]]
     ∧ UNCHANGED ⟨msgs, acceptorStates⟩
 
 ProposerNext ≜ ∃pid ∈ Proposer: LET p ≜ proposerStates[pid] IN
@@ -185,7 +157,7 @@ Next ≜
 Spec ≜ Init ∧ □[Next]_vars
 ----------------------------------------------------------------------------
 
-Inv ≜ ∧ TypeOK
-      ∧ ∀c1, c2 ∈ committed:
-            c1.seq = c2.seq ⇒ c1.val = c2.val
+Inv ≜ 
+    ∀c1, c2 ∈ committed:
+        c1.seq = c2.seq ⇒ c1.val = c2.val
 ============================================================================

multi-paxos-eb0/readme.md

@@ -35,13 +35,10 @@ or other systems that require higher availability but not frequent linearizable
 
 ## Checking time
 
-Hardware:
-
-8Cores
-
-Ballot = {0, 1}, MaxSeq = 2 => 1s
-
-Ballot = {0, 1}, MaxSeq = 3 => 13min 21s
+  | Hardware | Ballot | Seq       | time       |
+  | _        | _      | _         | _          |
+  | 8 Cores  | {0, 1} | {0, 1}    | 1s         |
+  | 8 Cores  | {0, 1} | {0, 1, 2} | 13 min 21s |
 
 ## TODO
 

readme.md

@@ -17,11 +17,11 @@ Verify some old or new concepts/models/algorithms/ideas of distributed/discrete
 
 What's Next:
 
-- [X] Github CI
-- [ ] Separate model from specification
+- [X] GitHub CI
+- [x] Separate model from specification
 - [X] Modeling Transaction Isolation Levels
-- [x] Add Liveness Invariants
-- [ ] Distributed Transaction On Sql Databases
+- [x] Add Liveness Properties
+- [ ] Distributed Transaction On SQL Databases
 - [ ] HLC and Quorum Intersection
 
 ## Q & A