Add MultiPaxos Leader Leases spec - #224
Conversation
Signed-off-by: Guanzhou Hu <josehgz@amazon.com>
muenchnerkindl
left a comment
muenchnerkindl
left a comment
There was a problem hiding this comment.
Thank you for your submission. I added a few comments and observations about your spec, hope you find them useful.
| (*************************) | ||
| (* Type check invariant. *) | ||
| (*************************) | ||
| TypeOK == /\ \A m \in msgs: m \in Messages |
There was a problem hiding this comment.
Why doesn't this go to MultiPaxos.tla? It is not just relevant for model checking.
| (* Type check invariant. *) | ||
| (*************************) | ||
| TypeOK == /\ \A m \in msgs: m \in Messages | ||
| /\ \A r \in Replicas: node[r] \in NodeStates |
There was a problem hiding this comment.
A typing invariant should have conjuncts such as
node \in [Replicas -> NodeStates]
that fixes the type of each variable. Note that in TLA+ you cannot deduce the predicate above from the one that you write.
| /\ \A r \in Replicas: node[r] \in NodeStates | ||
| /\ \A r \in Replicas: time[r] \in Times | ||
| /\ Len(pending) =< NumCommands | ||
| /\ Cardinality(Range(pending)) = Len(pending) |
There was a problem hiding this comment.
Consider using a predicate such as IsInjective from module Functions.tla in the CommunityModules.
| /\ \A r \in Replicas: time[r] \in Times | ||
| /\ Len(pending) =< NumCommands | ||
| /\ Cardinality(Range(pending)) = Len(pending) | ||
| /\ \A c \in Range(pending): c \in Commands |
There was a problem hiding this comment.
pending \in Seq(Commands)
| (*************************************) | ||
| (* Lease expiration safety property. *) | ||
| (*************************************) | ||
| LeaseExpirationSafety == |
There was a problem hiding this comment.
Again, this is a correctness property that should go to the main module rather than to the _MC module.
| ReadsAssumption == /\ IsFiniteSet(Reads) | ||
| /\ Cardinality(Reads) >= 0 | ||
| /\ "nil" \notin Writes | ||
|
|
There was a problem hiding this comment.
Also, should the sets Reads and Writes be disjoint? Consider introducing an operator ReadsWritesAssumption that lists all assumptions on commands.
| AckEvent(c, v) == [type |-> "Ack", cmd |-> c, val |-> v] | ||
| \* for a write command, val is the old value | ||
|
|
||
| InitPending == (CHOOSE ws \in [1..Cardinality(Writes) -> Writes] |
There was a problem hiding this comment.
This fixes an arbitrary but fixed (injective) sequence of Writes. Alternatively, you could set up your model so that all possible such sequences are verified – certainly at the cost of even heavier state space explosion.
| end with; | ||
| end macro; | ||
|
|
||
| \* Replica node crashes itself under promised conditions. |
There was a problem hiding this comment.
What do you mean by "promised conditions"?
| \* if fewer than (N - MajorityNum) number of replicas have failed | ||
| await /\ MajorityNum + numCrashed < Cardinality(Replicas) | ||
| /\ ~crashed[r] | ||
| /\ node[r].balMaxKnown < MaxBallot; |
There was a problem hiding this comment.
This condition is not explained in the comment.
| end macro; | ||
|
|
||
| \* Advances time by one tick globally, and garbage-collects expired lease | ||
| \* state. Per-pair seq counters are preserved across GC. |
There was a problem hiding this comment.
If time is modeled globally (i.e., all replicas share the same time at every moment), why model it as a local (pre-replica) variable that is updated simultaneously for all replicas? A global variable would show more clearly how time is represented in this spec.
2 participants
Adds a MultiPaxos Leader Leases spec. This spec builds on top of the earlier MultiPaxos-SMR spec. Please see specifications/MultiPaxos-LeaderLeases/README.md for more information on what it models.
Due to the nature of the leasing algorithm, checking the default config is a rather heavy task and runs for ~20 hours on a powerful EC2 instance. I included a
_shortvariant of the config that completes in ~1 minute for validation purposes.