From 92b423e1ce4ab50869c893fe63ebd5a78fd03e60 Mon Sep 17 00:00:00 2001 From: foreverbell Date: Sat, 3 Feb 2018 14:41:09 +0800 Subject: [PATCH] percolator: verify snapshot isolation property. (#6) --- Percolator/Percolator.cfg | 3 +- Percolator/Percolator.tla | 107 +++++++++++++++++++++++++++++++------- 2 files changed, 90 insertions(+), 20 deletions(-) diff --git a/Percolator/Percolator.cfg b/Percolator/Percolator.cfg index 828bc5d..0efe917 100644 --- a/Percolator/Percolator.cfg +++ b/Percolator/Percolator.cfg @@ -1,5 +1,5 @@ CONSTANT - KEY <- 1..5 + KEY <- 1..3 CLIENT <- {"C1", "C2", "C3"} SPECIFICATION @@ -11,3 +11,4 @@ INVARIANT LockConsistency CommittedConsistency AbortedConsistency + SnapshotIsolation diff --git a/Percolator/Percolator.tla b/Percolator/Percolator.tla index edf1f17..a68ea88 100644 --- a/Percolator/Percolator.tla +++ b/Percolator/Percolator.tla @@ -36,10 +36,17 @@ VARIABLES key_lock \* $key_write[k]$ is a sequence of committed version of the key. \* A committed version of the key is a record of [start_ts: ts, commit_ts: ts]. -VARIABLES key_write \* TODO: Rename to key_rw so we can also log reads? +VARIABLES key_write + +\* Two auxiliary variables for verifying snapshot isolation invariant. +\* $key_last_read_ts[k]$ denotes the last read timestamp for key $k$, this +\* should be monotonic. +\* $key_si[k]$ denotes the if the snapshot isolation invariant is preserved for +\* key $k$ so far. +VARIABLES key_last_read_ts, key_si client_vars == <> -key_vars == <> +key_vars == <> vars == <> -------------------------------------------------------------------------------- @@ -69,6 +76,16 @@ findWriteWithStartTS(k, ts) == findWriteWithCommitTS(k, ts) == {key_write[k][w] : w \in {w \in DOMAIN key_write[k] : key_write[k][w].commit_ts = ts}} +\* Updates $key_si$ for key $k$. If a new version of key $k$ is committed with +\* $commit_ts$ < last read timestamp, consider the snapshot isolation invariant +\* for key $k$ has been violated. +checkSnapshotIsolation(k, commit_ts) == + IF key_last_read_ts[k] >= commit_ts + THEN + key_si' = [key_si EXCEPT ![k] = FALSE] + ELSE + UNCHANGED <> + \* Cleans up a stale lock and its data. \* If the lock is a secondary lock, and the assoicated primary lock is cleaned \* up, we can clean up the lock and do, @@ -77,11 +94,12 @@ findWriteWithCommitTS(k, ts) == cleanupStaleLock(k, ts) == \E l \in key_lock[k] : /\ isStaleLock(k, l, ts) + /\ UNCHANGED <> /\ \/ /\ l.primary = k \* this is a primary key, always rollback \* because it is not committed. /\ key_data' = [key_data EXCEPT ![k] = @ \ {l.ts}] /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] - /\ UNCHANGED <> + /\ UNCHANGED <> \/ /\ l.primary # k \* this is a secondary key. /\ LET ws == findWriteWithStartTS(l.primary, l.ts) @@ -95,16 +113,17 @@ cleanupStaleLock(k, ts) == THEN /\ key_data' = [key_data EXCEPT ![l.primary] = @ \ {l.ts}] /\ key_lock' = [key_lock EXCEPT ![l.primary] = @ \ {l}] - /\ UNCHANGED <> + /\ UNCHANGED <> ELSE /\ key_data' = [key_data EXCEPT ![k] = @ \ {l.ts}] /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] - /\ UNCHANGED <> + /\ UNCHANGED <> ELSE \* the primary key is committed, commit the secondary key. \E w \in ws : /\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}] /\ key_write' = [key_write EXCEPT ![k] = Append(@, w)] + /\ checkSnapshotIsolation(k, w.commit_ts) /\ UNCHANGED <> \* Cleans up a stale lock when the client encounters one. @@ -120,6 +139,19 @@ cleanup(c) == /\ hasStaleLock(k, start_ts) /\ cleanupStaleLock(k, start_ts) +\* Reads one key if there is no stale lock, and updates last read timestamp. +readKey(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + \E k \in {primary} \union secondary : + /\ ~hasStaleLock(k, start_ts) + /\ key_last_read_ts[k] < start_ts + /\ key_last_read_ts' = [key_last_read_ts EXCEPT ![k] = start_ts] + /\ UNCHANGED <> + \* Returns TRUE if there is no lock for key $k$, and no any newer write than \* $ts$. canLockKey(k, ts) == @@ -133,7 +165,7 @@ canLockKey(k, ts) == lockKey(k, start_ts, primary) == /\ key_lock' = [key_lock EXCEPT ![k] = @ \union {[ts |-> start_ts, primary |-> primary]}] /\ key_data' = [key_data EXCEPT ![k] = @ \union {start_ts}] - /\ UNCHANGED <> + /\ UNCHANGED <> \* Tries to lock primary key first, then the secondary key. lock(c) == @@ -160,12 +192,14 @@ lock(c) == commitPrimary(c) == LET start_ts == client_ts[c].start_ts + commit_ts == client_ts[c].commit_ts primary == client_key[c].primary IN /\ hasLockEQ(primary, start_ts) /\ key_write' = [key_write EXCEPT ![primary] = Append(@, client_ts[c])] /\ key_lock' = [key_lock EXCEPT ![primary] = @ \ {[ts |-> start_ts, primary |-> primary]}] - /\ UNCHANGED <> + /\ checkSnapshotIsolation(primary, commit_ts) + /\ UNCHANGED <> \* Assigns $start_ts$ to the transaction. Start(c) == @@ -175,14 +209,18 @@ Start(c) == /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts'] /\ UNCHANGED <> -\* Advances to prewrite phase, or tries to clean up one stale lock if we are -\* going to read the corresponding key. +\* Does either one thing from these following threes. +\* 1. Advances to prewrite phase, +\* 2. Tries to clean up one stale lock, +\* 3. Reads one key if no stale lock. Get(c) == /\ client_state[c] = "working" /\ \/ /\ client_state' = [client_state EXCEPT ![c] = "prewriting"] /\ UNCHANGED <> \/ /\ cleanup(c) /\ UNCHANGED <> + \/ /\ readKey(c) + /\ UNCHANGED <> \* Enters commit phase if all locks are granted, otherwise tries to lock the \* primary lock and secondary locks. @@ -239,8 +277,10 @@ Init == /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, commit_ts |-> 0]] /\ client_key = [c \in CLIENT |-> chooseKey(KEY)] /\ key_lock = [k \in KEY |-> {}] - /\ key_write = [k \in KEY |-> <<>>] /\ key_data = [k \in KEY |-> {}] + /\ key_write = [k \in KEY |-> <<>>] + /\ key_last_read_ts = [k \in KEY |-> 0] + /\ key_si = [k \in KEY |-> TRUE] PercolatorSpec == Init /\ [][Next]_vars @@ -269,6 +309,12 @@ KeyLockTypeInv == KeyWriteTypeInv == key_write \in [KEY -> Seq([start_ts : Nat, commit_ts : Nat])] +KeyLastReadTsTypeInv == + key_last_read_ts \in [KEY -> Nat] + +KeySiTypeInv == + key_si \in [KEY -> BOOLEAN] + TypeInvariant == /\ NextTsTypeInv /\ ClientStateTypeInv @@ -277,6 +323,8 @@ TypeInvariant == /\ KeyDataTypeInv /\ KeyLockTypeInv /\ KeyWriteTypeInv + /\ KeyLastReadTsTypeInv + /\ KeySiTypeInv -------------------------------------------------------------------------------- \* The committed write timestamp of one key must be in order, and no two writes @@ -338,6 +386,11 @@ AbortedConsistency == ) => findWriteWithCommitTS(client_key[c].primary, client_ts[c].commit_ts) = {} +\* Snapshot isolation invariant should be preserved. +SnapshotIsolation == + \A k \in KEY : + key_si[k] = TRUE + -------------------------------------------------------------------------------- \* TLAPS proof for proving Spec keeps type invariant. LEMMA InitStateSatisfiesTypeInvariant == @@ -345,7 +398,8 @@ LEMMA InitStateSatisfiesTypeInvariant == PROOF <1> USE DEF Init, TypeInvariant <1> USE DEF NextTsTypeInv, ClientStateTypeInv, ClientTsTypeInv, ClientKeyTypeInv, - KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv + KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv, + KeyLastReadTsTypeInv, KeySiTypeInv <1> QED BY SMT, KeyNotEmpty LEMMA findWriteWithStartTSTypeInv == @@ -375,10 +429,11 @@ PROOF <1>a CASE Start(c) <2> USE DEF Start <2> USE DEF NextTsTypeInv, ClientStateTypeInv, ClientTsTypeInv, ClientKeyTypeInv, - KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv + KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv, + KeyLastReadTsTypeInv, KeySiTypeInv <2> QED BY <1>a <1>b CASE Get(c) - <2> USE DEF Get, cleanup + <2> USE DEF Get, cleanup, readKey <2>a NextTsTypeInv' BY <1>b DEF NextTsTypeInv <2>b ClientStateTypeInv' @@ -400,7 +455,14 @@ PROOF DEF ClientTsTypeInv, ClientKeyTypeInv, KeyWriteTypeInv, KeyLockTypeInv, KeyDataTypeInv, cleanupStaleLock <3> QED BY <1>b, <3>a DEF KeyWriteTypeInv, ClientKeyTypeInv, ClientTsTypeInv - <2> QED BY <2>a, <2>b, <2>c, <2>d, <2>e, <2>f, <2>g + <2>h KeyLastReadTsTypeInv' + <3>a ASSUME readKey(c) + PROVE KeyLastReadTsTypeInv' + BY <3>a DEF KeyLastReadTsTypeInv, ClientKeyTypeInv, ClientTsTypeInv + <3> QED BY <1>b, <3>a DEF KeyLastReadTsTypeInv, cleanupStaleLock + <2>i KeySiTypeInv' + BY <1>b DEF KeySiTypeInv, cleanupStaleLock, checkSnapshotIsolation + <2> QED BY <2>a, <2>b, <2>c, <2>d, <2>e, <2>f, <2>g, <2>h, <2>i <1>c CASE Prewrite(c) <2> USE DEF Prewrite, lock, lockKey <2>a NextTsTypeInv' @@ -443,16 +505,22 @@ PROOF <3> QED BY <3>a, <3>b <2>g KeyWriteTypeInv' BY <1>c DEF KeyWriteTypeInv - <2> QED BY <2>a, <2>b, <2>c, <2>d, <2>e, <2>f, <2>g + <2>h KeyLastReadTsTypeInv' + BY <1>c DEF KeyLastReadTsTypeInv + <2>i KeySiTypeInv' + BY <1>c DEF KeySiTypeInv + <2> QED BY <2>a, <2>b, <2>c, <2>d, <2>e, <2>f, <2>g, <2>h, <2>i <1>d CASE Commit(c) - <2> USE DEF Commit, commitPrimary, lock, lockKey + <2> USE DEF Commit, commitPrimary, lock, lockKey, checkSnapshotIsolation <2> USE DEF NextTsTypeInv, ClientStateTypeInv, ClientTsTypeInv, ClientKeyTypeInv, - KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv + KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv, + KeyLastReadTsTypeInv, KeySiTypeInv <2> QED BY <1>d <1>e CASE Abort(c) <2> USE DEF Abort <2> USE DEF NextTsTypeInv, ClientStateTypeInv, ClientTsTypeInv, ClientKeyTypeInv, - KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv + KeyDataTypeInv, KeyLockTypeInv, KeyWriteTypeInv, + KeyLastReadTsTypeInv, KeySiTypeInv <2> QED BY <1>e <1> QED BY <1>a, <1>b, <1>c, <1>d, <1>e DEF ClientOp @@ -468,6 +536,7 @@ THEOREM Safety == /\ WriteConsistency /\ LockConsistency /\ CommittedConsistency - /\ AbortedConsistency) + /\ AbortedConsistency + /\ SnapshotIsolation) ================================================================================