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

Minor refactorings #5880

Merged
merged 5 commits into from
Jan 2, 2024
Merged

Minor refactorings #5880

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
814c24c
Add DebugInvUpToDepth invariant to SIMccfraft to quickly generate a t…
lemmy Dec 22, 2023
2a05c28
Improve readability by removing unnecessary LET/IN.
lemmy Dec 22, 2023
8af6720
Handle empty subset outside of ChangeConfigurationInt.
lemmy Dec 22, 2023
fdfad6c
Formatting.
lemmy Dec 22, 2023
48a39b2
Show value of newConfiguration parameter of ChangeConfigurationInt in…
lemmy Dec 22, 2023
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
1 change: 1 addition & 0 deletions tla/consensus/SIMccfraft.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,3 +90,4 @@ INVARIANTS
\* DebugInvSuccessfulCommitAfterReconfig
\* DebugInvAllMessagesProcessable
\* DebugInvRetirementReachable
\* DebugInvUpToDepth
4 changes: 4 additions & 0 deletions tla/consensus/SIMccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,10 @@ StopAfter ==
(* The smoke test has a time budget of 20 minutes. *)
IN TLCSet("exit", TLCGet("duration") > timeout)

DebugInvUpToDepth ==
\* The following invariant causes TLC to terminate with a counterexample of length
\* -depth after generating the first trace.
TLCGet("level") < TLCGet("config").depth
=============================================================================

------------------------------- MODULE SIMPostCondition -------------------------------
Expand Down
31 changes: 14 additions & 17 deletions tla/consensus/ccfraft.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -635,29 +635,26 @@ SignCommittableMessages(i) ==
ChangeConfigurationInt(i, newConfiguration) ==
\* Only leader can propose changes
/\ state[i] = Leader
\* Configuration is non empty
/\ newConfiguration /= {}
\* Configuration is a proper subset of the Servers
/\ newConfiguration \subseteq Servers
\* Configuration is not equal to the previous configuration
\* Configuration is not equal to the previous configuration.
/\ newConfiguration /= MaxConfiguration(i)
\* CCF's integrity demands that a previously removed server cannot rejoin the network,
\* i.e., be re-added to a new configuration. Instead, the node has to rejoin with a
\* "fresh" identity (compare sec 6.2, page 8, https://arxiv.org/abs/2310.11559).
/\ \A s \in newConfiguration: s \notin removedFromConfiguration
\* Keep track of running reconfigurations to limit state space
/\ reconfigurationCount' = reconfigurationCount + 1
/\ removedFromConfiguration' = removedFromConfiguration \cup (CurrentConfiguration(i) \ newConfiguration)
/\ LET
entry == [
term |-> currentTerm[i],
configuration |-> newConfiguration,
contentType |-> TypeReconfiguration]
newLog == Append(log[i], entry)
IN
/\ log' = [log EXCEPT ![i] = newLog]
/\ configurations' = [configurations EXCEPT ![i] = configurations[i] @@ Len(log'[i]) :> newConfiguration]
/\ UNCHANGED <<messageVars, serverVars, candidateVars,
leaderVars, commitIndex, committableIndices>>
/\ log' = [log EXCEPT ![i] = Append(log[i],
[term |-> currentTerm[i],
configuration |-> newConfiguration,
contentType |-> TypeReconfiguration])]
/\ configurations' = [configurations EXCEPT ![i] = configurations[i] @@ Len(log'[i]) :> newConfiguration]
/\ UNCHANGED <<messageVars, serverVars, candidateVars, leaderVars, commitIndex, committableIndices>>

ChangeConfiguration(i) ==
\E newConfiguration \in SUBSET(Servers \ removedFromConfiguration) :
\* Reconfigure to any *non-empty* subset of servers. ChangeConfigurationInt checks that the new
\* configuration newConfiguration does not reintroduce nodes that have been removed previously.
\E newConfiguration \in SUBSET(Servers) \ {{}}:
lemmy marked this conversation as resolved.
Show resolved Hide resolved
ChangeConfigurationInt(i, newConfiguration)

\* Leader i advances its commitIndex to the next possible Index.
Expand Down