зеркало из https://github.com/microsoft/CCF.git
Check refinement of high-level spec abs with all models (#6509)
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de> Co-authored-by: Amaury Chamayou <amchamay@microsoft.com>
This commit is contained in:
Markus Alexander Kuppe
GitHub
Родитель
0ab6408da1
Коммит
76b2dcfacc
|
|
@ -6,7 +6,8 @@ CONSTANTS
|
|||
NodeThree = n3
|
||||
Servers <- MCServers
|
||||
Terms <- MCTerms
|
||||
MaxLogLength <- MCMaxLogLength
|
||||
Seq <- MCSeq
|
||||
TypeOK <- MCTypeOK
|
||||
|
||||
INVARIANTS
|
||||
NoConflicts
|
||||
|
|
@ -14,6 +15,14 @@ INVARIANTS
|
|||
|
||||
PROPERTIES
|
||||
AppendOnlyProp
|
||||
\* EquivExtendProp
|
||||
\* EquivCopyMaxAndExtendProp
|
||||
|
||||
SYMMETRY
|
||||
Symmetry
|
||||
Symmetry
|
||||
|
||||
CONSTRAINT
|
||||
MaxLogLengthConstraint
|
||||
|
||||
CHECK_DEADLOCK
|
||||
FALSE
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
---- MODULE MCabs ----
|
||||
|
||||
EXTENDS abs, TLC
|
||||
EXTENDS abs, TLC, SequencesExt
|
||||
|
||||
Symmetry ==
|
||||
Permutations(Servers)
|
||||
|
|
@ -9,6 +9,17 @@ CONSTANTS NodeOne, NodeTwo, NodeThree
|
|||
|
||||
MCServers == {NodeOne, NodeTwo, NodeThree}
|
||||
MCTerms == 2..4
|
||||
MCMaxLogLength == 7
|
||||
MaxExtend == 3
|
||||
|
||||
MCTypeOK ==
|
||||
\* 4 because of the initial log.
|
||||
cLogs \in [Servers -> BoundedSeq(Terms, 4 + MaxExtend)]
|
||||
|
||||
MCSeq(S) ==
|
||||
BoundedSeq(S, MaxExtend)
|
||||
|
||||
\* Limit length of logs to terminate model checking.
|
||||
MaxLogLengthConstraint ==
|
||||
\A i \in Servers :
|
||||
Len(cLogs[i]) <= 7
|
||||
====
|
||||
|
|
@ -44,6 +44,10 @@ CONSTANTS
|
|||
NodeTwo = n2
|
||||
NodeThree = n3
|
||||
|
||||
RefinementToAbsProp <- MCRefinementToAbsProp
|
||||
Extend <- [abs]ABSExtend
|
||||
CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
|
||||
|
||||
SYMMETRY Symmetry
|
||||
VIEW View
|
||||
|
||||
|
|
@ -68,8 +72,7 @@ PROPERTIES
|
|||
MembershipStateTransitionsProp
|
||||
PendingBecomesFollowerProp
|
||||
NeverCommitEntryPrevTermsProp
|
||||
\* Will be checked after https://github.com/microsoft/CCF/pull/6509
|
||||
\* RefinementToAbsProp
|
||||
RefinementToAbsProp
|
||||
|
||||
INVARIANTS
|
||||
LogInv
|
||||
|
|
|
|||
|
|
@ -174,17 +174,8 @@ PostConditions ==
|
|||
----
|
||||
\* Refinement
|
||||
|
||||
\* The inital log is up to 4 entries long + one log entry per request/reconfiguration + one signature per request/reconfiguration or new view (no consecutive sigs except across views)
|
||||
MaxLogLength ==
|
||||
4 + ((RequestCount + Len(Configurations)) * 2) + TermCount
|
||||
|
||||
MappingToAbs ==
|
||||
INSTANCE abs WITH
|
||||
Servers <- Servers,
|
||||
Terms <- StartTerm..(StartTerm + TermCount),
|
||||
MaxLogLength <- MaxLogLength,
|
||||
cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
|
||||
|
||||
RefinementToAbsProp == MappingToAbs!AbsSpec
|
||||
MCRefinementToAbsProp == MappingToAbs(StartTerm..StartTerm + TermCount)!AbsSpec
|
||||
|
||||
ABSExtend(i) == MappingToAbs(StartTerm..StartTerm + TermCount)!ExtendAxiom(i)
|
||||
ABSCopyMaxAndExtend(i) == MappingToAbs(StartTerm..StartTerm + TermCount)!CopyMaxAndExtendAxiom(i)
|
||||
===================================
|
||||
|
|
|
|||
|
|
@ -48,6 +48,10 @@ CONSTANTS
|
|||
|
||||
InitReconfigurationVars <- SIMInitReconfigurationVars
|
||||
|
||||
RefinementToAbsProp <- MCRefinementToAbsProp
|
||||
Extend <- [abs]ABSExtend
|
||||
CopyMaxAndExtend <- [abs]ABSCopyMaxAndExtend
|
||||
|
||||
CONSTRAINT
|
||||
StopAfter
|
||||
|
||||
|
|
@ -63,6 +67,7 @@ PROPERTIES
|
|||
MembershipStateTransitionsProp
|
||||
PendingBecomesFollowerProp
|
||||
NeverCommitEntryPrevTermsProp
|
||||
RefinementToAbsProp
|
||||
|
||||
POSTCONDITION
|
||||
WriteStatsFile
|
||||
|
|
|
|||
|
|
@ -44,6 +44,15 @@ DebugInvUpToDepth ==
|
|||
\* The following invariant causes TLC to terminate with a counterexample of length
|
||||
\* -depth after generating the first trace.
|
||||
TLCGet("level") < TLCGet("config").depth
|
||||
|
||||
----
|
||||
\* Refinement
|
||||
|
||||
MCRefinementToAbsProp == MappingToAbs(Nat \ 0..StartTerm-1)!AbsSpec
|
||||
|
||||
ABSExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1)!ExtendAxiom(i)
|
||||
ABSCopyMaxAndExtend(i) == MappingToAbs(Nat \ 0..StartTerm-1)!CopyMaxAndExtendAxiom(i)
|
||||
|
||||
=============================================================================
|
||||
|
||||
------------------------------- MODULE SIMPostCondition -------------------------------
|
||||
|
|
|
|||
|
|
@ -12,9 +12,6 @@ CONSTANT Terms
|
|||
ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms)
|
||||
/\ \E min \in Terms : \A t \in Terms : t <= min
|
||||
|
||||
CONSTANT MaxLogLength
|
||||
ASSUME MaxLogLength \in Nat
|
||||
|
||||
\* Commit logs from each node
|
||||
\* Each log is append-only and the logs will never diverge.
|
||||
VARIABLE cLogs
|
||||
|
|
@ -37,14 +34,56 @@ 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 Seq(Terms) :
|
||||
cLogs' = [cLogs EXCEPT ![i] = @ \o s]
|
||||
|
||||
ExtendToMax(i) == Extend(i, MaxLogLength)
|
||||
ExtendAxiom(i) ==
|
||||
\* i has the longest log.
|
||||
/\ \A j \in Servers : Len(cLogs[j]) \leq Len(cLogs[i])
|
||||
\* cLogs remains a function mapping from servers to logs.
|
||||
/\ cLogs' \in [Servers -> Seq(Terms)]
|
||||
\* i *extends* its log
|
||||
/\ IsPrefix(cLogs[i], cLogs'[i])
|
||||
\* The other logs remain the same.
|
||||
/\ \A j \in Servers \ {i} : cLogs'[j] = cLogs[j]
|
||||
|
||||
\* Extend and ExtendAxiom are logically equivalent definitions. However,
|
||||
\* TLC can check ExtendAxiom more efficiently when checking refinement,
|
||||
\* due to the absence of the existential quantifier in the definition.
|
||||
\* The same is true for CopyMaxAndExtend and CopyMaxAndExtendAxiom below.
|
||||
LEMMA ASSUME NEW i \in Servers PROVE
|
||||
ExtendAxiom(i) <=> Extend(i)
|
||||
OMITTED
|
||||
|
||||
\* Copy one of the longest logs (from whoever server
|
||||
\* has it) and extend it further upto length k. This
|
||||
\* is equivalent to Copy(i) \cdot Extend(i, k) ,
|
||||
\* that TLC cannot handle.
|
||||
CopyMaxAndExtend(i) ==
|
||||
\E j \in Servers :
|
||||
/\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[j])
|
||||
/\ \E s \in Seq(Terms) :
|
||||
cLogs' = [cLogs EXCEPT ![i] = cLogs[j] \o s]
|
||||
|
||||
CopyMaxAndExtendAxiom(i) ==
|
||||
\E s \in Servers :
|
||||
/\ \A r \in Servers: Len(cLogs[r]) \leq Len(cLogs[s])
|
||||
\* cLogs remains a function mapping from servers to logs.
|
||||
/\ cLogs' \in [Servers -> Seq(Terms)]
|
||||
\* i *extends* s' log
|
||||
/\ IsPrefix(cLogs[s], cLogs'[i])
|
||||
\* The other logs remain the same.
|
||||
/\ \A j \in Servers \ {i} : cLogs'[j] = cLogs[j]
|
||||
|
||||
LEMMA ASSUME NEW i \in Servers PROVE
|
||||
CopyMaxAndExtendAxiom(i) <=> CopyMaxAndExtend(i)
|
||||
OMITTED
|
||||
|
||||
\* The only possible actions are to append log entries.
|
||||
\* By construction there cannot be any conflicting log entries
|
||||
|
|
@ -52,7 +91,8 @@ ExtendToMax(i) == Extend(i, MaxLogLength)
|
|||
Next ==
|
||||
\E i \in Servers :
|
||||
\/ Copy(i)
|
||||
\/ ExtendToMax(i)
|
||||
\/ ExtendAxiom(i)
|
||||
\/ CopyMaxAndExtendAxiom(i)
|
||||
|
||||
AbsSpec == Init /\ [][Next]_cLogs
|
||||
|
||||
|
|
@ -64,4 +104,11 @@ NoConflicts ==
|
|||
\/ IsPrefix(cLogs[i], cLogs[j])
|
||||
\/ IsPrefix(cLogs[j], cLogs[i])
|
||||
|
||||
EquivExtendProp ==
|
||||
[][\A i \in Servers :
|
||||
Extend(i) <=> ExtendAxiom(i)]_cLogs
|
||||
|
||||
EquivCopyMaxAndExtendProp ==
|
||||
[][\A i \in Servers :
|
||||
CopyMaxAndExtend(i) <=> CopyMaxAndExtendAxiom(i)]_cLogs
|
||||
====
|
||||
|
|
@ -1620,6 +1620,20 @@ LogMatchingProp ==
|
|||
LeaderProp ==
|
||||
[]<><<\E i \in Servers : leadershipState[i] = Leader>>_vars
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
\* Refinement of the more high-level specification abs.tla that abstracts the
|
||||
\* asynchronous network and the message passing between nodes. Instead, any
|
||||
\* node may atomically observe the state of any other node.
|
||||
|
||||
MappingToAbs(T) ==
|
||||
INSTANCE abs WITH
|
||||
Servers <- Servers,
|
||||
Terms <- T,
|
||||
cLogs <- [i \in Servers |-> [j \in 1..commitIndex[i] |-> log[i][j].term]]
|
||||
|
||||
RefinementToAbsProp == \EE T : MappingToAbs(T)!AbsSpec
|
||||
THEOREM Spec => RefinementToAbsProp
|
||||
|
||||
------------------------------------------------------------------------------
|
||||
\* Debugging invariants
|
||||
\* These invariants should give error traces and are useful for debugging to see if important situations are possible
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче