From 9e508c68f74c2c2b939417cd4e55668759ef33b2 Mon Sep 17 00:00:00 2001 From: siddontang Date: Sun, 28 Jan 2018 21:24:32 +0800 Subject: [PATCH] add Percolator specification --- Percolator.tla | 336 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 336 insertions(+) create mode 100644 Percolator.tla diff --git a/Percolator.tla b/Percolator.tla new file mode 100644 index 0000000..d3032a4 --- /dev/null +++ b/Percolator.tla @@ -0,0 +1,336 @@ +---------------------------- MODULE Percolator ---------------------------- + +EXTENDS Integers, Sequences, Bags, TLC + +\* The set of transaction keys +CONSTANTS KEY + +\* The set of client to execute a transaction +CONSTANTS CLIENT + +\* next_ts is the timestamp for transaction. It is increased monotonically so +\* every transaction must have a unique start and commit ts. +VARIABLES next_ts + +\* $client_state[c] is the state of client +VARIABLES client_state + +\* $client_ts[c] is a record of [start: ts, commit: ts] +VARIABLES client_ts + +\* $client_keys[c] is a record of [primary: key, second: {key}] +VARIABLES client_key + +\* $key_lock[k] is the set of lock. +VARIABLES key_lock + +\* $key_write[k] is a sequence of committed version of the key. +VARIABLES key_write + +\* $key_data[k] is the set of multi-version data timestamp of the key. +VARIABLES key_data + +Init == + /\ next_ts = 0 + /\ client_state = [c \in CLIENT |-> "init"] + /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, commit_ts |-> 0]] + /\ client_key = [c \in CLIENT |-> [primary |-> "", secondary |-> {}]] + /\ key_lock = [k \in KEY |-> {}] + /\ key_write = [k \in KEY |-> <<>>] + /\ key_data = [k \in KEY |-> {}] + + +key_vars == <> +client_txn_vars == <> + + +\* Check whether there is a lock which start ts is less or equal than start_ts. +hasLockLE(k, start_ts) == + {l \in key_lock[k] : l.start_ts <= start_ts} /= {} + +\* Check whether there is a lock with start ts or not. +hasLockEQ(k, start_ts) == + {l \in key_lock[k] : l.start_ts <= start_ts} /= {} + +\* Select a primary key and use the rest for the secondary key +chooseKey == + LET + primary == CHOOSE k \in KEY: TRUE + IN + [primary |-> primary, secondary |-> KEY \ {primary}] + +\* Return TRUE means the client meets no lock and can does pre-write. +canPrewrite(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + /\ ~hasLockLE(primary, start_ts) + /\ \A k \in secondary : + /\ ~hasLockLE(k, start_ts) + +\* Return TRUE means a lock can be cleanup up if: +\* 1. The lock is a primary lock and the start ts is less than start_ts. +\* 2. Or the lock is a secondary lock and the associated primary key is cleaned up. +\* Notice: Percolator paper doesn't explain how to clean up the lock, here we just use +\* a simple way. +isStaleLock(l, start_ts) == + \/ /\ l.primary = "" + /\ l.start_ts < start_ts + \/ /\ l.primary /= "" + /\ ~hasLockEQ(l.primary, l.start_ts) + +\* Return TRUE if we have a stale lock for key. +hasStaleLock(k, start_ts) == + \A l \in key_lock[k] : + \/ isStaleLock(l, start_ts) + +\* Return TRUE means the client can clean up a stale lock +canCleanup(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + /\ ~hasStaleLock(primary, start_ts) + /\ \A k \in secondary : + /\ ~hasStaleLock(k, start_ts) + +\* Find write with start ts. +findWriteWithStart(k, start_ts) == + SelectSeq(key_write[k], LAMBDA w : w.start_ts = start_ts) + +\* Clean 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: +\* 1. If the primary key is committed, we must also commit the secondary key +\* 2. Otherwise, clean up the stale data too +cleanupStaleLock(k, start_ts) == + LET + \* Find a stale lock at first + l == CHOOSE l \in key_lock[k] : isStaleLock(l, start_ts) + IN + /\ key_lock' = key_lock \ {l} + /\ \/ /\ l.primary = "" + /\ key_data' = key_data \ {l.start_ts} + /\ UNCHANGED <> + \/ /\ l.primary /= "" + /\ LET + w == findWriteWithStart(l.primary, l.start_ts) + IN + IF Len(w) = 0 + THEN + \* The primary key is not committed, clean up the data + /\ key_data' = key_data \ {l.start_ts} + /\ UNCHANGED <> + ELSE + \* The primary key is committed, commit the secondary key + /\ key_write' = Append(key_write, w[1]) + /\ UNCHANGED <> + +\* Clean up a stale lock when the client meets. +cleanup(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + meetStaleLock(k) == /\ \/ k = primary + \/ k \in secondary + /\ hasStaleLock(k, start_ts) + k == CHOOSE k \in KEY : meetStaleLock(k) + IN + cleanupStaleLock(k, start_ts) + +\* Return TURE means there is no lock for key and no any newer write. +canLockKey(k, start_ts) == + LET + writes == {w \in DOMAIN key_write[k] : key_write[k][w].commit_ts >= start_ts} + IN + \* No any lock for the key + /\ key_lock[k] = {} + \* No any newer write + /\ writes = {} + +\* Return whether the client can lock all keys +canLock(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + /\ canLockKey(primary, start_ts) + /\ \A k \in secondary : + /\ canLockKey(k, start_ts) + +\* Lock the key and save the data +lockKey(k, start_ts, primary) == + /\ key_lock' = [key_lock EXCEPT ![k] = @ \UNION {[start_ts |-> start_ts, primary |-> primary]}] + /\ key_data' = [key_data EXCEPT ![k] = @ \UNION {start_ts}] + /\ UNCHANGED <> + + +\* Try to lock primary key first, then the secondary key +lock(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + IF hasLockEQ(primary, start_ts) + THEN + lockKey(primary, start_ts, "") + ELSE + \* primary key has already been locked, we must choose the a secondary key to lock + LET + k == CHOOSE k \in secondary : canLockKey(k, start_ts) + IN + lockKey(k, start_ts, primary) + +\* Return TRUE when the client locks all keys +canCommit(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + secondary == client_key[c].secondary + IN + /\ hasLockEQ(primary, start_ts) + /\ \A k \in secondary : + /\ hasLockEQ(k, start_ts) + +\* Return TRUE mean we can commit the primary key. +canCommitPrimary(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + IN + hasLockEQ(primary, start_ts) + +\* Commit the primary key. +commitPrimary(c) == + LET + start_ts == client_ts[c].start_ts + primary == client_key[c].primary + IN + /\ key_write' = [key_write EXCEPT ![primary] = Append(@, client_ts[c])] + /\ key_lock' = [key_lock EXCEPT ![primary] = @ \ {start_ts}] + +Start(c) == + /\ client_state[c] = "init" + /\ client_state' = [client_state EXCEPT ![c] = "working"] + /\ next_ts' = next_ts + 1 + /\ client_ts' = [client_ts EXCEPT ![c] = [@ EXCEPT !.start_ts = next_ts']] + /\ client_key' = [client_key EXCEPT ![c] = chooseKey] + /\ UNCHANGED <> + +Get(c) == + /\ client_state[c] = "working" + /\ + IF canPrewrite(c) + THEN + /\ client_state' = [client_state EXCEPT ![c] = "prewriting"] + /\ UNCHANGED <> + ELSE + IF canCleanup(c) + THEN + /\ cleanup(c) + /\ UNCHANGED <> + ELSE + /\ client_state' = [client_state EXCEPT ![c] = "aborted"] + /\ UNCHANGED <> + +Prewrite(c) == + /\ client_state[c] = "prewriting" + /\ IF canCommit(c) + THEN + /\ next_ts' = next_ts + 1 + /\ client_ts' = [client_ts EXCEPT ![c] = [@ EXCEPT !.commit_ts = next_ts']] + /\ client_state' = [client_state EXCEPT ![c] = "committing"] + /\ UNCHANGED <> + ELSE + IF canLock(c) + THEN + /\ lock(c) + /\ UNCHANGED <> + ELSE + /\ client_state' = [client_state EXCEPT ![c] = "aborted"] + /\ UNCHANGED <> + +Commit(c) == + /\ client_state[c] = "committing" + /\ IF canCommitPrimary(c) + THEN + /\ commitPrimary(c) + /\ client_state' = [client_state EXCEPT ![c] = "committed"] + /\ UNCHANGED <> + \* If we commit primary successfully, we can think the transaction is committed + \* TODO: use async message to commit second keys + ELSE + /\ client_state' = [client_state EXCEPT ![c] = "aborted"] + /\ UNCHANGED <> +Next == + \E c \in CLIENT: + Start(c) \/ Get(c) \/ Prewrite(c) \/ Commit(c) + + +checkWriteOrder(w1, w2) == + /\ w1.commit_ts < w2.commit_ts + /\ w1.start_ts < w2.start_ts + /\ w1.start_ts < w1.commit_ts + + +\* The committed write timestamp of the key must be in order. +WriteConsistency == + \A k \in KEY : + IF Len(key_write[k]) > 1 + THEN + LET + ws == [n \in 1..Len(key_write[k]) - 1 |-> checkWriteOrder(key_write[k][n], key_write[k][n + 1])] + IN + ~ FALSE \in ws + ELSE + IF Len(key_write[k]) = 1 + THEN + key_write[k][1].start_ts < key_write[k][1].commit_Ts + ELSE + TRUE + +\* find write with commit ts. +findWriteWithCommit(k, commit_ts) == + SelectSeq(key_write[k], LAMBDA w : w.commit_ts = commit_ts) + +CommittedConsistency == + \A c \in CLIENT : + LET + start_ts == client_ts[c].start + commit_ts == client_ts[c].commit + primary == client_key[c].primary + secondary == client_key[c].second + w == [start |-> start_ts, commit |-> commit_ts] + IN + \/ /\ client_state[c] = "committed" + \* The primary key lock must be cleaned up, and no any older lock. + /\ ~hasLockLE(primary, start_ts) + /\ findWriteWithCommit(primary, commit_ts) = <> + /\ {start_ts} \in key_data[primary] + /\ \A k \in secondary : + \* The secondary key lock can be empty or not. + /\ \/ /\ ~hasLockEQ(k, start_ts) + /\ findWriteWithCommit(k, commit_ts) = <> + /\ ~hasLockLE(k, start_ts - 1) + \/ /\ hasLockEQ(k, start_ts) + /\ findWriteWithCommit(k, commit_ts) = <<>> + /\ + IF Len(key_write[k]) > 0 + THEN + \* Lock has not been cleaned up, so the last write committed + \* timestamp must be less than lock start ts. + key_write[k][Len(key_write[k])].commit_ts < start_ts + ELSE + TRUE + /\ {start_ts} \in key_data[k] + \/ TRUE + +============================================================================= +\* Modification History +\* Last modified Fri Nov 17 16:40:19 CST 2017 by tangliu +\* Created Fri Nov 17 08:55:33 CST 2017 by tangliu