added WriteAndVerify committing #44
Conversation
|
/cc @3pointer @overvenus Would you take a look? Thanks! |
PutAndVerify/MC.tla
Outdated
| ---- | ||
|
|
||
| \* MV CONSTANT definitions CLIENTS | ||
| const_171964209906974000 == |
There was a problem hiding this comment.
this TLA spec is not heavy, can you add more clients?
There was a problem hiding this comment.
I run it with 3 clients and no error reported. Also if someone wants to verify with more clients, he may modify the model constants manually.
I prefer keeping two clients by default because the state transform graph can still be read by a human... Starting from 3 the state transform gets too complex to be read...
PutAndVerify/WriteAndVerify.tla
Outdated
|
|
||
| (* Delete the file when aborted. *) | ||
| RollBack(c) == /\ clState[c] = "aborted" | ||
| /\ storage[c] /= "none" |
There was a problem hiding this comment.
In fact not. This won't create new states but just adding arrows between states.
However our implmentation includes this, so I left it here.
|
@lance6716 I added crashing and RWLock cases to the model, PTAL and thanks~ |
PutAndVerify/WriteAndVerify.tla
Outdated
| /\ clState' = [ clState EXCEPT ![c] = "committed" ] | ||
| /\ UNCHANGED << clFavor >> | ||
|
|
||
| BeRO(c) == /\ clState[c] = "begin" |
There was a problem hiding this comment.
what's the actual meaning of BeRO? client can generate "empty-ro" in storage but I don't know why it should exist
There was a problem hiding this comment.
BeRO means become a "read-only" node. Then the algorithm become a implementation of RWLock instead of Mutex.
There was a problem hiding this comment.
Generally, there can be many storage slots contains "written-ro" or exactly one storage slot contains "written". (RWLock)
Signed-off-by: Hillium <[email protected]>
Relative PR / Issues:
A draft doc:
https://github.com/pingcap/tidb/blob/dda8f114335d94ce3430aee77e42bd39ec155b63/docs/design/2024-10-11-put-and-verify-transactions-for-external-storages.md