From 245ef9f418d0fb221da09724abcef21504a46698 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Thu, 3 Aug 2023 15:47:04 -0400 Subject: [PATCH 1/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly Signed-off-by: Murat Demirbas --- .../KeyValueStore/ClientCentric.tla | 185 ++++++++++++++++ specifications/KeyValueStore/KVsnap.tla | 204 ++++++++++++++++++ specifications/KeyValueStore/MCKVsnap.cfg | 18 ++ specifications/KeyValueStore/MCKVsnap.tla | 5 + specifications/KeyValueStore/README.md | 16 ++ specifications/KeyValueStore/Util.tla | 49 +++++ 6 files changed, 477 insertions(+) create mode 100644 specifications/KeyValueStore/ClientCentric.tla create mode 100644 specifications/KeyValueStore/KVsnap.tla create mode 100644 specifications/KeyValueStore/MCKVsnap.cfg create mode 100644 specifications/KeyValueStore/MCKVsnap.tla create mode 100644 specifications/KeyValueStore/README.md create mode 100644 specifications/KeyValueStore/Util.tla diff --git a/specifications/KeyValueStore/ClientCentric.tla b/specifications/KeyValueStore/ClientCentric.tla new file mode 100644 index 00000000..39543aa2 --- /dev/null +++ b/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 (tim.soethout@ing.com) + +\* 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. +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 + +============================================================================= diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla new file mode 100644 index 00000000..e50ffb19 --- /dev/null +++ b/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}; + \* } + \* }; + + diff --git a/specifications/KeyValueStore/MCKVsnap.cfg b/specifications/KeyValueStore/MCKVsnap.cfg new file mode 100644 index 00000000..c37043fb --- /dev/null +++ b/specifications/KeyValueStore/MCKVsnap.cfg @@ -0,0 +1,18 @@ +CONSTANTS + Key = {k1, k2} + TxId = {t1, t2, t3} + NoVal = NoVal + +SYMMETRY + TxIdSymmetric + +SPECIFICATION + Spec + +INVARIANTS + TypeOK + SnapshotIsolation +\* Serialization + +PROPERTIES + Termination \ No newline at end of file diff --git a/specifications/KeyValueStore/MCKVsnap.tla b/specifications/KeyValueStore/MCKVsnap.tla new file mode 100644 index 00000000..4f672b21 --- /dev/null +++ b/specifications/KeyValueStore/MCKVsnap.tla @@ -0,0 +1,5 @@ +---- MODULE MCKVsnap ---- +EXTENDS KVsnap, TLC +TxIdSymmetric == Permutations(TxId) +==== + diff --git a/specifications/KeyValueStore/README.md b/specifications/KeyValueStore/README.md new file mode 100644 index 00000000..f0e225bf --- /dev/null +++ b/specifications/KeyValueStore/README.md @@ -0,0 +1,16 @@ +This repo contains TLA+ specifications of simple key-value store exhibiting snapshot algorithm. + +## TLA+ model +Andrew Helwer contributed the following: ++ `KeyValueStore.tla` has the TLA+ specs for the key-value store with snapshot isolation ++ `MCKS.tla` is the file to use for TLC model checking ++ `MCKVS*.cfg` are alternative config files to use for TLC checking + + +## PlusCal model +Murat Demirbas wrote a PlusCal version of the key-value store with snapshot isolation. He also instantiated the `ClientCentric.tla` (from Tim Soethout's work) to be able to properly check the key-value store for snapshot isolation semantics. ++ `KVsnap.tla` is the Pluscal model for the key-value store ++ `MCKVsnap.tla` is the file to use for TLC model checking ++ `MCKVsnap.cfg` is the corresponding config file for model checking (with this config, model checking completes under a minute; it is possible to add another key and model check) + +If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability. \ No newline at end of file diff --git a/specifications/KeyValueStore/Util.tla b/specifications/KeyValueStore/Util.tla new file mode 100644 index 00000000..1f6dddb2 --- /dev/null +++ b/specifications/KeyValueStore/Util.tla @@ -0,0 +1,49 @@ +-------------------------------- MODULE Util -------------------------------- +EXTENDS Sequences, FiniteSets, Naturals, TLC +\* Simple utility functions +intersects(a, b) == (Cardinality(a \cap b) > 0) +max(s) == CHOOSE i \in s : (~\E j \in s : j > i) +min(s) == CHOOSE i \in s : (~\E j \in s : j < i) + +\* Utilies from Practical TLA+ +ReduceSet(op(_, _), set, acc) == + LET f[s \in SUBSET set] == \* here's where the magic is + IF s = {} THEN acc + ELSE LET x == CHOOSE x \in s: TRUE + IN op(x, f[s \ {x}]) + IN f[set] +ReduceSeq(op(_, _), seq, acc) == + ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc) +\* Pulls an indice of the sequence for elem. +Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem +\* end from Practical TLA+ + +Range(T) == { T[x] : x \in DOMAIN T } + +SeqToSet(s) == {s[i] : i \in DOMAIN s} +Last(seq) == seq[Len(seq)] +IsEmpty(seq) == Len(seq) = 0 +\* Remove all occurences of `elem` from `seq` +Remove(seq, elem) == SelectSeq(seq, LAMBDA e: e /= elem) + +\* Dual to UNION on intersect +INTERSECTION(setOfSets) == ReduceSet(\intersect, setOfSets, UNION setOfSets) + +\* Borrowed from Stephan Merz. TLA+ Case Study: A Resource Allocator. [Intern report] A04-R-101 || merz04a, 2004, 20 p. ffinria-00107809f +(* The set of permutations of a finite set, represented as sequences. *) +PermSeqs(S) == + LET perms[ss \in SUBSET S] == + IF ss = {} THEN { << >> } + ELSE LET ps == [ x \in ss |-> + { Append(sq,x) : sq \in perms[ss \ {x}] } ] + IN UNION { ps[x] : x \in ss } + IN perms[S] + +\* Helper to write "unit test" ASSUMES which print when false +test(lhs, rhs) == lhs /= rhs => Print(<>, FALSE) + + +============================================================================= +\* Modification History +\* Last modified Tue Jun 16 12:04:20 CEST 2020 by tim +\* Created Tue Apr 28 16:43:24 CEST 2020 by tim From fbaf36a7efa56bbaedb7ca9e56ebf9eb167cc7b1 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Thu, 3 Aug 2023 18:21:13 -0400 Subject: [PATCH 2/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, modified manifest Signed-off-by: Murat Demirbas --- manifest.json | 29 +++++++++++++++++++++++++- specifications/KeyValueStore/README.md | 7 ++++++- 2 files changed, 34 insertions(+), 2 deletions(-) diff --git a/manifest.json b/manifest.json index d5528b4b..019a4dcc 100644 --- a/manifest.json +++ b/manifest.json @@ -453,7 +453,8 @@ "description": "A simple KVS implementing snapshot isolation", "source": "", "authors": [ - "Andrew Helwer" + "Andrew Helwer", + "Murat Demirbas" ], "tags": [], "modules": [ @@ -502,6 +503,32 @@ "result": "success" } ] + }, + { + "path": "specifications/KeyValueStore/KVsnap.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KeyValueStore/MCKVsnap.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [ + { + "path": "specifications/KeyValueStore/MCKVsnap.cfg", + "runtime": "00:00:50", + "size": "medium", + "mode": "exhaustive search", + "config": [], + "features": [ + "symmetry" + ], + "result": "success" + } + ] } ] }, diff --git a/specifications/KeyValueStore/README.md b/specifications/KeyValueStore/README.md index f0e225bf..f7e03efa 100644 --- a/specifications/KeyValueStore/README.md +++ b/specifications/KeyValueStore/README.md @@ -13,4 +13,9 @@ Murat Demirbas wrote a PlusCal version of the key-value store with snapshot isol + `MCKVsnap.tla` is the file to use for TLC model checking + `MCKVsnap.cfg` is the corresponding config file for model checking (with this config, model checking completes under a minute; it is possible to add another key and model check) -If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability. \ No newline at end of file +If you uncomment the Serialization invariant in `KVsnap.tla`, and `MCKVsnap.cfg`, you can see a counterexample of how this snapshot-isolation key-value store violates serializability. + +## Model checking with VSCode TLA+ plugin ++ Make sure TLA+ plugin is installed in VSCode ++ Open the .cfg file you are interested in checking in VSCode ++ Get the VSCode panel (Option+X on Mac), and choose "TLA+: Check Model with TLC") \ No newline at end of file From 013bdd1a3eef3bbd8e9f929ed8971f36bb0f01fd Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Thu, 3 Aug 2023 18:33:00 -0400 Subject: [PATCH 3/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, modified manifest for a fix Signed-off-by: Murat Demirbas --- manifest.json | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/manifest.json b/manifest.json index 019a4dcc..24604de5 100644 --- a/manifest.json +++ b/manifest.json @@ -529,7 +529,21 @@ "result": "success" } ] - } + }, + { + "path": "specifications/KeyValueStore/Util.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + }, + { + "path": "specifications/KeyValueStore/ClientCentric.tla", + "communityDependencies": [], + "tlaLanguageVersion": 2, + "features": [], + "models": [] + } ] }, { From 386b1f1541ad35f8fedd6df3e87bf113d80610d6 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Thu, 3 Aug 2023 18:38:23 -0400 Subject: [PATCH 4/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, added manifest Signed-off-by: Murat Demirbas --- manifest.json | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/manifest.json b/manifest.json index 24604de5..08459533 100644 --- a/manifest.json +++ b/manifest.json @@ -508,7 +508,7 @@ "path": "specifications/KeyValueStore/KVsnap.tla", "communityDependencies": [], "tlaLanguageVersion": 2, - "features": [], + "features": ["pluscal"], "models": [] }, { @@ -524,6 +524,7 @@ "mode": "exhaustive search", "config": [], "features": [ + "liveness", "symmetry" ], "result": "success" From f4f5984a809641cb21fcab5fb597e5033f01c096 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Sat, 5 Aug 2023 16:33:48 -0400 Subject: [PATCH 5/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified manifest Signed-off-by: Murat Demirbas --- specifications/KeyValueStore/KVsnap.tla | 5 ++--- specifications/KeyValueStore/LICENSE | 25 ++++++++++++++++++++++++ specifications/KeyValueStore/Util.tla | 26 +++++++++++-------------- 3 files changed, 38 insertions(+), 18 deletions(-) create mode 100644 specifications/KeyValueStore/LICENSE diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla index e50ffb19..3011ea0d 100644 --- a/specifications/KeyValueStore/KVsnap.tla +++ b/specifications/KeyValueStore/KVsnap.tla @@ -40,7 +40,6 @@ variables 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 @@ -101,12 +100,12 @@ COMMIT: \* Commit the transaction to the database if there is no conflict } *) -\* BEGIN TRANSLATION (chksum(pcal) = "38698f36" /\ chksum(tla) = "2d9d1e7d") +\* BEGIN TRANSLATION (chksum(pcal) = "2e9a6c18" /\ chksum(tla) = "5ad2eccd") 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) diff --git a/specifications/KeyValueStore/LICENSE b/specifications/KeyValueStore/LICENSE new file mode 100644 index 00000000..87a9458a --- /dev/null +++ b/specifications/KeyValueStore/LICENSE @@ -0,0 +1,25 @@ +BSD 2-Clause License for ClientCentric.tla + +Copyright (c) 2020, ING Bank / CWI +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +2. Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. \ No newline at end of file diff --git a/specifications/KeyValueStore/Util.tla b/specifications/KeyValueStore/Util.tla index 1f6dddb2..6e043b08 100644 --- a/specifications/KeyValueStore/Util.tla +++ b/specifications/KeyValueStore/Util.tla @@ -1,24 +1,20 @@ -------------------------------- MODULE Util -------------------------------- -EXTENDS Sequences, FiniteSets, Naturals, TLC +EXTENDS Sequences, FiniteSets, Functions, Naturals, TLC \* Simple utility functions intersects(a, b) == (Cardinality(a \cap b) > 0) max(s) == CHOOSE i \in s : (~\E j \in s : j > i) min(s) == CHOOSE i \in s : (~\E j \in s : j < i) -\* Utilies from Practical TLA+ -ReduceSet(op(_, _), set, acc) == - LET f[s \in SUBSET set] == \* here's where the magic is - IF s = {} THEN acc - ELSE LET x == CHOOSE x \in s: TRUE - IN op(x, f[s \ {x}]) - IN f[set] -ReduceSeq(op(_, _), seq, acc) == - ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc) -\* Pulls an indice of the sequence for elem. -Index(seq, elem) == CHOOSE i \in 1..Len(seq): seq[i] = elem -\* end from Practical TLA+ - -Range(T) == { T[x] : x \in DOMAIN T } +ReduceSet(op(_, _), set, base) == + LET iter[s \in SUBSET set] == + IF s = {} THEN base + ELSE LET x == CHOOSE x \in s: TRUE + IN op(x, iter[s \ {x}]) + IN iter[set] + +ReduceSeq(op(_, _), seq, acc) == FoldFunction(op, acc, seq) + +Index(seq, e) == CHOOSE i \in 1..Len(seq): seq[i] = e SeqToSet(s) == {s[i] : i \in DOMAIN s} Last(seq) == seq[Len(seq)] From adb3d2aa3f62812a2becd5c2f6700d69eb1c5134 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Sat, 5 Aug 2023 16:39:14 -0400 Subject: [PATCH 6/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest Signed-off-by: Murat Demirbas --- manifest.json | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/manifest.json b/manifest.json index 08459533..8bb3a6fe 100644 --- a/manifest.json +++ b/manifest.json @@ -533,7 +533,9 @@ }, { "path": "specifications/KeyValueStore/Util.tla", - "communityDependencies": [], + "communityDependencies": [ + "Functions" + ], "tlaLanguageVersion": 2, "features": [], "models": [] From 8687adf4278e9acdbe3528cb939863b466d5ef36 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Tue, 8 Aug 2023 23:34:03 -0400 Subject: [PATCH 7/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest Signed-off-by: Murat Demirbas --- specifications/KeyValueStore/Util.tla | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/specifications/KeyValueStore/Util.tla b/specifications/KeyValueStore/Util.tla index 6e043b08..b4012922 100644 --- a/specifications/KeyValueStore/Util.tla +++ b/specifications/KeyValueStore/Util.tla @@ -1,7 +1,7 @@ -------------------------------- MODULE Util -------------------------------- -EXTENDS Sequences, FiniteSets, Functions, Naturals, TLC +EXTENDS Sequences, Functions, Naturals, TLC \* Simple utility functions -intersects(a, b) == (Cardinality(a \cap b) > 0) +intersects(a, b) == a \cap b # {} max(s) == CHOOSE i \in s : (~\E j \in s : j > i) min(s) == CHOOSE i \in s : (~\E j \in s : j < i) @@ -41,5 +41,5 @@ test(lhs, rhs) == lhs /= rhs => Print(<>, FALSE) ============================================================================= \* Modification History -\* Last modified Tue Jun 16 12:04:20 CEST 2020 by tim +\* Last modified Sun Aug 05 16:44:44 ET 2023 by murat \* Created Tue Apr 28 16:43:24 CEST 2020 by tim From 94fa1b21c2cae7c9cc1d3470466ae507cc54c0b0 Mon Sep 17 00:00:00 2001 From: Murat Demirbas Date: Tue, 22 Aug 2023 16:27:53 -0400 Subject: [PATCH 8/8] Added Pluscal version of the key-value store with snapshot isolation, instantiated clientcentric checking to model check for snapshot isolation properly, added LICENSE for clientcentric module and modified the manifest, improved the model, and handled CR comments Signed-off-by: Murat Demirbas --- .../KeyValueStore/ClientCentric.tla | 4 +- specifications/KeyValueStore/KVsnap.tla | 69 +++++++------------ 2 files changed, 27 insertions(+), 46 deletions(-) diff --git a/specifications/KeyValueStore/ClientCentric.tla b/specifications/KeyValueStore/ClientCentric.tla index 39543aa2..3cf66553 100644 --- a/specifications/KeyValueStore/ClientCentric.tla +++ b/specifications/KeyValueStore/ClientCentric.tla @@ -40,7 +40,7 @@ executionStates(execution) == [ i \in 1..Len(execution) |-> execution[i].parentS 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. +\* 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′)" @@ -81,7 +81,7 @@ PrereadAll(execution, transactions) == 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 contains all previous states, to ensure that empty txns do not incorrectly invalidate the checked isolation level readStatesForEmptyTransaction == { s \in SeqToSet(executionStates(execution)) : beforeOrEqualInExecution(execution, s, parentState(execution, transaction)) } IN state \in INTERSECTION(setOfAllReadStatesOfOperation(transaction) \union { readStatesForEmptyTransaction } ) diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla index 3011ea0d..a2dbe08a 100644 --- a/specifications/KeyValueStore/KVsnap.tla +++ b/specifications/KeyValueStore/KVsnap.tla @@ -25,12 +25,6 @@ variables \* 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 |-> {}], @@ -50,8 +44,6 @@ define { 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] } @@ -59,12 +51,13 @@ define { \* Transaction processing fair process (t \in TxId) variables + snapshotStore = [k \in Key |-> NoVal], \* local snapshot of the store 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 + snapshotStore := 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 @@ -74,25 +67,24 @@ START: \* Start the transaction 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}); + ops[self] := ops[self] \o SetToSeq({rOp(k, snapshotStore[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; + snapshotStore := [k \in Key |-> IF k \in write_keys THEN self ELSE snapshotStore[k] ]; COMMIT: \* Commit the transaction to the database if there is no conflict - if (missed[self] \intersect written[self] = {}) { + if (missed[self] \intersect write_keys = {}) { \* 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]]; + missed := [o \in TxId |-> IF o \in tx THEN missed[o] \union write_keys ELSE missed[o]]; \* update store - store := [k \in Key |-> IF k \in written[self] THEN snapshotStore[self][k] ELSE store[k] ]; + store := [k \in Key |-> IF k \in write_keys THEN snapshotStore[k] ELSE store[k] ]; \* log reads for CC isolation check - ops[self] := ops[self] \o SetToSeq({wOp(k, self): k \in written[self]}); + ops[self] := ops[self] \o SetToSeq({wOp(k, self): k \in write_keys}); } } @@ -100,12 +92,11 @@ COMMIT: \* Commit the transaction to the database if there is no conflict } *) -\* BEGIN TRANSLATION (chksum(pcal) = "2e9a6c18" /\ chksum(tla) = "5ad2eccd") -VARIABLES store, tx, snapshotStore, written, missed, ops, pc +\* BEGIN TRANSLATION (chksum(pcal) = "5ef5c453" /\ chksum(tla) = "f592c6a0") +VARIABLES store, tx, missed, ops, pc (* define statement *) InitialState == [k \in Key |-> NoVal] - SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f) @@ -116,25 +107,22 @@ 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 +VARIABLES snapshotStore, read_keys, write_keys -vars == << store, tx, snapshotStore, written, missed, ops, pc, read_keys, - write_keys >> +vars == << store, tx, missed, ops, pc, snapshotStore, 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 *) + /\ snapshotStore = [self \in TxId |-> [k \in Key |-> NoVal]] /\ read_keys = [self \in TxId |-> {}] /\ write_keys = [self \in TxId |-> {}] /\ pc = [self \in ProcSet |-> "START"] @@ -147,30 +135,29 @@ START(self) == /\ pc[self] = "START" /\ read_keys' = [read_keys EXCEPT ![self] = rk] /\ write_keys' = [write_keys EXCEPT ![self] = wk] /\ pc' = [pc EXCEPT ![self] = "READ"] - /\ UNCHANGED << store, written, missed, ops >> + /\ UNCHANGED << store, 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 >> + /\ UNCHANGED << store, tx, missed, snapshotStore, 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] = {} + /\ IF missed[self] \intersect write_keys[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]})] + /\ missed' = [o \in TxId |-> IF o \in tx' THEN missed[o] \union write_keys[self] ELSE missed[o]] + /\ store' = [k \in Key |-> IF k \in write_keys[self] THEN snapshotStore[self][k] ELSE store[k] ] + /\ ops' = [ops EXCEPT ![self] = ops[self] \o SetToSeq({wOp(k, self): k \in write_keys[self]})] ELSE /\ TRUE /\ UNCHANGED << store, tx, missed, ops >> /\ pc' = [pc EXCEPT ![self] = "Done"] - /\ UNCHANGED << snapshotStore, written, read_keys, write_keys >> + /\ UNCHANGED << snapshotStore, read_keys, write_keys >> t(self) == START(self) \/ READ(self) \/ UPDATE(self) \/ COMMIT(self) @@ -190,14 +177,8 @@ Termination == <>(\A self \in ProcSet: pc[self] = "Done") =========================================================================== -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}; - \* } - \* }; +As an exercise try to add more yield points, make the actions smaller. +Especially see if you can pull out something from the atomic "COMMIT" label to earlier, and see what breaks. +