Skip to content

Improvements to tlaplus/ghostferry_share_safety.tla #385

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

Draft
wants to merge 1 commit into
base: verify_share_nowait_with_tla+
Choose a base branch
from
Draft

Improvements to tlaplus/ghostferry_share_safety.tla #385

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions tlaplus/ghostferry_share_safety.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CONSTANTS
Records = {r1, r2}
TableCapacity = 2
LockMode = "FOR_UPDATE"
LockMode = "FOR_SHARE_NOWAIT"
TableIterator = TableIterator
Application = Application
NoRecordHere = NoRecord
Expand All @@ -19,4 +19,4 @@ PROPERTIES
ModificationProgress

\* State constraint to prevent state space explosion
CONSTRAINT StateConstraint
CONSTRAINT StateConstraint
76 changes: 46 additions & 30 deletions tlaplus/ghostferry_share_safety.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
----------------------------- MODULE ghostferry_share_safety -----------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
CONSTANTS
Records, \* Set of possible records that can be in the database
TableCapacity, \* Maximum size of the table
LockMode, \* Either "FOR_UPDATE" or "FOR_SHARE_NOWAIT"
Expand All @@ -11,7 +11,7 @@ ASSUME /\ LockMode \in {"FOR_UPDATE", "FOR_SHARE_NOWAIT"}
/\ NoRecordHere \notin Records

\* Process identifiers
CONSTANTS
CONSTANTS
TableIterator, \* Process that copies data
Application \* Process that writes data

Expand All @@ -28,7 +28,7 @@ CanAcquireLock(row, proc, owners) ==
\/ owners[row] = {}
\/ ~(\E owner \in owners[row]: owner = Application)

VARIABLES
VARIABLES
SourceTable, \* Source database table
TargetTable, \* Target database table
lockOwners, \* Map from row -> set of processes that own the lock
Expand All @@ -37,10 +37,10 @@ VARIABLES
rowToModify, \* Row that Application is trying to modify
newValue \* New value for the row

vars == << SourceTable, TargetTable, lockOwners, copyComplete,
vars == << SourceTable, TargetTable, lockOwners, copyComplete,
currentRow, rowToModify, newValue >>

Init ==
Init ==
/\ SourceTable \in [PrimaryKeys -> PossibleRecords]
/\ TargetTable = [k \in PrimaryKeys |-> NoRecordHere]
/\ lockOwners = [r \in PrimaryKeys |-> {}]
Expand All @@ -50,26 +50,31 @@ Init ==
/\ newValue \in Records

\* TableIterator tries to copy a row
CopyRow ==
LockRowToCopy ==
/\ ~copyComplete
/\ currentRow <= TableCapacity
/\ CanAcquireLock(currentRow, TableIterator, lockOwners)
/\ lockOwners' = [lockOwners EXCEPT ![currentRow] = @ \cup {TableIterator}]
/\ IF SourceTable[currentRow] # NoRecordHere
THEN TargetTable' = [TargetTable EXCEPT ![currentRow] = SourceTable[currentRow]]
ELSE UNCHANGED TargetTable
/\ lockOwners' = [lockOwners' EXCEPT ![currentRow] = @ \ {TableIterator}]
/\ currentRow' = currentRow + 1
/\ UNCHANGED << SourceTable, copyComplete, rowToModify, newValue >>
/\ UNCHANGED << SourceTable, TargetTable, copyComplete, currentRow, rowToModify, newValue >>

\* TableIterator skips a row when it can't get a lock (FOR_SHARE_NOWAIT)
SkipLockedRow ==
\* TableIterator errors on a cursor batch when it can't get a lock on any row (FOR_SHARE_NOWAIT)
FailOnLockedRow ==
/\ ~copyComplete
/\ currentRow <= TableCapacity
/\ LockMode = "FOR_SHARE_NOWAIT"
/\ ~CanAcquireLock(currentRow, TableIterator, lockOwners)
/\ UNCHANGED << SourceTable, TargetTable, lockOwners, currentRow, copyComplete, rowToModify, newValue >>

\* TableIterator tries copies
CopyRow ==
/\ ~copyComplete
/\ currentRow <= TableCapacity
/\ lockOwners' = [lockOwners EXCEPT ![currentRow] = @ \ {TableIterator}]
/\ IF SourceTable[currentRow] # NoRecordHere
THEN TargetTable' = [TargetTable EXCEPT ![currentRow] = SourceTable[currentRow]]
ELSE UNCHANGED TargetTable
/\ currentRow' = currentRow + 1
/\ UNCHANGED << SourceTable, TargetTable, lockOwners, copyComplete, rowToModify, newValue >>
/\ UNCHANGED << SourceTable, copyComplete, rowToModify, newValue >>

\* TableIterator waits for a row (FOR_UPDATE)
WaitForRow ==
Expand All @@ -87,12 +92,19 @@ CompleteCopy ==
/\ UNCHANGED << SourceTable, TargetTable, lockOwners, currentRow, rowToModify, newValue >>

\* Application modifies a row
ModifyRow ==
LockRowToModify ==
/\ ~copyComplete
/\ CanAcquireLock(rowToModify, Application, lockOwners)
/\ lockOwners[rowToModify] = {} \* No locks on the row (in any mode, it's a FOR UPDATE by Application)
/\ lockOwners' = [lockOwners EXCEPT ![rowToModify] = @ \cup {Application}]
/\ UNCHANGED << SourceTable, TargetTable, copyComplete, rowToModify, currentRow, newValue >>

ModifyRow ==
/\ ~copyComplete
/\ SourceTable' = [SourceTable EXCEPT ![rowToModify] = newValue]
/\ lockOwners' = [lockOwners' EXCEPT ![rowToModify] = @ \ {Application}]
/\ IF TargetTable[rowToModify] # NoRecordHere \* Simulate a streaming-like update to TargetTable too, if row exists
THEN TargetTable' = [TargetTable EXCEPT ![rowToModify] = newValue]
ELSE UNCHANGED TargetTable
/\ lockOwners' = [lockOwners EXCEPT ![rowToModify] = @ \ {Application}]
/\ \E r \in PrimaryKeys, v \in Records:
/\ rowToModify' = r
/\ newValue' = v
Expand All @@ -116,20 +128,24 @@ Done ==
Stutter ==
UNCHANGED vars

Next ==
\/ CopyRow
\/ SkipLockedRow
Next ==
\/ LockRowToCopy
\/ CopyRow
\/ FailOnLockedRow
\/ WaitForRow
\/ CompleteCopy
\/ ModifyRow
\/ PickNewRow
\/ CompleteCopy
\/ LockRowToModify
\/ ModifyRow
\/ PickNewRow
\/ Done
\/ Stutter

Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(LockRowToCopy)
/\ WF_vars(CopyRow)
/\ WF_vars(SkipLockedRow)
/\ WF_vars(FailOnLockedRow)
/\ WF_vars(CompleteCopy)
/\ WF_vars(LockRowToModify)
/\ WF_vars(ModifyRow)
/\ WF_vars(PickNewRow)
\* No fairness for WaitForRow or Stutter
Expand All @@ -145,7 +161,7 @@ TypeOK ==
LockSafety ==
\A row \in PrimaryKeys:
\/ lockOwners[row] = {} \* No locks
\/ /\ LockMode = "FOR_UPDATE"
\/ /\ LockMode = "FOR_UPDATE"
/\ Cardinality(lockOwners[row]) = 1 \* Exclusive lock
\/ /\ LockMode = "FOR_SHARE_NOWAIT"
/\ ~(\E owner1, owner2 \in lockOwners[row]: \* No writer conflicts
Expand All @@ -157,21 +173,21 @@ DataConsistency ==
TargetTable[k] # NoRecordHere => TargetTable[k] = SourceTable[k]

FinalConsistency ==
copyComplete => (\A k \in PrimaryKeys:
copyComplete => (\A k \in PrimaryKeys:
SourceTable[k] # NoRecordHere => TargetTable[k] = SourceTable[k])

\* Liveness Properties
CopyEventuallyCompletes ==
CopyEventuallyCompletes ==
LockMode = "FOR_SHARE_NOWAIT" => <>(copyComplete \/ ENABLED Stutter)

ModificationProgress ==
[]<>(\A k \in PrimaryKeys:
[]<>(\A k \in PrimaryKeys:
\/ copyComplete
\/ CanAcquireLock(k, Application, lockOwners)
\/ ENABLED Stutter)

\* State Constraints
StateConstraint ==
StateConstraint ==
/\ Cardinality(DOMAIN SourceTable) <= TableCapacity
/\ Cardinality(DOMAIN TargetTable) <= TableCapacity

Expand Down
Loading