diff --git a/tlaplus/ghostferry_share_safety.cfg b/tlaplus/ghostferry_share_safety.cfg new file mode 100644 index 000000000..1dfafe666 --- /dev/null +++ b/tlaplus/ghostferry_share_safety.cfg @@ -0,0 +1,22 @@ +CONSTANTS + Records = {r1, r2} + TableCapacity = 2 + LockMode = "FOR_UPDATE" + TableIterator = TableIterator + Application = Application + NoRecordHere = NoRecord + +SPECIFICATION Spec + +INVARIANTS + TypeOK + LockSafety + DataConsistency + +PROPERTIES + FinalConsistency + CopyEventuallyCompletes + ModificationProgress + +\* State constraint to prevent state space explosion +CONSTRAINT StateConstraint \ No newline at end of file diff --git a/tlaplus/ghostferry_share_safety.tla b/tlaplus/ghostferry_share_safety.tla new file mode 100644 index 000000000..27a7cd115 --- /dev/null +++ b/tlaplus/ghostferry_share_safety.tla @@ -0,0 +1,178 @@ +----------------------------- MODULE ghostferry_share_safety ----------------------------- +EXTENDS Integers, Sequences, FiniteSets, TLC + +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" + NoRecordHere \* Special value to indicate no record exists + +ASSUME /\ LockMode \in {"FOR_UPDATE", "FOR_SHARE_NOWAIT"} + /\ NoRecordHere \notin Records + +\* Process identifiers +CONSTANTS + TableIterator, \* Process that copies data + Application \* Process that writes data + +PrimaryKeys == 1..TableCapacity +PossibleRecords == Records \cup {NoRecordHere} + +\* Helper operator to check if a process can acquire a lock on a row +CanAcquireLock(row, proc, owners) == + CASE LockMode = "FOR_UPDATE" -> + \* For update: only if no other process holds the lock + owners[row] = {} + [] LockMode = "FOR_SHARE_NOWAIT" -> + \* For share: ok if no writer holds the lock + \/ owners[row] = {} + \/ ~(\E owner \in owners[row]: owner = Application) + +VARIABLES + SourceTable, \* Source database table + TargetTable, \* Target database table + lockOwners, \* Map from row -> set of processes that own the lock + copyComplete, \* Whether TableIterator has finished copying + currentRow, \* Current row being processed by TableIterator + rowToModify, \* Row that Application is trying to modify + newValue \* New value for the row + +vars == << SourceTable, TargetTable, lockOwners, copyComplete, + currentRow, rowToModify, newValue >> + +Init == + /\ SourceTable \in [PrimaryKeys -> PossibleRecords] + /\ TargetTable = [k \in PrimaryKeys |-> NoRecordHere] + /\ lockOwners = [r \in PrimaryKeys |-> {}] + /\ copyComplete = FALSE + /\ currentRow = 1 + /\ rowToModify \in PrimaryKeys + /\ newValue \in Records + +\* TableIterator tries to copy a row +CopyRow == + /\ ~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 >> + +\* TableIterator skips a row when it can't get a lock (FOR_SHARE_NOWAIT) +SkipLockedRow == + /\ ~copyComplete + /\ currentRow <= TableCapacity + /\ LockMode = "FOR_SHARE_NOWAIT" + /\ ~CanAcquireLock(currentRow, TableIterator, lockOwners) + /\ currentRow' = currentRow + 1 + /\ UNCHANGED << SourceTable, TargetTable, lockOwners, copyComplete, rowToModify, newValue >> + +\* TableIterator waits for a row (FOR_UPDATE) +WaitForRow == + /\ ~copyComplete + /\ currentRow <= TableCapacity + /\ LockMode = "FOR_UPDATE" + /\ ~CanAcquireLock(currentRow, TableIterator, lockOwners) + /\ UNCHANGED vars + +\* TableIterator completes copying +CompleteCopy == + /\ ~copyComplete + /\ currentRow > TableCapacity + /\ copyComplete' = TRUE + /\ UNCHANGED << SourceTable, TargetTable, lockOwners, currentRow, rowToModify, newValue >> + +\* Application modifies a row +ModifyRow == + /\ ~copyComplete + /\ CanAcquireLock(rowToModify, Application, lockOwners) + /\ lockOwners' = [lockOwners EXCEPT ![rowToModify] = @ \cup {Application}] + /\ SourceTable' = [SourceTable EXCEPT ![rowToModify] = newValue] + /\ lockOwners' = [lockOwners' EXCEPT ![rowToModify] = @ \ {Application}] + /\ \E r \in PrimaryKeys, v \in Records: + /\ rowToModify' = r + /\ newValue' = v + /\ UNCHANGED << TargetTable, copyComplete, currentRow >> + +\* Application picks a new row to modify +PickNewRow == + /\ ~copyComplete + /\ ~CanAcquireLock(rowToModify, Application, lockOwners) + /\ \E r \in PrimaryKeys, v \in Records: + /\ rowToModify' = r + /\ newValue' = v + /\ UNCHANGED << SourceTable, TargetTable, lockOwners, copyComplete, currentRow >> + +\* System is done when copy is complete +Done == + /\ copyComplete + /\ UNCHANGED vars + +\* Always-enabled action to prevent deadlocks +Stutter == + UNCHANGED vars + +Next == + \/ CopyRow + \/ SkipLockedRow + \/ WaitForRow + \/ CompleteCopy + \/ ModifyRow + \/ PickNewRow + \/ Done + \/ Stutter + +Spec == /\ Init /\ [][Next]_vars + /\ WF_vars(CopyRow) + /\ WF_vars(SkipLockedRow) + /\ WF_vars(CompleteCopy) + /\ WF_vars(ModifyRow) + /\ WF_vars(PickNewRow) + \* No fairness for WaitForRow or Stutter + +\* Safety Properties +TypeOK == + /\ SourceTable \in [PrimaryKeys -> PossibleRecords] + /\ TargetTable \in [PrimaryKeys -> PossibleRecords] + /\ lockOwners \in [PrimaryKeys -> SUBSET {TableIterator, Application}] + /\ currentRow \in 1..(TableCapacity+1) + /\ copyComplete \in BOOLEAN + +LockSafety == + \A row \in PrimaryKeys: + \/ lockOwners[row] = {} \* No locks + \/ /\ LockMode = "FOR_UPDATE" + /\ Cardinality(lockOwners[row]) = 1 \* Exclusive lock + \/ /\ LockMode = "FOR_SHARE_NOWAIT" + /\ ~(\E owner1, owner2 \in lockOwners[row]: \* No writer conflicts + /\ owner1 # owner2 + /\ (owner1 = Application \/ owner2 = Application)) + +DataConsistency == + \A k \in PrimaryKeys: + TargetTable[k] # NoRecordHere => TargetTable[k] = SourceTable[k] + +FinalConsistency == + copyComplete => (\A k \in PrimaryKeys: + SourceTable[k] # NoRecordHere => TargetTable[k] = SourceTable[k]) + +\* Liveness Properties +CopyEventuallyCompletes == + LockMode = "FOR_SHARE_NOWAIT" => <>(copyComplete \/ ENABLED Stutter) + +ModificationProgress == + []<>(\A k \in PrimaryKeys: + \/ copyComplete + \/ CanAcquireLock(k, Application, lockOwners) + \/ ENABLED Stutter) + +\* State Constraints +StateConstraint == + /\ Cardinality(DOMAIN SourceTable) <= TableCapacity + /\ Cardinality(DOMAIN TargetTable) <= TableCapacity + +============================================================================= \ No newline at end of file diff --git a/tlaplus/ghostferry_share_safety.toolbox/GhostferryShareModel.launch b/tlaplus/ghostferry_share_safety.toolbox/GhostferryShareModel.launch new file mode 100644 index 000000000..0540636a8 --- /dev/null +++ b/tlaplus/ghostferry_share_safety.toolbox/GhostferryShareModel.launch @@ -0,0 +1,22 @@ + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file