Add ResolvedTS spec #27
Conversation
Signed-off-by: Neil Shen <overvenus@gmail.com>
| FetchTS == | ||
| /\ nextTS' = nextTS + 1 \* Try not to blew up | ||
| \* state space by increasing nextTS | ||
| /\ LET resolvedTS == IF Len(resolvedQueue) = 0 THEN 0 |
There was a problem hiding this comment.
where to use resolvedTS?
| \* resolved ts solely by FetchTS. | ||
| ResolveLiveness == | ||
| (/\ \A rm \in RM: /\ reState[rm].minPTS = 0 | ||
| /\ \E i \in 1..Len(chan): chan[i].type = "FetchTS" /\ i < chanOffset) |
There was a problem hiding this comment.
i =< chanOffset means the msg had been handled, right?
|
|
||
| \* Even if there is no write, it can always output | ||
| \* resolved ts solely by FetchTS. | ||
| ResolveLiveness == |
There was a problem hiding this comment.
I think this variant is always true, and the feature you really want to verify is that if there are any writes at some point, the resolvedTS would still forward, which also means at least one state has resolvedTS == fetchTS
| \/ (/\ rmState[rm].pTS = rmState[rm].cTS | ||
| /\ rmState[rm].pTS = 0) | ||
|
|
||
| ResolvedConsistency == |
There was a problem hiding this comment.
verify resolvedQueue # << >>
| /\ CanHandleMsg("Rollback") | ||
| /\ LET m == chan[chanOffset + 1] | ||
| IN /\ reState' = [reState EXCEPT ![m.rm].minPTS = 0] | ||
| /\ UNCHANGED <<nextTS, rmState, resolvedQueue, chan>> |
There was a problem hiding this comment.
| /\ UNCHANGED <<nextTS, rmState, resolvedQueue, chan>> | |
| /\ UNCHANGED <<nextTS, rmState, outputTSQueue, resolvedQueue, chan>> |
| chan, chanOffset>> | ||
|
|
||
| Messages == | ||
| [type: {"Prewrite", "Commit", "Rollback"}, rm: RM, ts: Nat] |
There was a problem hiding this comment.
| [type: {"Prewrite", "Commit", "Rollback"}, rm: RM, ts: Nat] | |
| [type: {"Prewrite", "Commit"}, rm: RM, ts: Nat] |
| /\ chanOffset = 0 | ||
|
|
||
| PessimisticPrewrite(r) == | ||
| LET t == nextTS - 2 \* Pessimistic Txns start TS can be stale. |
There was a problem hiding this comment.
don't get the point that using nextTS-2 in this verification, in a sense, the pessimistic transaction is exactly the same as the optimistic transaction, for a key TS is always incremental.
| \/ HandleMsgPrewrite | ||
| \/ HandleMsgCommit | ||
| \/ HandleMsgFetchTS | ||
|
|
There was a problem hiding this comment.
| \/ HandleMsgRollback | |
Signed-off-by: Neil Shen overvenus@gmail.com