[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Translational Symmetry for Model Checking

Thanks, that thread is helpful! I was thinking about it in the context of distributed protocols that utilize various types of logical version numbers. One thought was to define a VIEW function that looks at all version values in the current state, and shifts them all downward so the smallest version in that state is sent to zero e.g.

View(1,1,1) == (0,0,0) 
View(1,2,1) == (0,1,0)
View(1,2,4) == (0,1,3) 

I attached a simple experiment of this for a toy quorum based election protocol based on monotonically increasing terms/epochs. The VIEW _expression_ in TLA+ is written as:

MinTerm == Min(Range(currentTerm))
currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]
View == <<currentTermsShifted, state>>

where currentTerm is variable that maps from server identifiers to natural numbers. 

Without the view _expression_ and setting a state constraint of MaxTerm=10, TLC finds 631 reachable states for the SimpleElection spec and attached config. With the VIEW _expression_ enabled it finds 118 reachable states. For a MaxTerm=20 it finds 2461 states without the view, and 238 states with the view. For a MaxTerm=50 it finds 15151 states without the view and 598 states with it. I wonder if this approach would help reduce model checking burden for some real world specs, or if the gains in most cases wouldn't be significant enough to warrant it.

I suppose it may be sound in some cases to abstract further and have the view _expression_ only look at the ordering relationships between counter values in a state. This seems like a kind of manual predicate abstraction i.e. if a protocol only depends on the fact that one value is <,>,= another, but doesn't care about the concrete values. This seems to echo some of Ron's comments in the linked thread.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/004d850e-5165-43aa-8e6d-04d025d16aefn%40googlegroups.com.
---- MODULE SimpleElection ----
EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC

CONSTANTS Secondary, Primary, Nil

VARIABLE currentTerm

vars == <<currentTerm, state>>

\* The set of all quorums in a given set.
Quorums == {i \in SUBSET Server : Cardinality(i) * 2 > Cardinality(Server)}

\* Node 'i' gets elected as a primary.
BecomeLeader(i, voteQuorum) == 
    LET newTerm == currentTerm[i] + 1 IN
    /\ i \in voteQuorum \* The new leader should vote for itself.
    /\ \A v \in voteQuorum : currentTerm[v] < newTerm
    \* Update the terms of each voter.
    /\ currentTerm' = [s \in Server |-> IF s \in voteQuorum THEN newTerm ELSE currentTerm[s]]
    /\ state' = [s \in Server |->
                    IF s = i THEN Primary
                    ELSE IF s \in voteQuorum THEN Secondary \* All voters should revert to secondary state.
                    ELSE state[s]]    \* Allow new leaders to write a no-op on step up if they want to. It is optional, but permissible.

Init == 
    /\ currentTerm = [i \in Server |-> InitTerm]
    /\ state       = [i \in Server |-> Secondary]

Next == \E s \in Server : \E Q \in Quorums : BecomeLeader(s, Q)

Spec == Init /\ [][Next]_vars

UniqueLeader == \A s,t \in Server : 
    (/\ state[s] = Primary 
     /\ state[t] = Primary
     /\ currentTerm[s] = currentTerm[t]) => (s = t)



StateConstraint == \A s \in Server : currentTerm[s] <= MaxTerm

Range(T) == { T[x] : x \in DOMAIN T }
Min(S) == CHOOSE x \in S: \A y \in S \ {x}: y > x

\* Define a view expression that shifts all terms so 
\* that the minimum term value in the current state is shifted
\* down to zero.

MinTerm == Min(Range(currentTerm))

currentTermsShifted == [s \in Server |-> (currentTerm[s] - MinTerm)]

View == <<currentTermsShifted, state>>


Nil = Nil
Server = {n1,n2,n3}
Secondary = Secondary
Primary = Primary
MaxTerm = 50
InitTerm = 0
CONSTRAINT StateConstraint
INVARIANT UniqueLeader