mirror of
https://github.com/pingcap/tla-plus.git
synced 2025-04-15 19:50:29 +08:00
percolator: verify snapshot isolation property. (#6)
This commit is contained in:
foreverbell
siddontang
parent
013fe46836
commit
92b423e1ce
Percolator
@ -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
|
||||
|
||||
@ -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 == <<client_state, client_ts, client_key>>
|
||||
key_vars == <<key_data, key_lock, key_write>>
|
||||
key_vars == <<key_data, key_lock, key_write, key_last_read_ts, key_si>>
|
||||
vars == <<next_ts, client_vars, key_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 <<key_si>>
|
||||
|
||||
\* 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 <<key_last_read_ts>>
|
||||
/\ \/ /\ 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 <<key_write>>
|
||||
/\ UNCHANGED <<key_write, key_si>>
|
||||
\/ /\ 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 <<key_write>>
|
||||
/\ UNCHANGED <<key_write, key_si>>
|
||||
ELSE
|
||||
/\ key_data' = [key_data EXCEPT ![k] = @ \ {l.ts}]
|
||||
/\ key_lock' = [key_lock EXCEPT ![k] = @ \ {l}]
|
||||
/\ UNCHANGED <<key_write>>
|
||||
/\ UNCHANGED <<key_write, key_si>>
|
||||
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 <<key_data>>
|
||||
|
||||
\* 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 <<key_data, key_lock, key_write, key_si>>
|
||||
|
||||
\* 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 <<key_write>>
|
||||
/\ UNCHANGED <<key_write, key_last_read_ts, key_si>>
|
||||
|
||||
\* 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 <<key_data>>
|
||||
/\ checkSnapshotIsolation(primary, commit_ts)
|
||||
/\ UNCHANGED <<key_data, key_last_read_ts>>
|
||||
|
||||
\* 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 <<key_vars, client_key>>
|
||||
|
||||
\* 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 <<next_ts, key_vars, client_ts, client_key>>
|
||||
\/ /\ cleanup(c)
|
||||
/\ UNCHANGED <<next_ts, client_vars>>
|
||||
\/ /\ readKey(c)
|
||||
/\ UNCHANGED <<next_ts, client_vars>>
|
||||
|
||||
\* 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)
|
||||
|
||||
================================================================================
|
||||
|
||||
Loading…
Reference in New Issue
Block a user