Merge pull request #7 from gosuda/test/tla-retire-prefix

test(tla): EPaxosRetirePrefix fold domination

Author: metaphorics

epaxos/performance_benchmark_test.go

@@ -328,3 +328,83 @@ func residentInstanceBytes(inst *instance) uintptr {
 	}
 	return bytes
 }
+
+
+func growResidentNode(b *testing.B, n int) *RawNode {
+	b.Helper()
+	rn, err := NewRawNode(Config{ID: 1, Voters: makeIDs(3)})
+	if err != nil {
+		b.Fatal(err)
+	}
+	key := []byte("bench-key")
+	for i := 1; i <= n; i++ {
+		ref := InstanceRef{Conf: 1, Replica: 1, Instance: InstanceNum(i)}
+		rec := InstanceRecord{
+			Ref: ref, Status: StatusCommitted, Seq: uint64(i), Ballot: Ballot{Replica: 1},
+			Deps: rn.q.deps(), Command: Command{Payload: []byte("x"), ConflictKeys: [][]byte{key}},
+		}
+		rec.Checksum = ChecksumRecord(rec)
+		rn.installInstance(&instance{rec: rec, phase: phaseCommitted})
+	}
+	return rn
+}
+
+func BenchmarkComputeAttrsResident1k(b *testing.B) {
+	rn := growResidentNode(b, 1000)
+	cmd := Command{Payload: []byte("y"), ConflictKeys: [][]byte{[]byte("bench-key")}}
+	exclude := InstanceRef{Conf: 1, Replica: 1, Instance: 1001}
+	b.ReportAllocs()
+	b.ResetTimer()
+	for i := 0; i < b.N; i++ {
+		_ = rn.computeAttrs(cmd, exclude)
+	}
+}
+
+func BenchmarkComputeAttrsResident100k(b *testing.B) {
+	if testing.Short() {
+		b.Skip("100k resident bench")
+	}
+	rn := growResidentNode(b, 100000)
+	cmd := Command{Payload: []byte("y"), ConflictKeys: [][]byte{[]byte("bench-key")}}
+	exclude := InstanceRef{Conf: 1, Replica: 1, Instance: 100001}
+	b.ReportAllocs()
+	b.ResetTimer()
+	for i := 0; i < b.N; i++ {
+		_ = rn.computeAttrs(cmd, exclude)
+	}
+}
+
+func BenchmarkStepPreAcceptGrown(b *testing.B) {
+	rn := growResidentNode(b, 1000)
+	b.ReportAllocs()
+	b.ResetTimer()
+	for i := 0; i < b.N; i++ {
+		ref := InstanceRef{Conf: 1, Replica: 2, Instance: InstanceNum(i + 1)}
+		cmd := Command{ID: CommandID{Client: 9, Sequence: uint64(i + 1)}, Payload: []byte("z"), ConflictKeys: [][]byte{[]byte("bench-key")}}
+		msg := Message{Type: MsgPreAccept, From: 2, To: 1, Ref: ref, Ballot: Ballot{Replica: 2}, Command: cmd}
+		_ = rn.Step(msg)
+	}
+}
+
+func BenchmarkRetireExecuted(b *testing.B) {
+	b.ReportAllocs()
+	for i := 0; i < b.N; i++ {
+		b.StopTimer()
+		rn, err := NewRawNode(Config{ID: 1, Voters: makeIDs(3), RetainExecutedPerLane: 8})
+		if err != nil {
+			b.Fatal(err)
+		}
+		for j := 1; j <= 64; j++ {
+			ref := InstanceRef{Conf: 1, Replica: 1, Instance: InstanceNum(j)}
+			rec := InstanceRecord{
+				Ref: ref, Status: StatusExecuted, Seq: uint64(j), Ballot: Ballot{Replica: 1},
+				Deps: rn.q.deps(), Command: Command{Payload: []byte("x"), ConflictKeys: [][]byte{[]byte("k")}},
+			}
+			rec.Checksum = ChecksumRecord(rec)
+			rn.installInstance(&instance{rec: rec, phase: phaseCommitted})
+			rn.executed.add(ref)
+		}
+		b.StartTimer()
+		rn.retireExecuted()
+	}
+}

tests/tla_model_check.sh

@@ -190,6 +190,11 @@ for cfg in tla/KVOmissionRecovery.cfg; do
 done
 
 run_tlc tla/Quorum.tla tla/Quorum.cfg
+
+for cfg in tla/EPaxosRetirePrefix.cfg; do
+  run_tlc tla/EPaxosRetirePrefix.tla "$cfg"
+done
+
 for cfg in tla/EPaxosVoterBootstrapSize1.cfg tla/EPaxosVoterBootstrapSize2.cfg tla/EPaxosVoterBootstrapSize3.cfg tla/EPaxosVoterBootstrapSize4.cfg tla/EPaxosVoterBootstrapSize5.cfg tla/EPaxosVoterBootstrapSize6.cfg tla/EPaxosVoterBootstrapCrashPrefix.cfg tla/EPaxosVoterBootstrapRace.cfg tla/EPaxosVoterBootstrapFair.cfg; do
   run_tlc tla/EPaxosVoterBootstrap.tla "$cfg"
 done

tests/tla_model_check_runner.py

@@ -28,6 +28,7 @@
 )
 
 FAST_PROFILE = (
+    ("tla/EPaxosRetirePrefix.tla", "tla/EPaxosRetirePrefix.cfg"),
     ("tla/ReadyAdvance.tla", "tla/ReadyAdvance.cfg"),
     ("tla/ReadyAdvance.tla", "tla/ReadyAdvanceCapped.cfg"),
     ("tla/Quorum.tla", "tla/Quorum.cfg"),
@@ -46,6 +47,7 @@
 )
 
 FULL_PROFILE = (
+    ("tla/EPaxosRetirePrefix.tla", "tla/EPaxosRetirePrefix.cfg"),
     *(("tla/EPaxos.tla", cfg) for cfg in ("tla/EPaxos.cfg", "tla/EPaxosKVConflict.cfg", "tla/EPaxosThreeReplica.cfg")),
     *(("tla/ReadyAdvance.tla", cfg) for cfg in ("tla/ReadyAdvance.cfg", "tla/ReadyAdvanceCapped.cfg")),
     *(("tla/EPaxosResponses.tla", cfg) for cfg in ("tla/EPaxosResponses.cfg", "tla/EPaxosResponsesFive.cfg")),

tla/EPaxosRetirePrefix.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  MaxI = 3
+  MaxS = 3
+  Lanes = {l1, l2}
+INVARIANT Inv
+CHECK_DEADLOCK FALSE

tla/EPaxosRetirePrefix.tla

@@ -0,0 +1,61 @@
+---- MODULE EPaxosRetirePrefix ----
+EXTENDS Naturals, FiniteSets
+
+\* Two lanes, instances 1..MaxI. Folding a present instance advances folded
+\* and retains max seq. Invariant: folded instances are absent from present,
+\* and retiredMaxSeq is monotonic and bounded.
+
+CONSTANTS MaxI, MaxS, Lanes
+
+VARIABLES seq, present, folded, retiredMaxSeq
+
+vars == <<seq, present, folded, retiredMaxSeq>>
+
+TypeOK ==
+  /\ seq \in [Lanes -> [1..MaxI -> 1..MaxS]]
+  /\ present \in [Lanes -> SUBSET (1..MaxI)]
+  /\ folded \in [Lanes -> 0..MaxI]
+  /\ retiredMaxSeq \in [Lanes -> 0..MaxS]
+
+Init ==
+  /\ seq = [lane \in Lanes |-> [i \in 1..MaxI |-> 1]]
+  /\ present = [lane \in Lanes |-> {}]
+  /\ folded = [lane \in Lanes |-> 0]
+  /\ retiredMaxSeq = [lane \in Lanes |-> 0]
+
+Install(lane, i, s) ==
+  /\ i \in 1..MaxI
+  /\ s \in 1..MaxS
+  /\ i > folded[lane]
+  /\ present' = [present EXCEPT ![lane] = @ \union {i}]
+  /\ seq' = [seq EXCEPT ![lane][i] = s]
+  /\ UNCHANGED <<folded, retiredMaxSeq>>
+
+FoldOne(lane) ==
+  /\ folded[lane] < MaxI
+  /\ (folded[lane] + 1) \in present[lane]
+  /\ LET n == folded[lane] + 1 IN
+       /\ folded' = [folded EXCEPT ![lane] = n]
+       /\ present' = [present EXCEPT ![lane] = @ \ {n}]
+       /\ retiredMaxSeq' =
+            [retiredMaxSeq EXCEPT ![lane] =
+               IF seq[lane][n] > retiredMaxSeq[lane] THEN seq[lane][n] ELSE retiredMaxSeq[lane]]
+       /\ UNCHANGED seq
+
+Next ==
+  \/ \E lane \in Lanes, i \in 1..MaxI, s \in 1..MaxS: Install(lane, i, s)
+  \/ \E lane \in Lanes: FoldOne(lane)
+
+Spec == Init /\ [][Next]_vars
+
+\* Folded prefix is disjoint from present; retired max seq never exceeds MaxS
+\* and is at least the seq of any still-folded boundary instance when defined.
+Inv ==
+  /\ TypeOK
+  /\ \A lane \in Lanes:
+       /\ \A i \in present[lane]: i > folded[lane]
+       /\ retiredMaxSeq[lane] \in 0..MaxS
+       /\ \A i \in 1..MaxI:
+            (i <= folded[lane]) => (seq[lane][i] <= retiredMaxSeq[lane])
+
+====