---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/KVsnap.tla
---
-------------------------------- MODULE KVsnap ---------------------------------
(**************************************************************************)
(* Pluscal algorithm 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, 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}
\* for instantiating the ClientCentric module
wOp(k, v) == CC!w(k,v)
rOp(k, v) == CC!r(k,v)
InitialState == [k \in Key |-> NoVal]
SetToSeq(S) == CHOOSE f \in [1..Cardinality(S) -> S]: IsInjective(f)
(* --algorithm KVsnap {
variables
\* A data store mapping keys to values
store = [k \in Key |-> NoVal],
\* The set of open snapshot transactions
tx = {},
\* The set of writes invisible to each transaction
missed = [t \in TxId |-> {}];
\* See end of file for invariants
\* 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
ops = <<>>; \* a log of reads & writes this transaction executes; used for interfacing to CC
{
START: \* Start the transaction
tx := tx \union {self};
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
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 := ops \o SetToSeq({rOp(k, snapshotStore[k]): k \in read_keys});
UPDATE: \* Process writes on my snapshot, write 'self' as value
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 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 write_keys ELSE missed[o]];
\* update store
store := [k \in Key |-> IF k \in write_keys THEN snapshotStore[k] ELSE store[k] ];
\* log reads for CC isolation check
ops := ops \o SetToSeq({wOp(k, self): k \in write_keys});
}
}
}
*)
\* BEGIN TRANSLATION (chksum(pcal) = "1adfcb46" /\ chksum(tla) = "5b28617f")
VARIABLES store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
vars == << store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
>>
ProcSet == (TxId)
Init == (* Global variables *)
/\ store = [k \in Key |-> NoVal]
/\ tx = {}
/\ missed = [t \in TxId |-> {}]
(* Process t *)
/\ snapshotStore = [self \in TxId |-> [k \in Key |-> NoVal]]
/\ read_keys = [self \in TxId |-> {}]
/\ write_keys = [self \in TxId |-> {}]
/\ ops = [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, 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, 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]]]
/\ pc' = [pc EXCEPT ![self] = "COMMIT"]
/\ UNCHANGED << store, tx, missed, read_keys, write_keys, ops >>
COMMIT(self) ==
/\ pc[self] = "COMMIT"
/\ IF missed[self] \intersect write_keys[self] = {}
THEN
/\ tx' = tx \ {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, 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
\* Snapshot isolation invariant
SnapshotIsolation == CC!SnapshotIsolation(InitialState, Range(ops))
TypeOK == \* type invariant
/\ store \in [Key -> TxId \union {NoVal}]
/\ tx \subseteq TxId
/\ missed \in [TxId -> SUBSET Key]
\* Serializability would not be satisfied due to write-skew
Serialization == CC!Serializability(InitialState, Range(ops))
================================================================================
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.