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.
| 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.
There was a problem hiding this comment.
Agreed. For the purpose of this spec, I think naming an arbitrary sequence is enough because Writes is anyways a symmetric set. There's no significance to any particular permutation. Checking one sequence generalizes to all.
| 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"?
There was a problem hiding this comment.
I meant "when > majority number of nodes are healthy", in which case crashing one more doesn't block the protocol from making progress.
This was added because the spec originally only modeled termination when all commands are processed. I'll remove this condition and instead consider termination when all replicas have crashed or reached max time ticks. That would be a more proper approach.
| 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.
There was a problem hiding this comment.
I would think a per-node clock matches the leasing algorithm more closely. Nodes don't have a global sense of time. They all compute their own expiration timestamps using their own clock.
For simplicity, this spec initializes all nodes clock to 1 and advances them by the same amount 1 for every tick. In reality, the first half is not needed for leases to work: nodes don't need to align on their absolute clock vlaues (i.e., clock skew is okay), only how fast they think time flies (i.e., bounded clock drift). Per-node clocks better captures this aspect.
Will add comments inline to clarify.
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.