-
Notifications
You must be signed in to change notification settings - Fork 205
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
WIP: New definition of TxID ordered speculative linearizability #6185
base: main
Are you sure you want to change the base?
Conversation
|
||
\* Ordering over txIDs, the form of which is <<view,seqnum>> | ||
TxIDStrictlyLessThan(x, y) == | ||
\/ x[1] < y[1] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A less invasive refactoring than the introduction of records would be the addition of two definitions such as View==1
and SeqNum==2
to be able to write x[View] < y[View] ...
.
\* guarantee provided by CCF. Note that this invariant is stronger than traditional linearizability. | ||
\* TxID ordered speculative linearizability means that once a rw transaction is committed, it is linearizable | ||
\* and that the ordering of execution is consistent with the order of transaction IDs. | ||
\* In CCF, a client receives a response before it learns that the transaction is committed, the speculative |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If this sentence is grammatically correct, I find it very hard to read.
\* Note that this invariant is only considers committed read-write transactions. | ||
CommittedRwOrderedSerializableInv == | ||
\/ Len(CommittedRwResponses) < 2 | ||
\/ \A i \in 1..Len(CommittedRwResponses)-1: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The first disjunct is redundant because \A i \in 1..0: P
is true.
|
||
\* If a transaction response is received (event i) before another transaction is requested (event j), | ||
\* then tx_id of the first transaction is strictly less than the tx_id of the second transaction. | ||
\* Note that this invariant is only considers committed read-write transactions. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Superfluous "is".
\/ /\ x[1] = y[1] | ||
/\ x[2] < y[2] | ||
|
||
\* CommittedRwResponseSorted is a subset of history containing only the responses to committed rx transactions |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
- Dangling "Sorted" in "CommittedRwResponseSorted"?
- "subsequence" instead of "subset"
WIP, opened for CI