Added Pluscal version of the key-value store with snapshot isolation,…

… instantiated clientcentric checking to model check for snapshot isolation properly

specifications/KeyValueStore/ClientCentric.tla

@@ -0,0 +1,185 @@
+--------------------------- MODULE ClientCentric ---------------------------
+EXTENDS Naturals, TLC, Sequences, FiniteSets, Util
+VARIABLES Keys, Values
+\* TODO InitValue could be bottom (_|_)
+
+\* TLA+ specifications of Client Centric Isolation Specification by Crooks et al: https://dl.acm.org/doi/10.1145/3087801.3087802
+\* TLA+ specifications by Tim Soethout ([email protected])
+
+\* A database `State` is represented by keys with corresponding values
+State == [Keys -> Values]
+
+\* An `Operation` is a read or write of a key and value
+Operation == [op: {"read", "write"}, key: Keys, value: Values]
+
+\* Helpers representing Reads and Writes
+r(k,v) == [op |-> "read",  key |-> k, value |-> v]
+w(k,v) == [op |-> "write", key |-> k, value |-> v]
+
+\* A `Transaction` is a total order of `Operation`s
+\* Transaction == [ops: Seq(Operation), start: TimeStamp, commit: TimeStamp]
+Transaction == Seq(Operation)
+\* For simplicity we store start and commit in a lookup function
+TimeStamp == Nat
+TransactionTimes == [t \in Transaction |-> [start: TimeStamp, commit: TimeStamp]]
+
+\* "An execution e for a set of transactions
+\* T is a totally ordered set defined by the pair (Se,−−t \in T−→),
+\* where Se is the set of states generated by applying, 
+\* starting from the system’s initial state, a permutation of all the transactions in T ."
+ExecutionElem == [parentState: State, transaction: Transaction]
+\* resultState is the parentState of the next transaction, but not used in the isolation definitions.
+\* ExecutionElem == [parentState: State, transaction: Transaction, resultState: State]
+\* We represent an `Execution` as a sequence of `Transaction`s with their corresponding parent state.
+\* Note: This execution does therefor not contain the "final state" of the execution, since it is not a parent state of a transaction.
+Execution == Seq(ExecutionElem)
+
+\* Seq
+executionStates(execution) == [ i \in 1..Len(execution) |-> execution[i].parentState ]
+\* Set
+executionTransactions(execution) == { ep.transaction : ep \in SeqToSet(execution) }
+
+\* "The parent state is the last state in the execution
+\* Definition 1: s -T-> s' ≡ [(k,v) ∈ s ∧ (k,v)􏰍 \notin s'] => k ∈ W_T /\ w(k,v) ∈ Σ_T => (k,v) ∈ s.
+\* We refer to s as the parent state of T (denoted as sp,T ); to the
+\* transaction that generated s as Ts ; and to the set of keys in which
+\* s and s′ differ as ∆(s,s′)"
+parentState(execution, transaction) == 
+  LET ind == CHOOSE i \in 1..Len(execution): execution[i].transaction = transaction
+  IN execution[ind].parentState
+
+\* w(k,v) -to-> r(k,v)
+\* check reads and writes, implicit because of "write" check in ReadStates
+earlierInTransaction(transaction, op1, op2) == Index(transaction, op1) < Index(transaction, op2)
+
+\* state1 -*-> state2
+beforeOrEqualInExecution(execution, state1, state2) == 
+  LET states == executionStates(execution)
+  IN  Index(states, state1) <= Index(states, state2)
+
+\* Read states: from which states can the operation read it's value
+ReadStates(execution, operation, transaction) == 
+  LET Se == SeqToSet(executionStates(execution))
+      sp == parentState(execution, transaction)
+  IN { s \in Se:
+        /\ beforeOrEqualInExecution(execution, s, sp) \* s -*-> s_p: restrict the valid read states for the operations in T to be no later than sp
+        /\ \/ s[operation.key] = operation.value \* (k,v) \in s
+           \/ \E write \in SeqToSet(transaction): 
+              /\ write.op = "write" /\ write.key = operation.key /\ write.value = operation.value
+              /\ earlierInTransaction(transaction, write, operation) \* w(k,v)-to->r(k,v)
+\* "By convention, write operations have read states too: for a write operation in T , they include all states in Se up to and including T ’s parent state."
+           \/ operation.op = "write"
+     }
+
+Preread(execution, transaction) ==
+  \A operation \in SeqToSet(transaction): ReadStates(execution, operation, transaction) /= {}
+
+PrereadAll(execution, transactions) == 
+  \A transaction \in transactions: Preread(execution, transaction)
+
+\* A state `s` is complete for `T` in `e` if every operation in `T` can read from `s`
+Complete(execution, transaction, state) == 
+  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)) }
+  IN state \in INTERSECTION(setOfAllReadStatesOfOperation(transaction) \union { readStatesForEmptyTransaction } )
+
+\* "the write set of T comprises the keys that T updates: WT = {k|w(k, v) ∈ ΣT }.
+\* For simplicity of exposition, we assume that a transaction only writes a key once."
+WriteSet(transaction) == 
+  LET writes == { operation \in SeqToSet(transaction) : operation.op = "write" } 
+  IN { operation.key : operation \in writes } 
+\* "Denoting the set of keys in which s and s′ differ as ∆(s, s′), we express this as NO-CONF_T (s) ≡ ∆(s, sp) ∩ WT = ∅"
+NoConf(execution, transaction, state) == 
+  LET Sp == parentState(execution, transaction)
+      delta == { key \in DOMAIN Sp : Sp[key] /= state[key] }
+  IN delta \intersect WriteSet(transaction) = {}
+
+\* `t1` comes before `t2` in wall clock/oracle time
+ComesStrictBefore(t1, t2, timestamps) == timestamps[t1].commit < timestamps[t2].start
+
+\* Given system state and single transaction (seq of operations), determines new state
+effects(state, transaction) == 
+       ReduceSeq(LAMBDA o, newState: IF o.op = "write" THEN [newState EXCEPT ![o.key] = o.value] ELSE newState, transaction, state)
+
+\* Lists all possible permutations of executions given set of transactions
+executions(initialState, transactions) == 
+  \* All possible permutations
+  LET orderings == PermSeqs(transactions)
+\*      initialState == [k \in Keys |-> InitValue] \* makes it level-1 therefor pass it in
+      accummulator == [ execution |-> <<>>, nextState |-> initialState ]
+  IN { LET executionAcc == ReduceSeq(
+         \*                                store ExecutionElem in accumulator
+                            LAMBDA t, acc: [ execution |-> Append(acc.execution, [parentState |-> acc.nextState, transaction |-> t])
+  \*                                         calcultate next state
+                                           , nextState |-> effects(acc.nextState,t) 
+                            ],
+                            ordering, accummulator)
+\*              recover ExecutionElems
+       IN executionAcc.execution
+     : ordering \in orderings }
+
+\* Helper: checks if specific execution satisfies given commit test
+executionSatisfiesCT(execution, commitTest(_,_)) ==
+  LET transactions == executionTransactions(execution)
+  IN \A transaction \in transactions: commitTest(transaction, execution)
+
+\* tests there exists an execution for `transactions`, that satisfies the isolation level given by `commitTest`
+\* "Definition 5 Given a set of transactions T and their read states, 
+\* a storagesystem satisfies an isolation level I iff ∃e:∀t ∈ T :CTI(t,e)."
+satisfyIsolationLevel(initialState, transactions, commitTest(_,_)) ==
+  \E execution \in executions(initialState, transactions): \A transaction \in transactions:
+    \* PrintT(<<"try execution:",execution>>) =>
+    commitTest(transaction, execution)
+
+\* Serializability commit test
+CT_SER(transaction, execution) ==
+  Complete(execution, transaction, parentState(execution, transaction))
+Serializability(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_SER)
+
+\*SerializabilityDebug(initialState, transactions) == 
+\*  \* if no executions satify commit test, print all executions
+\*  \/ (~\E execution \in executions(initialState, transactions): \A transaction \in transactions:
+\*       CT_SER(transaction, execution)) => \A execution \in executions(initialState, transactions): PrintT(<<"Execution not Serializable:",execution>>)
+\*  \* fall back to normal check
+\*  \/ \E execution \in executions(initialState, transactions): \A transaction \in transactions: CT_SER(transaction, execution)
+
+SerializabilityDebug(initialState, transactions) == 
+  ~ Serializability(initialState, transactions) => Print(<<"Executions not Serializable:",  executions(initialState, transactions)>>, FALSE)
+
+\* Snapshot Isolation
+CT_SI(transaction, execution) == \E state \in SeqToSet(executionStates(execution)):
+  Complete(execution, transaction, state) /\ NoConf(execution, transaction, state)
+SnapshotIsolation(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_SI)
+
+\* Strict Serializability: ∀T ∈T:T <s T => s_T′ -*-> s_T.
+CT_SSER(timestamps, transaction, execution) ==
+  LET Sp == parentState(execution, transaction)
+  IN /\ Complete(execution, transaction, Sp)
+     /\ \A otherTransaction \in executionTransactions(execution): 
+        ComesStrictBefore(otherTransaction, transaction, timestamps) => 
+          beforeOrEqualInExecution(execution, parentState(execution, otherTransaction), Sp)
+\* For now inline `satisfyIsolationLevel` instead of `satisfyIsolationLevel(transactions, CT_SSER(timestamps)) because partial functions are not supported/hard`
+StrictSerializability(initialState, transactions, timestamps) ==
+  \E execution \in executions(initialState, transactions): \A transaction \in transactions: CT_SSER(timestamps, transaction, execution)
+
+\* Read Committed
+CT_RC(transaction, execution) == Preread(execution, transaction)
+ReadCommitted(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_RC)
+
+\* Read Uncommitted
+CT_RU(transaction, execution) == TRUE
+ReadUncommitted(initialState, transactions) == satisfyIsolationLevel(initialState, transactions, CT_RU)
+
+\* Check types in derived specification
+TypeOKT(transactions) ==
+\*  /\ InitValue \in Values
+  /\ transactions \subseteq Transaction
+
+TypeOK(transactions, execution) == 
+  /\ TypeOKT(transactions)
+\*  /\ PrintT(State)
+  /\ execution \in Execution
+
+=============================================================================

specifications/KeyValueStore/KVsnap.tla

@@ -0,0 +1,204 @@
+--------------------------- MODULE KVsnap ---------------------------------
+(**************************************************************************)
+(* Pluscal algoritm for a simple key-value store with snapshot isolation  *)
+(* This version has atomic updates of store and missed sets of txns       *)
+(**************************************************************************)
+EXTENDS Integers, Sequences, FiniteSets, TLC, Util
+
+CONSTANTS   Key,            \* The set of all keys.
+            TxId,           \* The set of all transaction IDs.
+            NoVal           \* NoVal, which all keys are initialized with.
+
+\* Instantiating ClientCentric enables us to check transaction isolation guarantees this model satisfies
+\* https://muratbuffalo.blogspot.com/2022/07/automated-validation-of-state-based.html         
+CC == INSTANCE ClientCentric WITH Keys <- Key, Values <- TxId \union {NoVal}          
+
+wOp(k,v) == CC!w(k,v)
+rOp(k,v) == CC!r(k,v)
+
+(* --algorithm KVsnap {
+
+variables 
+    \* A data store mapping keys to values
+    store = [k \in Key |-> NoVal],
+
+    \* The set of open snapshot transactions
+    tx = {},
+
+    \* Snapshots of the store for each transaction
+    snapshotStore = [t \in TxId |-> [k \in Key |-> NoVal]],
+
+    \* A log of writes performed within each transaction 
+    written = [t \in TxId |-> {}],
+
+    \* The set of writes invisible to each transaction
+    missed = [t \in TxId |-> {}],
+
+    \*  reads/writes per txn_id, used for interfacing to CC
+    ops = [ tId \in TxId |-> <<>> ];     
+
+define {
+    \* for instantiating the ClientCentric module
+    InitialState == [k \in Key |-> NoVal]   
+    IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b   
+    SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
+
+    \* snapshot isolation invariant
+    SnapshotIsolation == CC!SnapshotIsolation(InitialState, Range(ops))
+
+\*    Serialization == CC!Serializability(InitialState, Range(ops))
+
+    TypeOK == \* type invariant
+        /\ store \in [Key -> TxId \union {NoVal}]
+        /\ tx \subseteq TxId
+        /\ snapshotStore \in [TxId -> [Key -> TxId \union {NoVal}]]
+        /\ written \in [TxId -> SUBSET Key]
+        /\ missed \in [TxId -> SUBSET Key] 
+}
+
+
+\* Transaction processing
+fair process (t \in TxId)
+variables
+    read_keys={},    \* read keys for the transaction
+    write_keys={};   \* write keys for the transaction    
+{
+START: \* Start the transaction
+    tx := tx \union {self};
+    snapshotStore[self] := store; \* take my snapshot of store
+
+    with (rk \in SUBSET Key; wk \in SUBSET Key \ {}) {
+        read_keys := rk;     \* select a random read-key-set  from possible read-keys
+        write_keys := wk;    \* select a random write-key-set from possible write-keys  
+    };
+
+
+READ: \* Process reads on my snapshot          
+    \* log reads for CC isolation check 
+    ops[self] := ops[self] \o SetToSeq({rOp(k, snapshotStore[self][k]): k \in read_keys}); 
+
+UPDATE: \* Process writes on my snapshot, write 'self' as value
+    snapshotStore[self] := [k \in Key |-> IF k \in write_keys THEN self ELSE snapshotStore[self][k] ];    
+    written[self] := write_keys;
+
+COMMIT: \* Commit the transaction to the database if there is no conflict   
+    if (missed[self] \intersect written[self] = {}) { 
+        \* take self off of active txn set
+        tx := tx \ {self}; 
+
+        \* Update the missed writes for other open transactions (nonlocal update!)
+        missed := [o \in TxId |-> IF o \in tx THEN missed[o] \union written[self] ELSE missed[o]];
+
+        \* update store
+        store := [k \in Key |-> IF k \in written[self] THEN snapshotStore[self][k] ELSE store[k] ];  
+
+        \* log reads for CC isolation check 
+        ops[self] := ops[self] \o SetToSeq({wOp(k, self): k \in written[self]}); 
+    }
+}
+
+
+}
+*)
+
+\* BEGIN TRANSLATION (chksum(pcal) = "38698f36" /\ chksum(tla) = "2d9d1e7d")
+VARIABLES store, tx, snapshotStore, written, missed, ops, pc
+
+(* define statement *)
+InitialState == [k \in Key |-> NoVal]
+IsInjective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b
+SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
+
+
+SnapshotIsolation == CC!SnapshotIsolation(InitialState, Range(ops))
+
+
+
+TypeOK ==
+    /\ store \in [Key -> TxId \union {NoVal}]
+    /\ tx \subseteq TxId
+    /\ snapshotStore \in [TxId -> [Key -> TxId \union {NoVal}]]
+    /\ written \in [TxId -> SUBSET Key]
+    /\ missed \in [TxId -> SUBSET Key]
+
+VARIABLES read_keys, write_keys
+
+vars == << store, tx, snapshotStore, written, missed, ops, pc, read_keys, 
+           write_keys >>
+
+ProcSet == (TxId)
+
+Init == (* Global variables *)
+        /\ store = [k \in Key |-> NoVal]
+        /\ tx = {}
+        /\ snapshotStore = [t \in TxId |-> [k \in Key |-> NoVal]]
+        /\ written = [t \in TxId |-> {}]
+        /\ missed = [t \in TxId |-> {}]
+        /\ ops = [ tId \in TxId |-> <<>> ]
+        (* Process t *)
+        /\ read_keys = [self \in TxId |-> {}]
+        /\ write_keys = [self \in TxId |-> {}]
+        /\ pc = [self \in ProcSet |-> "START"]
+
+START(self) == /\ pc[self] = "START"
+               /\ tx' = (tx \union {self})
+               /\ snapshotStore' = [snapshotStore EXCEPT ![self] = store]
+               /\ \E rk \in SUBSET Key:
+                    \E wk \in SUBSET Key \ {}:
+                      /\ read_keys' = [read_keys EXCEPT ![self] = rk]
+                      /\ write_keys' = [write_keys EXCEPT ![self] = wk]
+               /\ pc' = [pc EXCEPT ![self] = "READ"]
+               /\ UNCHANGED << store, written, missed, ops >>
+
+READ(self) == /\ pc[self] = "READ"
+              /\ ops' = [ops EXCEPT ![self] = ops[self] \o SetToSeq({rOp(k, snapshotStore[self][k]): k \in read_keys[self]})]
+              /\ pc' = [pc EXCEPT ![self] = "UPDATE"]
+              /\ UNCHANGED << store, tx, snapshotStore, written, missed, 
+                              read_keys, write_keys >>
+
+UPDATE(self) == /\ pc[self] = "UPDATE"
+                /\ snapshotStore' = [snapshotStore EXCEPT ![self] = [k \in Key |-> IF k \in write_keys[self] THEN self ELSE snapshotStore[self][k] ]]
+                /\ written' = [written EXCEPT ![self] = write_keys[self]]
+                /\ pc' = [pc EXCEPT ![self] = "COMMIT"]
+                /\ UNCHANGED << store, tx, missed, ops, read_keys, write_keys >>
+
+COMMIT(self) == /\ pc[self] = "COMMIT"
+                /\ IF missed[self] \intersect written[self] = {}
+                      THEN /\ tx' = tx \ {self}
+                           /\ missed' = [o \in TxId |-> IF o \in tx' THEN missed[o] \union written[self] ELSE missed[o]]
+                           /\ store' = [k \in Key |-> IF k \in written[self] THEN snapshotStore[self][k] ELSE store[k] ]
+                           /\ ops' = [ops EXCEPT ![self] = ops[self] \o SetToSeq({wOp(k, self): k \in written[self]})]
+                      ELSE /\ TRUE
+                           /\ UNCHANGED << store, tx, missed, ops >>
+                /\ pc' = [pc EXCEPT ![self] = "Done"]
+                /\ UNCHANGED << snapshotStore, written, read_keys, write_keys >>
+
+t(self) == START(self) \/ READ(self) \/ UPDATE(self) \/ COMMIT(self)
+
+(* Allow infinite stuttering to prevent deadlock on termination. *)
+Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
+               /\ UNCHANGED vars
+
+Next == (\E self \in TxId: t(self))
+           \/ Terminating
+
+Spec == /\ Init /\ [][Next]_vars
+        /\ \A self \in TxId : WF_vars(t(self))
+
+Termination == <>(\A self \in ProcSet: pc[self] = "Done")
+
+\* END TRANSLATION 
+
+
+===========================================================================
+nonatomic version would be as follows. It would be interesting to model check this with nanatomic version, with more yield points with labels to see where we need the latches.  
+
+    \* while (write_keys #{}){
+    \*     \* all values being distinct works best for checking, so use self??
+    \*     with (k \in write_keys) {
+    \*         snapshotStore[self][k] := self;
+    \*         written[self] := written[self] \union {k};
+    \*     } 
+    \* };
+
+