Skip to content
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.

Sign up for GitHub

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

Make meaning of AcquirableSessionTokens clearer #6

Merged
merged 2 commits into from
Dec 14, 2023
Merged

Make meaning of AcquirableSessionTokens clearer #6

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
05115fd
Make meaning of AcquirableSessionTokens clearer
fhackett Dec 13, 2023
aa69c51
Improve phrasing of CosmosDB.tla comments
fhackett Dec 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions simple-model/CosmosDB.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,10 @@ SessionTokens == [
epoch: Epochs
]

\* The "not a session token" session token.
\* The "not a session token" session token. It precedes all session tokens,
\* and should be used when no session token is known / available.
\* It is not a valid session token itself, but is usually compatible with them.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"usually"? Perhaps add, under what condition it is incompatible?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I believe always, but I was being vague as a reflex because there may be some edge case (which would be a bug) where that isn't true. I'll just delete the word.

\*
\* It is not a member of SessionTokens because it has an epoch of 0,
\* which is special-cased such that it is valid at all epochs.
\* A read or write operation can be given this token, and that
Expand Down Expand Up @@ -194,13 +197,17 @@ TypesOK ==
/\ epoch \in Epochs
/\ WriteConsistencyLevel \in ConsistencyLevels

\* This operator can be used to generate a
\* fresh session token. Combined with session-consistent reads and writes,
\* the expectation is that one could model a client holding and progressively
\* updating a session token using this operator and the ones defined near it.
\* Assuming session-consistent reads and writes,
\* this operator describes the set of all session tokens that could be
\* acquired during the current action.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

AcquirableSessionTokens is a state-level formula? Should "during the current action" be replaced with "in the current state"? Nitpicking: AcquirableSessionTokens also describes the set of all session independently of session-consistent reads and writes.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Makes sense I think - I edited that a little bit to account for both things as I understand them.

\*
\* Note that the range of possible checkpoints is very broad: if the newest
\* write to a key is very old, the current spec will consider the returned
\* token's checkpoint to point to that oldest index, even if
\* the checkpoint is older than readIndex.
AcquirableSessionTokens == [
epoch: {epoch},
checkpoint: readIndex..Len(log)
checkpoint: 0..(Len(log) + 1) \* +1 to account for incomplete writes
]

\* Whether the database's current state accepts writes.
Expand Down
13 changes: 13 additions & 0 deletions simple-model/CosmosDBProps.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,6 +433,19 @@ SessionTokenWhenValid ==
/\ token.epoch = epoch \/ token = NoSessionToken
=> SessionConsistencyRead(token, key) # {}

SessionTokenAlwaysAcquirableRead ==
ReadConsistencyOK(SessionConsistency)
=>
\A key \in Keys :
{ UpdateTokenFromRead(NoSessionToken, read)
: read \in SessionConsistencyRead(NoSessionToken, key) }
\subseteq AcquirableSessionTokens

SessionTokenAlwaysAcquirableWrite ==
WriteConsistencyLevel = SessionConsistency
=>
WriteInitToken \in AcquirableSessionTokens

\* ConsistentPrefix
\* https://docs.microsoft.com/en-us/azure/cosmos-db/consistency-levels#consistent-prefix-consistency
\* Note: consistent prefix does not seem to be observable
Expand Down
3 changes: 3 additions & 0 deletions simple-model/MCCosmosDBProps.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,9 @@ INVARIANT
BoundedStalenessReadsFollowReadIndex
BoundedStalenessIsBounded

SessionTokenAlwaysAcquirableRead
SessionTokenAlwaysAcquirableWrite

\* very slow:
SessionConsistencyReadsMonotonicPerTokenSequence
SessionConsistencyReadsFollowReadIndex
Expand Down
2 changes: 1 addition & 1 deletion simple-model/MCCosmosDBProps.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ CheckpointsImpl == LogIndicesImpl \cup {0}
EpochsImpl == 1..3

SpecificStateSpace ==
/\ Len(log) < Max(LogIndicesImpl)
/\ Len(log) < (Max(LogIndicesImpl) - 1)
/\ epoch < Max(EpochsImpl)

StalenessBoundImpl == 2
Expand Down
Loading