Added Pluscal version of the key-value store with snapshot isolation,… #84
Conversation
… instantiated clientcentric checking to model check for snapshot isolation properly Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly, modified manifest Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly, modified manifest for a fix Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly, added manifest Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified manifest Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
|
LGTM, @muenchnerkindl are you also going to review? |
| @@ -0,0 +1,185 @@ | |||
| --------------------------- MODULE ClientCentric --------------------------- | |||
| EXTENDS Naturals, TLC, Sequences, FiniteSets, Util | |||
| VARIABLES Keys, Values | |||
There was a problem hiding this comment.
Is it useful to declare these as variable rather than constant parameters? If they were constants, all definitions in this module would be constant level as well, which may avoid trouble further down the line. Also note that the parameters are actually instantiated by constants in module KVsnap.
There was a problem hiding this comment.
ClientCentric is not my module, written by Tim, so I am reluctant to make any change there.
There was a problem hiding this comment.
The module is instantiated as seen in: https://github.com/tlaplus/Examples/pull/84/files/adb3d2aa3f62812a2becd5c2f6700d69eb1c5134#diff-ccf178cee4a4265b5f8405a78d596e79973a841e20119a281c19775a1ecae139R14
CC == INSTANCE ClientCentric WITH Keys <- Key, Values <- TxId \union {NoVal}
If something similar is possible with constant parameters, and it is more idiomatic TLA, you should definitely go for constant parameters.
FYI I have no issues in changing/updating the code in any way. Glad that your are using it and/or inspired by my work. :)
There was a problem hiding this comment.
Instantiation is certainly possible for constant as well as variable parameters. Declaring Keys and Values to be variables allows these sets to change during an execution, which might be interesting for some applications, but I don't know what the original paper had in mind. If they are constants, the module is a constant module (since all operator definitions are of constant level as well), which allows operators to be instantiated at constant, variable or action level. Potential complications with non-constant modules are described in section 17.8 of Specifying Systems. However, my comment was just a caveat for later, there is nothing wrong with the modules as they are written, and they are accepted by TLC.
| LET setOfAllReadStatesOfOperation(transactionOperations) == | ||
| { ReadStates(execution, operation, transaction) : operation \in SeqToSet(transactionOperations) } | ||
| \* also include all states for when the transaction contains no operations | ||
| readStatesForEmptyTransaction == { s \in SeqToSet(executionStates(execution)) : beforeOrEqualInExecution(execution, s, parentState(execution, transaction)) } |
There was a problem hiding this comment.
I don't see how this definition (or its use) is restricted to the case "when the transaction contains no operation"? Perhaps rephrase the comment?
There was a problem hiding this comment.
ClientCentric is not my module, written by Tim, so I am reluctant to make any change there.
There was a problem hiding this comment.
If I remember correctly, this is where I deviated from the original definitions in the paper by Crooks (https://www.cs.cornell.edu/lorenzo/papers/Crooks17Seeing.pdf). The comment is mainly there to upgrade the definition to also allow transactions with an empty operation set, while still satisfying the isolation level.
I personally used when incrementally model checking isolation levels of the Two-Phase Locking and Local-Coordination Avoidance protocols, which contained empty transactions when initializing.
The comment could for example be rephrased to:
"readStatesForEmptyTransaction contains all previous states, in order to make sure that empty transactions do not incorrectly invalidate the checked isolation level."
There was a problem hiding this comment.
Has this conversation been resolved? If yes, it looks like this PR is ready to be merged.
There was a problem hiding this comment.
I certainly have no objection to merging the PR, although I don't think that the wording of the comment has been changed (Tim's suggestion clarifies the intent of the definition IMHO).
There was a problem hiding this comment.
@muratdem can you do the finishing touches (wording of this comment + removal [] copy/paste artifact), and the we merge it?
There was a problem hiding this comment.
yes, I will also pull some global variables to be process local.
… instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
|
I don't understand why the download TLA+ dependencies step in CI is failing.
|
|
The failures do not appear to be related to your spec: the Linux issue is a failure to build TLAPS (an issue that pops up occasionally, we don't really understand why), the MacOS build fails to what appears to be a version issue with the tree sitter grammar, which I have never seen before. Hopefully @lemmy and/or @ahelwer will be able to comment. |
|
Yeah this is a pretty weird error on macOS. Looking into it now. |
|
Both of these issues are unfortunately transient. Tracked in following issues:
Re-running the workflow should fix them. I have a PR here which will print out tool version information that at least might help figure out why this is happening next time: #88 |
|
Really cool to see that you are adding examples based on my earlier work. :) |
… instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest, improved the model, and handled CR comments Signed-off-by: Murat Demirbas <mudemirb@amazon.com>
… instantiated clientcentric checking to model check for snapshot isolation properly