Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Model max_uncommitted_tx_count of raft.h in abs.tla #6508

Closed
wants to merge 2 commits into from
Closed

Model max_uncommitted_tx_count of raft.h in abs.tla #6508

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e14391a
Align spec with CCF by replacing global upper bound MaxLogLength
lemmy Sep 26, 2024
8620bd4
Limit the global length of all logs to 7 during model checking.
lemmy Sep 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions tla/consensus/MCabs.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ CONSTANTS
NodeThree = n3
Servers <- MCServers
Terms <- MCTerms
MaxLogLength <- MCMaxLogLength
MaxUncommittedCount = 3

INVARIANTS
NoConflicts
Expand All @@ -16,4 +16,7 @@ PROPERTIES
AppendOnlyProp

SYMMETRY
Symmetry
Symmetry

CONSTRAINT
MaxLogLengthConstraint
5 changes: 4 additions & 1 deletion tla/consensus/MCabs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,9 @@ CONSTANTS NodeOne, NodeTwo, NodeThree

MCServers == {NodeOne, NodeTwo, NodeThree}
MCTerms == 2..4
MCMaxLogLength == 7

\* Limit length of logs to terminate model checking.
MaxLogLengthConstraint ==
\A i \in Servers :
Len(cLogs[i]) <= 7
====
2 changes: 1 addition & 1 deletion tla/consensus/MCccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ MappingToAbs ==
INSTANCE abs WITH
Servers <- Servers,
Terms <- StartTerm..MaxTermLimit,
MaxLogLength <- MaxLogLength,
MaxUncommittedCount <- MaxLogLength,
cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]

RefinementToAbsProp == MappingToAbs!AbsSpec
Expand Down
21 changes: 12 additions & 9 deletions tla/consensus/abs.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,11 @@ CONSTANT Terms
ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms)
/\ \E min \in Terms : \A t \in Terms : t <= min

CONSTANT MaxLogLength
ASSUME MaxLogLength \in Nat
\* See `max_uncommitted_tx_count` in raft.h: Maximum number of
\* uncommitted transactions allowed before the primary refuses
\* new transactions. Unlimited if set to 0.
CONSTANT MaxUncommittedCount
ASSUME MaxUncommittedCount \in Nat

\* Commit logs from each node
\* Each log is append-only and the logs will never diverge.
Expand All @@ -37,22 +40,22 @@ Copy(i) ==
/\ \E l \in 1..(Len(cLogs[j]) - Len(cLogs[i])) :
cLogs' = [cLogs EXCEPT ![i] = @ \o SubSeq(cLogs[j], Len(@) + 1, Len(@) + l)]

\* A node i with the longest log can extend its log upto length k.
Extend(i, k) ==
\* A node i with the longest log can non-deterministically extend
\* its log by any finite number of log entries. An implementation
\* may choose a particular number of log entries by which to extend
\* the log to prevent the leader from racing ahead of the followers.
Extend(i) ==
/\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
/\ \E l \in 0..(k - Len(cLogs[i])) :
\E s \in [1..l -> Terms] :
/\ \E s \in BoundedSeq(Terms, MaxUncommittedCount) :
cLogs' = [cLogs EXCEPT ![i] = @ \o s]

ExtendToMax(i) == Extend(i, MaxLogLength)

\* The only possible actions are to append log entries.
\* By construction there cannot be any conflicting log entries
\* Log entries are copied if the node's log is not the longest.
Next ==
\E i \in Servers :
\/ Copy(i)
\/ ExtendToMax(i)
\/ Extend(i)

AbsSpec == Init /\ [][Next]_cLogs

Expand Down