diff --git a/.gitignore b/.gitignore index 6e72a9c..a3fd7a7 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,7 @@ states/ **/*.toolbox/*___*_SnapShot_*.launch **/*.toolbox/.project **/*.toolbox/.settings/ +**/*.toolbox/*.aux +**/*.toolbox/*.log +**/*.toolbox/*.pdf +**/*.toolbox/*.tex diff --git a/DistributedTransaction/DistributedTransaction.pdf b/DistributedTransaction/DistributedTransaction.pdf index defaace..e020e0d 100644 Binary files a/DistributedTransaction/DistributedTransaction.pdf and b/DistributedTransaction/DistributedTransaction.pdf differ diff --git a/DistributedTransaction/DistributedTransaction.tla b/DistributedTransaction/DistributedTransaction.tla index 151410c..3109719 100644 --- a/DistributedTransaction/DistributedTransaction.tla +++ b/DistributedTransaction/DistributedTransaction.tla @@ -1,5 +1,5 @@ ----------------------- MODULE DistributedTransaction ----------------------- -EXTENDS Integers, FiniteSets +EXTENDS Integers, FiniteSets, TLC \* The set of all keys. CONSTANTS KEY @@ -8,251 +8,388 @@ CONSTANTS KEY CONSTANTS OPTIMISTIC_CLIENT, PESSIMISTIC_CLIENT CLIENT == PESSIMISTIC_CLIENT \union OPTIMISTIC_CLIENT -\* CLIENT_KEY is a set of [Client -> SUBSET KEY] -\* representing the involved keys of each client. -CONSTANTS CLIENT_KEY -ASSUME \A c \in CLIENT: CLIENT_KEY[c] \subseteq KEY +CONSTANTS CLIENT_READ_KEY, CLIENT_WRITE_KEY +CLIENT_KEY == [c \in CLIENT |-> CLIENT_READ_KEY[c] \union CLIENT_WRITE_KEY[c]] \* CLIENT_PRIMARY is the primary key of each client. CONSTANTS CLIENT_PRIMARY + +\* Pessimistic clients can't read a key without writing it and commit it, +\* and pessimistic client read the keys while acquiring pessimistic locks +\* so the CLIENT_READ_KEY for pessimistic clients should be empty. +ASSUME \A c \in PESSIMISTIC_CLIENT: CLIENT_READ_KEY[c] = {} + +ASSUME \A c \in CLIENT: CLIENT_KEY[c] \subseteq KEY ASSUME \A c \in CLIENT: CLIENT_PRIMARY[c] \in CLIENT_KEY[c] -\* Timestamp of transactions. -Ts == Nat \ {0} -NoneTs == 0 - \* The algorithm is easier to understand in terms of the set of msgs of -\* all messages that have ever been sent. A more accurate model would use +\* all messages that have ever been sent. A more accurate model would use \* one or more variables to represent the messages actually in transit, \* and it would include actions representing message loss and duplication \* as well as message receipt. \* \* In the current spec, there is no need to model message loss because we -\* are mainly concerned with the algorithm's safety property. The safety +\* are mainly concerned with the algorithm's safety property. The safety \* part of the spec says only what messages may be received and does not -\* assert that any message actually is received. Thus, there is no +\* assert that any message actually is received. Thus, there is no \* difference between a lost message and one that is never received. VARIABLES req_msgs VARIABLES resp_msgs -\* key_data[k] is the set of multi-version data of the key. Since we +\* key_data[k] is the set of multi-version data of the key. Since we \* don't care about the concrete value of data, a start_ts is sufficient \* to represent one data version. VARIABLES key_data -\* key_lock[k] is the set of lock (zero or one element). A lock is of a -\* record of [ts: start_ts, primary: key, type: lock_type]. If primary -\* equals to k, it is a primary lock, otherwise secondary lock. lock_type +\* key_lock[k] is the set of lock (zero or one element). A lock is of a +\* record of [ts: start_ts, primary: key, type: lock_type]. If primary +\* equals to k, it is a primary lock, otherwise secondary lock. lock_type \* is one of {"prewrite_optimistic", "prewrite_pessimistic", "lock_key"}. \* lock_key denotes the pessimistic lock performed by ServerLockKey \* action, the prewrite_pessimistic denotes percolator optimistic lock \* who is transformed from a lock_key lock by action \* ServerPrewritePessimistic, and prewrite_optimistic denotes the \* classic optimistic lock. -\* +\* \* In TiKV, key_lock has an additional for_update_ts field and the -\* LockType is of four variants: +\* LockType is of four variants: \* {"PUT", "DELETE", "LOCK", "PESSIMISTIC"}. -\* +\* \* In the spec, we abstract them by: \* (1) LockType \in {"PUT", "DELETE", "LOCK"} /\ for_update_ts = 0 <=> \* type = "prewrite_optimistic" \* (2) LockType \in {"PUT", "DELETE"} /\ for_update_ts > 0 <=> \* type = "prewrite_pessimistic" \* (3) LockType = "PESSIMISTIC" <=> type = "lock_key" +\* +\* There's an min_commit_ts field to indicate the minimum commit time +\* It's used in non-blocked reading. +\* TODO: upd min_commit_ts comment. VARIABLES key_lock \* key_write[k] is a sequence of commit or rollback record of the key. -\* It's a record of [ts, start_ts, type, [protected]]. type can be either -\* "write" or "rollback". ts represents the commit_ts of "write" record. -\* Otherwise, ts equals to start_ts on "rollback" record. "rollback" -\* record has an additional protected field. protected signifies the +\* It's a record of [ts, start_ts, type, [protected]]. type can be either +\* "commit" or "rollback". ts represents the commit_ts of "commit" record. +\* Otherwise, ts equals to start_ts on "rollback" record. "rollback" +\* record has an additional protected field. protected signifies the \* rollback record would not be collapsed. VARIABLES key_write -\* client_state[c] indicates the current transaction stage of client c. -VARIABLES client_state -\* client_ts[c] is a record of [start_ts, commit_ts, for_update_ts]. +\* client_stage[c] indicates the current transaction stage of client c. +VARIABLES client_stage +\* client_ts[c] is a record of [start_ts, commit_ts, for_update_ts, min_commit_ts]. \* Fields are all initialized to NoneTs. VARIABLES client_ts -\* client_key[c] is a record of [locking: {key}, prewriting: {key}]. -\* Hereby, "locking" denotes the keys whose pessimistic locks -\* haven't been acquired, "prewriting" denotes the keys that are pending -\* for prewrite. +\* client_key[c] is a record of [reading: {key}, locking: {key}, prewriting: {key}]. +\* Hereby, "reading" denotes the keys that the optimistic client is reading, +\* "locking" denotes the keys that the pessimistic client is acquiring for pessimistic +\* locks, and "prewriting" denotes the keys that are waiting for prewrite success. VARIABLES client_key +\* client_read[c][k] stores the value that the client has read from server for +\* key `k` (by optimsitic read or pessimistic lock key). This is used for checking +\* snapshot isolation. +VARIABLES client_read \* next_ts is a globally monotonically increasing integer, representing -\* the virtual clock of transactions. In practice, the variable is +\* the virtual clock of transactions. In practice, the variable is \* maintained by PD, the time oracle of a cluster. VARIABLES next_ts msg_vars == <> -client_vars == <> +client_vars == <> key_vars == <> vars == <> +SendReq(msg) == req_msgs' = req_msgs \union {msg} SendReqs(msgs) == req_msgs' = req_msgs \union msgs SendResp(msg) == resp_msgs' = resp_msgs \union {msg} +SendResps(msgs) == resp_msgs' = resp_msgs \union msgs ----------------------------------------------------------------------------- \* Type Definitions +\* Timestamp for transactions. +Ts == Nat \ {0} +NoneTs == 0 + +\* Represents the data version read from TiKV. NoneTs means that the value is empty. +ValueTs == Ts \union {NoneTs} + +\* The messages that sent from client to the server. ReqMessages == [start_ts : Ts, primary : KEY, type : {"lock_key"}, key : KEY, for_update_ts : Ts] + \union [start_ts : Ts, primary : KEY, type : {"read_optimistic"}, key : KEY] \union [start_ts : Ts, primary : KEY, type : {"prewrite_optimistic"}, key : KEY] \union [start_ts : Ts, primary : KEY, type : {"prewrite_pessimistic"}, key : KEY] \union [start_ts : Ts, primary : KEY, type : {"commit"}, commit_ts : Ts] - \union [start_ts : Ts, primary : KEY, type : {"cleanup"}] \union [start_ts : Ts, primary : KEY, type : {"resolve_rollbacked"}] \union [start_ts : Ts, primary : KEY, type : {"resolve_committed"}, commit_ts : Ts] -RespMessages == - [start_ts : Ts, type : {"prewrited", "locked_key"}, key : KEY] - \union [start_ts : Ts, type : {"lock_failed"}, key : KEY, latest_commit_ts : Ts] - \union [start_ts : Ts, type : {"committed", - "commit_aborted", - "prewrite_aborted", - "lock_key_aborted"}] + \* In TiKV, there's an extra flag `rollback_if_not_exist` in the `check_txn_status` request. + \* + \* Because the client prewrites the primary key and secondary key in parallel, it's possible + \* that the primary key lock is missing and also no commit or rollback record for the transaction + \* is found in the write CF, while there is a lock on the secondary key (so other transaction + \* is blocked, therefore this check_txn_status is sent). And there are two possible cases: + \* + \* 1. The prewrite request for the primary key has not reached yet. + \* 2. The client is crashed after sending the prewrite request for the secondary key. + \* + \* In order to address the first case, the client sending `check_txn_status` should not rollback + \* the primary key until the TTL on the secondary key is expired, and thus, `rollback_if_not_exist` + \* should be set to false before the TTL expires (and set true afterward). + \* + \* In TLA+ spec, the TTL is considered constantly expired when the action is taken, so the + \* `rollback_if_not_exist` is assumed true, thus no need to carry it in the message. + \union [start_ts : Ts, caller_start_ts : Ts \union {NoneTs}, primary : KEY, type : {"check_txn_status"}, + resolving_pessimistic_lock : BOOLEAN] + +\* In this spec, the responses from the server to the client are modeled differently from the requests. +\* A response is modeled as a direct call to client handling function which makes the client states and +\* the server states change in atomic. +\* +\* This is ok because, different from requests, which may be duplicated, delayed, or lost, the response +\* can only be lost or delayed. Every client handling function will have a branch that the response +\* is simply ignored, in order to simulate losing the response. Still, we can not simulate the delaying +\* situation, but the client should (we thing) be ok with the delayed response since the client only +\* handles the response at the matching stage (e.g. "reading", "locking", "prewriting"), and every +\* client handling function only changes the client state to one key and leaving the state to other keys +\* untouched, which makes the order of receiving the response to different keys is irrelevant. +\* +\* One more draw back is that, a delayed resent request to server may result in a call the client +\* handling function, which is impossible in real-world because the client must drop the previous +\* connection before retry, in other words, the client is only possible to recieve and to handle the +\* response to the request it last sent. We overcome this by checking whether the client is in the right +\* stage to handle the response. But still, the model will face to some response to the resent resquest +\* for the same client stage. However, the model has just been tested against more but no less cases +\* comparing to the real-world, and is still passing the check. +DirectRespMessages == + [start_ts : Ts, type : {"read_optimistic_succeed"}, key : KEY, value_ts : ValueTs] + \union [start_ts : Ts, type : {"lock_key_succeed"}, key : KEY, for_update_ts : Ts, value_ts : ValueTs] + \union [start_ts : Ts, type : {"key_is_locked"}, key : KEY, lock_primary: KEY, lock_ts : Ts] + \union [start_ts : Ts, type : {"lock_key_failed_write_conflict"}, key : KEY, latest_commit_ts : Ts] + \union [start_ts : Ts, type : {"prewrited"}, key : KEY] + \union [start_ts : Ts, type : {"commit_ts_expired"}, min_commit_ts : Ts] + +\* The responses defined in RespMessages will not be handled by the client in this spec, because they all +\* drive the transaction the an end. The messages defined here are used to record the history, in order to +\* check the invariants later defined in the spec (e.g. TiKV server should never has responded a transcation +\* committed while it has also responded the transaction aborted). +RespMessages == [start_ts : Ts, type : {"committed", + "commit_aborted", + "lock_key_aborted", + "prewrite_aborted"}] TypeOK == /\ req_msgs \in SUBSET ReqMessages /\ resp_msgs \in SUBSET RespMessages /\ key_data \in [KEY -> SUBSET Ts] - /\ key_lock \in [KEY -> SUBSET [ts : Ts, - primary : KEY, + /\ key_lock \in [KEY -> SUBSET [start_ts : Ts, + primary : KEY, + \* As defined above, Ts == Nat \ 0, here we use 0 + \* to indicates that there's no min_commit_ts limit + \* becuase every valid commit ts is larger than 0. + min_commit_ts : Ts \union {NoneTs}, type : {"prewrite_optimistic", "prewrite_pessimistic", "lock_key"}]] + /\ key_write \in [KEY -> SUBSET ( + [ts : Ts, start_ts : Ts, type : {"commit"}] + \union [ts : Ts, start_ts : Ts, type : {"rollback"}, protected : BOOLEAN])] \* At most one lock in key_lock[k] /\ \A k \in KEY: Cardinality(key_lock[k]) <= 1 - /\ key_write \in [KEY -> SUBSET ( - [ts : Ts, start_ts : Ts, type : {"write"}] - \union [ts : Ts, start_ts : Ts, type : {"rollback"}, protected : BOOLEAN])] - /\ client_state \in [CLIENT -> {"init", "locking", "prewriting", "committing"}] + /\ client_stage \in [CLIENT -> {"init", "reading", "locking", "prewriting", "committing"}] /\ client_ts \in [CLIENT -> [start_ts : Ts \union {NoneTs}, commit_ts : Ts \union {NoneTs}, for_update_ts : Ts \union {NoneTs}]] - /\ client_key \in [CLIENT -> [locking: SUBSET KEY, prewriting : SUBSET KEY]] + /\ client_key \in [CLIENT -> [reading : SUBSET KEY, locking : SUBSET KEY, prewriting : SUBSET KEY]] + /\ client_read \in [CLIENT -> [KEY -> + [type : {"not_read_yet"}] + \union [type : {"read_succeed"}, value_ts : ValueTs]]] + /\ \A c \in CLIENT: client_key[c].locking \intersect client_key[c].prewriting = {} /\ next_ts \in Ts ----------------------------------------------------------------------------- \* Client Actions -ClientLockKey(c) == - /\ client_state[c] = "init" - /\ client_state' = [client_state EXCEPT ![c] = "locking"] - /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts, ![c].for_update_ts = next_ts] +\* Once the get request is sent, it exist permanently in the req_msgs. +ClientReadOptimistic(c) == + /\ client_stage[c] = "init" + /\ client_stage' = [client_stage EXCEPT ![c] = "reading"] + /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts] + /\ client_key' = [client_key EXCEPT ![c].reading = CLIENT_READ_KEY[c]] /\ next_ts' = next_ts + 1 - \* Assume we need to acquire pessimistic locks for all keys - /\ client_key' = [client_key EXCEPT ![c].locking = CLIENT_KEY[c]] + /\ SendReqs({[type |-> "read_optimistic", + start_ts |-> client_ts'[c].start_ts, + primary |-> CLIENT_PRIMARY[c], + key |-> k] : k \in CLIENT_READ_KEY[c]}) + /\ UNCHANGED <> + +add_client_read_history(c, k, value_ts) == + client_read' = [client_read EXCEPT ![c][k] = [type |-> "read_succeed", value_ts |-> value_ts]] + +ClientReadOptimisticSucceed(resp) == + /\ Assert(resp.type = "read_optimistic_succeed", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + /\ client_stage[c] = "reading" + /\ resp.key \in client_key[c].reading + /\ client_key' = [client_key EXCEPT ![c].reading = @ \ {resp.key}] + /\ add_client_read_history(c, resp.key, resp.value_ts) + /\ UNCHANGED <> + +ClientResolveLock(resp) == + /\ Assert(resp.type = "key_is_locked", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + /\ client_stage[c] = "locking" + /\ resp.key \in client_key[c].locking + /\ SendReq([type |-> "check_txn_status", + start_ts |-> resp.lock_ts, + caller_start_ts |-> NoneTs, + primary |-> resp.lock_primary, + resolving_pessimistic_lock |-> resp.lock_type = "lock_key"]) + /\ UNCHANGED <> + +ClientLockKey(c) == + /\ client_stage[c] = "init" + /\ client_stage' = [client_stage EXCEPT ![c] = "locking"] + /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts, ![c].for_update_ts = next_ts] + /\ client_key' = [client_key EXCEPT ![c].locking = CLIENT_WRITE_KEY[c]] + /\ next_ts' = next_ts + 1 + \* For pessimistic clients assume we need to acquire pessimistic locks for all keys. /\ SendReqs({[type |-> "lock_key", start_ts |-> client_ts'[c].start_ts, primary |-> CLIENT_PRIMARY[c], key |-> k, - for_update_ts |-> client_ts'[c].for_update_ts] : k \in CLIENT_KEY[c]}) - /\ UNCHANGED <> + for_update_ts |-> client_ts'[c].for_update_ts] : k \in CLIENT_WRITE_KEY[c]}) + /\ UNCHANGED <> -ClientLockedKey(c) == - /\ client_state[c] = "locking" - /\ \E resp \in resp_msgs : - /\ resp.type = "locked_key" - /\ resp.start_ts = client_ts[c].start_ts - /\ resp.key \in client_key[c].locking - /\ client_key' = [client_key EXCEPT ![c].locking = @ \ {resp.key}] - /\ UNCHANGED <> +ClientLockKeySucceed(resp) == + /\ Assert(resp.type = "lock_key_succeed", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + \* The client guarantees that it will never recieve a response for + \* a previously sent lock_key request with smaller for_update_ts, which + \* may carry a bad value that breaks the snapshot isolation. This + \* guarantee holds because the previous gRPC connection must have closed. + /\ client_ts[c].for_update_ts = resp.for_update_ts + /\ client_stage[c] = "locking" + /\ resp.key \in client_key[c].locking + /\ client_key' = [client_key EXCEPT ![c].locking = @ \ {resp.key}] + /\ add_client_read_history(c, resp.key, resp.value_ts) + /\ UNCHANGED <> + +ClientLockKeyFailedWriteConflict(resp) == + /\ Assert(resp.type = "lock_key_failed_write_conflict", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + /\ client_stage[c] = "locking" + /\ resp.key \in client_key[c].locking + /\ resp.latest_commit_ts > client_ts[c].for_update_ts + /\ client_ts' = [client_ts EXCEPT ![c].for_update_ts = next_ts] + /\ next_ts' = next_ts + 1 + /\ SendReqs({[type |-> "lock_key", + start_ts |-> client_ts'[c].start_ts, + primary |-> CLIENT_PRIMARY[c], + key |-> resp.key, + for_update_ts |-> client_ts'[c].for_update_ts]}) + /\ UNCHANGED <> + +ClientPrewriteOptimistic(c) == + /\ client_stage[c] = "reading" + /\ client_key[c].reading = {} + /\ client_stage' = [client_stage EXCEPT ![c] = "prewriting"] + /\ client_key' = [client_key EXCEPT ![c].prewriting = CLIENT_WRITE_KEY[c]] + /\ SendReqs({[type |-> "prewrite_optimistic", + start_ts |-> client_ts[c].start_ts, + primary |-> CLIENT_PRIMARY[c], + key |-> k] : k \in CLIENT_WRITE_KEY[c]}) + /\ UNCHANGED <> -ClientRetryLockKey(c) == - /\ client_state[c] = "locking" - /\ \E resp \in resp_msgs : - /\ resp.type = "lock_failed" - /\ resp.start_ts = client_ts[c].start_ts - /\ resp.latest_commit_ts > client_ts[c].for_update_ts - /\ client_ts' = [client_ts EXCEPT ![c].for_update_ts = resp.latest_commit_ts] - /\ SendReqs({[type |-> "lock_key", - start_ts |-> client_ts'[c].start_ts, - primary |-> CLIENT_PRIMARY[c], - key |-> resp.key, - for_update_ts |-> client_ts'[c].for_update_ts]}) - /\ UNCHANGED <> - ClientPrewritePessimistic(c) == - /\ client_state[c] = "locking" + /\ client_stage[c] = "locking" /\ client_key[c].locking = {} - /\ client_state' = [client_state EXCEPT ![c] = "prewriting"] - /\ client_key' = [client_key EXCEPT ![c].prewriting = CLIENT_KEY[c]] + /\ client_stage' = [client_stage EXCEPT ![c] = "prewriting"] + /\ client_key' = [client_key EXCEPT ![c].prewriting = CLIENT_WRITE_KEY[c]] /\ SendReqs({[type |-> "prewrite_pessimistic", start_ts |-> client_ts[c].start_ts, primary |-> CLIENT_PRIMARY[c], - key |-> k] : k \in CLIENT_KEY[c]}) - /\ UNCHANGED <> + key |-> k] : k \in CLIENT_WRITE_KEY[c]}) + /\ UNCHANGED <> -ClientPrewriteOptimistic(c) == - /\ client_state[c] = "init" - /\ client_state' = [client_state EXCEPT ![c] = "prewriting"] - /\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts] - /\ next_ts' = next_ts + 1 - /\ client_key' = [client_key EXCEPT ![c].prewriting = CLIENT_KEY[c]] - /\ SendReqs({[type |-> "prewrite_optimistic", - start_ts |-> client_ts'[c].start_ts, - primary |-> CLIENT_PRIMARY[c], - key |-> k] : k \in CLIENT_KEY[c]}) - /\ UNCHANGED <> - -ClientPrewrited(c) == - /\ client_state[c] = "prewriting" - /\ client_key[c].locking = {} - /\ \E resp \in resp_msgs : - /\ resp.type = "prewrited" - /\ resp.start_ts = client_ts[c].start_ts - /\ resp.key \in client_key[c].prewriting - /\ client_key' = [client_key EXCEPT ![c].prewriting = @ \ {resp.key}] - /\ UNCHANGED <> +ClientPrewrited(resp) == + /\ Assert(resp.type = "prewrited", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + /\ client_stage[c] = "prewriting" + /\ resp.key \in client_key[c].prewriting + /\ client_key' = [client_key EXCEPT ![c].prewriting = @ \ {resp.key}] + /\ UNCHANGED <> ClientCommit(c) == - /\ client_state[c] = "prewriting" + /\ client_stage[c] = "prewriting" /\ client_key[c].prewriting = {} - /\ client_state' = [client_state EXCEPT ![c] = "committing"] + /\ client_stage' = [client_stage EXCEPT ![c] = "committing"] /\ client_ts' = [client_ts EXCEPT ![c].commit_ts = next_ts] /\ next_ts' = next_ts + 1 /\ SendReqs({[type |-> "commit", - start_ts |-> client_ts'[c].start_ts, - primary |-> CLIENT_PRIMARY[c], - commit_ts |-> client_ts'[c].commit_ts]}) - /\ UNCHANGED <> + start_ts |-> client_ts'[c].start_ts, + primary |-> CLIENT_PRIMARY[c], + commit_ts |-> client_ts'[c].commit_ts]}) + /\ UNCHANGED <> + +ClientRetryCommit(resp) == + /\ Assert(resp.type = "commit_ts_expired", "Message Type Error") + /\ \/ UNCHANGED <> + \/ \E c \in CLIENT: + /\ client_ts[c].start_ts = resp.start_ts + /\ client_stage[c] = "commiting" + /\ client_ts[c].commit_ts < resp.min_commit_ts + /\ client_ts' = [client_ts EXCEPT ![c].commit_ts = next_ts] + /\ next_ts' = next_ts + 1 + /\ SendReqs({[type |-> "commit", + start_ts |-> client_ts'[c].start_ts, + primary |-> CLIENT_PRIMARY[c], + commit_ts |-> client_ts'[c].commit_ts]}) + /\ UNCHANGED <> ----------------------------------------------------------------------------- \* Server Actions \* Write the write column and unlock the lock iff the lock exists. +unlock_key(k) == + /\ key_lock' = [key_lock EXCEPT ![k] = {}] + commit(pk, start_ts, commit_ts) == \E l \in key_lock[pk] : - /\ l.ts = start_ts - /\ key_lock' = [key_lock EXCEPT ![pk] = {}] + /\ l.start_ts = start_ts + /\ unlock_key(pk) /\ key_write' = [key_write EXCEPT ![pk] = @ \union {[ts |-> commit_ts, - type |-> "write", + type |-> "commit", start_ts |-> start_ts]}] \* Rollback the transaction that starts at start_ts on key k. rollback(k, start_ts) == LET \* Rollback record on the primary key of a pessimistic transaction - \* needs to be protected from being collapsed. If we can't decide - \* whether it suffices that because the lock is missing or mismatched, - \* it should also be protected. - protected == \/ \E l \in key_lock[k] : - /\ l.ts = start_ts - /\ l.primary = k - /\ l.type \in {"lock_key", "prewrite_pessimistic"} - \/ \E l \in key_lock[k] : l.ts /= start_ts - \/ key_lock[k] = {} + \* needs to be protected from being collapsed. + protected == \E l \in key_lock[k] : + /\ l.start_ts = start_ts + /\ l.primary = k + /\ l.type \in {"lock_key", "prewrite_pessimistic"} IN \* If a lock exists and has the same ts, unlock it. - /\ IF \E l \in key_lock[k] : l.ts = start_ts - THEN key_lock' = [key_lock EXCEPT ![k] = {}] + /\ IF \E l \in key_lock[k]: l.start_ts = start_ts + THEN unlock_key(k) ELSE UNCHANGED key_lock /\ key_data' = [key_data EXCEPT ![k] = @ \ {start_ts}] - /\ IF - /\ ~ \E w \in key_write[k]: w.ts = start_ts + /\ IF ~ \E w \in key_write[k]: w.ts = start_ts THEN key_write' = [key_write EXCEPT - ![k] = + ![k] = \* collapse rollback - (@ \ {w \in @ : w.type = "rollback" /\ ~w.protected /\ w.ts < start_ts}) + (@ \ {w \in @: w.type = "rollback" /\ ~ w.protected /\ w.ts < start_ts}) \* write rollback record \union {[ts |-> start_ts, start_ts |-> start_ts, @@ -261,50 +398,183 @@ rollback(k, start_ts) == ELSE UNCHANGED <> +\* In optimistic transaction, read_ts is start_ts, and, in pessimistic transaction, +\* read_ts is for_update_ts. +find_readable_commit(k, read_ts) == + LET + all_commits_before_read_ts == {w \in key_write[k]: w.type = "commit" /\ w.ts <= read_ts} + latest_commit_before_read_ts == + {w \in all_commits_before_read_ts : + \A w2 \in all_commits_before_read_ts : + w.ts >= w2.ts} + IN + latest_commit_before_read_ts + +\* Optimistic read successfully. Return `value_ts = NoneTs` if the value is empty. +respond_read_succeed(k, start_ts) == + LET + readable_commit == find_readable_commit(k, start_ts) + IN + \/ /\ readable_commit = {} + /\ ClientReadOptimisticSucceed([start_ts |-> start_ts, + type |-> "read_optimistic_succeed", + key |-> k, + value_ts |-> NoneTs]) + \/ \E committed_record \in readable_commit: + /\ ClientReadOptimisticSucceed([start_ts |-> start_ts, + type |-> "read_optimistic_succeed", + key |-> k, + value_ts |-> committed_record.ts]) + +\* Pessimistic lock successfully. Return `value_ts = NoneTs` if the value is empty. +respond_lock_key_succeed(k, start_ts, for_update_ts) == + LET + readable_commit == find_readable_commit(k, for_update_ts) + IN + \/ /\ readable_commit = {} + /\ ClientLockKeySucceed([start_ts |-> start_ts, + type |-> "lock_key_succeed", + key |-> k, + for_update_ts |-> for_update_ts, + value_ts |-> NoneTs]) + \/ \E committed_record \in readable_commit: + /\ ClientLockKeySucceed([start_ts |-> start_ts, + type |-> "lock_key_succeed", + key |-> k, + for_update_ts |-> for_update_ts, + value_ts |-> committed_record.ts]) + +ServerReadKey == + \E req \in req_msgs : + /\ req.type = "read_optimistic" + /\ \E c \in CLIENT : + /\ client_ts[c].start_ts = req.start_ts + /\ LET + k == req.key + start_ts == req.start_ts + IN + \* If the lock belongs to the transaction sending the request, or + \* if it's a pessimistic lock, return read succeed. + \* + \* The reason why pessimistic lock will not block the read is that + \* the owner transaction of the pessimistic lock is impossible to + \* commit the key with a commit_ts smaller than req.start_ts because + \* the owner transaction must get commit_ts after all prewrites have + \* completed which is apperently not done since the lock type is + \* not a prewrite lock. + /\ IF \/ key_lock[k] = {} + \/ \E l \in key_lock[k]: l.type = "lock_key" \/ l.start_ts = start_ts + THEN + /\ respond_read_succeed(k, start_ts) + /\ UNCHANGED <> + ELSE + \E l \in key_lock[k]: + /\ ClientResolveLock([start_ts |-> start_ts, + type |-> "key_is_locked", + key |-> k, + lock_primary |-> l.primary, + lock_ts |-> l.start_ts]) + /\ UNCHANGED <> + ServerLockKey == \E req \in req_msgs : /\ req.type = "lock_key" /\ LET k == req.key start_ts == req.start_ts + for_update_ts == req.for_update_ts IN - \* Pessimistic lock is allowed only if no stale lock exists. If - \* there is one, wait until ServerCleanupStaleLock to clean it up. - /\ key_lock[k] = {} - /\ LET - latest_write == {w \in key_write[k] : \A w2 \in key_write[k] : w.ts >= w2.ts} - - all_commits == {w \in key_write[k] : w.type = "write"} - latest_commit == {w \in all_commits : \A w2 \in all_commits : w.ts >= w2.ts} - IN - IF \E w \in key_write[k] : w.start_ts = start_ts /\ w.type = "rollback" - THEN - \* If corresponding rollback record is found, which - \* indicates that the transcation is rollbacked, abort the - \* transaction. - /\ SendResp([start_ts |-> start_ts, type |-> "lock_key_aborted"]) + \* Pessimistic lock is allowed only if no stale lock exists. If + \* there is one, wait until ClientCheckTxnStatus to clean it up. + \/ /\ key_lock[k] = {} + /\ LET + all_commits == {w \in key_write[k]: w.type = "commit"} + latest_commit == {w \in all_commits: \A w2 \in all_commits: w.ts >= w2.ts} + IN + IF \E w \in key_write[k]: w.start_ts = start_ts /\ w.type = "rollback" + THEN + \* If corresponding rollback record is found, which + \* indicates that the transcation is rollbacked, abort the + \* transaction. + /\ SendResp([start_ts |-> start_ts, type |-> "lock_key_aborted"]) + /\ UNCHANGED <> + ELSE + \* Acquire pessimistic lock only if for_update_ts of req + \* is greater or equal to the latest "commit" record. + \* Because if the latest record is "commit", it means that + \* a new version is committed after for_update_ts, which + \* violates Read Committed guarantee. + \/ /\ ~ \E w \in latest_commit: w.ts > req.for_update_ts + /\ key_lock' = [key_lock EXCEPT ![k] = {[start_ts |-> start_ts, + primary |-> req.primary, + min_commit_ts |-> NoneTs, + type |-> "lock_key"]}] + /\ respond_lock_key_succeed(k, start_ts, for_update_ts) + /\ UNCHANGED <> + \* Otherwise, reject the request and let client to retry + \* with new for_update_ts. + \/ \E w \in latest_commit : + /\ w.ts > req.for_update_ts + /\ ~ \E w2 \in all_commits: w2.start_ts = req.start_ts + /\ ClientLockKeyFailedWriteConflict([start_ts |-> start_ts, + type |-> "lock_key_failed_write_conflict", + key |-> k, + latest_commit_ts |-> w.ts]) + /\ UNCHANGED <> + \* Lock exsits + \/ \E l \in key_lock[k]: + IF l.start_ts = start_ts + THEN + /\ respond_lock_key_succeed(k, start_ts, for_update_ts) + /\ UNCHANGED <> + ELSE + /\ ClientResolveLock([start_ts |-> start_ts, + type |-> "key_is_locked", + key |-> k, + lock_primary |-> l.primary, + lock_ts |-> l.start_ts, + lock_type |-> l.type]) + /\ UNCHANGED <> + +ServerPrewriteOptimistic == + \E req \in req_msgs: + /\ req.type = "prewrite_optimistic" + /\ LET + k == req.key + start_ts == req.start_ts + IN + \/ /\ key_lock[k] = {} + /\ IF \E w \in key_write[k]: w.start_ts = start_ts /\ w.type = "commit" THEN + \* This is a duplicated prewrite request. + UNCHANGED <> + ELSE IF \/ \E w \in key_write[k]: w.start_ts = start_ts /\ w.type = "rollback" + \/ \E w \in key_write[k]: w.ts >= start_ts THEN + \* This transacstion has been rollbacked or has write conflict. + /\ SendResp([start_ts |-> start_ts, type |-> "prewrite_aborted"]) /\ UNCHANGED <> ELSE - \* Acquire pessimistic lock only if for_update_ts of req - \* is greater or equal to the latest "write" record. - \* Because if the latest record is "write", it means that - \* a new version is committed after for_update_ts, which - \* violates Read Committed guarantee. - \/ /\ ~ \E w \in latest_commit : w.ts > req.for_update_ts - /\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> start_ts, - primary |-> req.primary, - type |-> "lock_key"]}] - /\ SendResp([start_ts |-> start_ts, type |-> "locked_key", key |-> k]) - /\ UNCHANGED <> - \* Otherwise, reject the request and let client to retry - \* with new for_update_ts. - \/ \E w \in latest_commit : - /\ w.ts > req.for_update_ts - /\ SendResp([start_ts |-> start_ts, - type |-> "lock_failed", - key |-> k, - latest_commit_ts |-> w.ts]) - /\ UNCHANGED <> + \* Prewrite the key. + /\ key_lock' = [key_lock EXCEPT ![k] = {[start_ts |-> start_ts, + primary |-> req.primary, + type |-> "prewrite_optimistic", + min_commit_ts |-> NoneTs]}] + /\ key_data' = [key_data EXCEPT ![k] = @ \union {start_ts}] + /\ ClientPrewrited([start_ts |-> start_ts, type |-> "prewrited", key |-> k]) + /\ UNCHANGED <> + \/ \E l \in key_lock[k]: + IF l.start_ts = start_ts + THEN + /\ ClientPrewrited([start_ts |-> start_ts, type |-> "prewrited", key |-> k]) + /\ UNCHANGED <> + ELSE + \* Clean up the stale lock. + /\ ClientResolveLock([start_ts |-> start_ts, + type |-> "key_is_locked", + key |-> k, + lock_primary |-> l.primary, + lock_ts |-> l.start_ts, + lock_type |-> l.type]) + /\ UNCHANGED <> ServerPrewritePessimistic == \E req \in req_msgs : @@ -313,104 +583,136 @@ ServerPrewritePessimistic == k == req.key start_ts == req.start_ts IN - \* Pessimistic prewrite is allowed only if pressimistic lock is - \* acquired, otherwise abort the transaction. - /\ IF \E l \in key_lock[k] : l.ts = start_ts - THEN - /\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> start_ts, - primary |-> req.primary, - type |-> "prewrite_pessimistic"]}] - /\ key_data' = [key_data EXCEPT ![k] = @ \union {start_ts}] - /\ SendResp([start_ts |-> start_ts, type |-> "prewrited", key |-> k]) - /\ UNCHANGED <> - ELSE - /\ SendResp([start_ts |-> start_ts, type |-> "prewrite_aborted"]) - /\ UNCHANGED <> - -ServerPrewriteOptimistic == - \E req \in req_msgs : - /\ req.type = "prewrite_optimistic" - /\ LET - k == req.key - start_ts == req.start_ts - IN - /\ IF \E w \in key_write[k] : w.ts >= start_ts - THEN - /\ SendResp([start_ts |-> start_ts, type |-> "prewrite_aborted"]) - /\ UNCHANGED <> - ELSE - \* Optimistic prewrite is allowed only if no stale lock exists. If - \* there is one, wait until ServerCleanupStaleLock to clean it up. - /\ \/ key_lock[k] = {} - \/ \E l \in key_lock[k] : l.ts = start_ts - /\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> start_ts, - primary |-> req.primary, - type |-> "prewrite_optimistic"]}] - /\ key_data' = [key_data EXCEPT ![k] = @ \union {start_ts}] - /\ SendResp([start_ts |-> start_ts, type |-> "prewrited", key |-> k]) - /\ UNCHANGED <> + \* Pessimistic prewrite is only allowed if pressimistic lock is + \* acquired, or, if there's no lock, and no write record whose + \* commit_ts >= start_ts, otherwise abort the transaction. + IF + \/ \E l \in key_lock[k] : + /\ l.start_ts = start_ts + /\ l.type = "lock_key" + \/ /\ key_lock[k] = {} + /\ ~ \E w \in key_write[k]: w.ts >= start_ts + THEN + /\ key_lock' = [key_lock EXCEPT ![k] = {[start_ts |-> start_ts, + primary |-> req.primary, + type |-> "prewrite_pessimistic", + min_commit_ts |-> NoneTs]}] + /\ key_data' = [key_data EXCEPT ![k] = @ \union {start_ts}] + /\ ClientPrewrited([start_ts |-> start_ts, type |-> "prewrited", key |-> k]) + /\ UNCHANGED <> + ELSE + /\ SendResp([start_ts |-> start_ts, type |-> "prewrite_aborted"]) + /\ UNCHANGED <> ServerCommit == - \E req \in req_msgs : + \E req \in req_msgs: /\ req.type = "commit" /\ LET pk == req.primary start_ts == req.start_ts IN - IF \E w \in key_write[pk] : w.start_ts = start_ts /\ w.type = "write" + IF \E w \in key_write[pk]: w.start_ts = start_ts /\ w.type = "commit" THEN - \* Key has already been committed. Do nothing. + \* Key has already been committed. Do nothing. /\ SendResp([start_ts |-> start_ts, type |-> "committed"]) /\ UNCHANGED <> ELSE - IF \E l \in key_lock[pk] : l.ts = start_ts - THEN - \* Commit the key only if the prewrite lock exists. - /\ commit(pk, start_ts, req.commit_ts) - /\ SendResp([start_ts |-> start_ts, type |-> "committed"]) - /\ UNCHANGED <> - ELSE - \* Otherwise, abort the transaction. - /\ SendResp([start_ts |-> start_ts, type |-> "commit_aborted"]) - /\ UNCHANGED <> + \/ \E l \in key_lock[pk]: + IF l.start_ts = start_ts /\ ~ l.type = "lock_key" + THEN + IF req.commit_ts >= l.min_commit_ts + THEN + \* Commit the key only if the prewrite lock exists and commit_ts is greater than + \* the min_commit_ts in the prewrite lock. + /\ commit(pk, start_ts, req.commit_ts) + /\ SendResp([start_ts |-> start_ts, type |-> "committed"]) + /\ UNCHANGED <> + ELSE + /\ ClientRetryCommit([start_ts |-> start_ts, + type |-> "commit_ts_expired", + min_commit_ts |-> l.min_commit_ts]) + /\ UNCHANGED <> + ELSE + /\ SendResp([start_ts |-> start_ts, type |-> "commit_aborted"]) + /\ UNCHANGED <> + \/ /\ key_lock[pk] = {} + /\ SendResp([start_ts |-> start_ts, type |-> "commit_aborted"]) + /\ UNCHANGED <> -\* In the spec, the primary key with a lock may clean up itself -\* spontaneously. There is no need to model a client to request clean up -\* because there is no difference between a optimistic client trying to -\* read a key that has lock timeouted and the key trying to unlock itself. -ServerCleanupStaleLock == - \E k \in KEY : - \E l \in key_lock[k] : - /\ SendReqs({[type |-> "cleanup", - start_ts |-> l.ts, - primary |-> l.primary]}) +\* Found the matching lock. +check_txn_status_has_lock(lock, caller_start_ts, resolving_pessimistic_lock) == + LET + start_ts == lock.start_ts + pk == lock.primary + IN + \/ IF lock.type = "lock_key" /\ resolving_pessimistic_lock + THEN + \* Pessimistic lock will be unlocked directly without rollback record. + /\ unlock_key(pk) + /\ UNCHANGED <> + ELSE + /\ rollback(pk, start_ts) + /\ SendReqs({[type |-> "resolve_rollbacked", + start_ts |-> start_ts, + primary |-> pk]}) + /\ UNCHANGED <> + \/ + \* Push min_commit_ts. + /\ lock.min_commit_ts <= caller_start_ts + /\ key_lock' = [key_lock EXCEPT ![pk] = {[start_ts |-> lock.start_ts, + type |-> lock.type, + primary |-> lock.primary, + min_commit_ts |-> caller_start_ts + 1]}] + /\ UNCHANGED <> + +\* Lock not found or start_ts on the lock mismatches. +check_txn_status_missing_lock(start_ts, pk, resolving_pessimistic_lock) == + LET + committed_record == {w \in key_write[pk]: w.start_ts = start_ts /\ w.type = "commit"} + IN + IF committed_record /= {} THEN + /\ SendReqs({[type |-> "resolve_committed", + start_ts |-> start_ts, + primary |-> pk, + commit_ts |-> w.ts]: w \in committed_record}) /\ UNCHANGED <> + ELSE IF resolving_pessimistic_lock = TRUE THEN + UNCHANGED <> + ELSE + /\ rollback(pk, start_ts) + /\ SendReqs({[type |-> "resolve_rollbacked", + start_ts |-> start_ts, + primary |-> pk]}) + /\ UNCHANGED <> -\* Clean up stale locks by checking the status of the primary key. Commmit -\* the secondary keys if primary key is committed; otherwise rollback the -\* transaction by rolling-back the primary key, and then also rollback the -\* secondarys. -ServerCleanup == +\* Clean up the stale transaction by checking the status of the primary key. +\* +\* In practice, the transaction will be rolled back only if TTL on the lock is expired. But +\* because it is hard to model the TTL in TLA+ spec, the TTL is considered constantly expired +\* when ServerCheckTxnStatus is called. +\* +\* Moreover, TiKV will send a response `TxnStatus` to the client, and depending on the `TxnStatus` +\* the client will send `resolve_rollback` or `resolve_commit` to the secondary keys to clean up +\* stale locks on secondary keys. In the TLA+ spec, ServerCheckTxnStatus will not respond to the +\* client and instead TiKV will directly send `resolve_rollback` or `resolve_commit` message to +\* the server where the secondary keys are on, because the action of client sending resolve message +\* by proxying the `TxnStatus` from TiKV to other TiKV does not change the state of the client, +\* therefore is equal to directly sending resolve message from TiKV to TiKV directly. +ServerCheckTxnStatus == \E req \in req_msgs : - /\ req.type = "cleanup" + /\ req.type = "check_txn_status" /\ LET - pk == req.primary - start_ts == req.start_ts - committed == {w \in key_write[pk] : w.start_ts = start_ts /\ w.type = "write"} + pk == req.primary + start_ts == req.start_ts IN - IF committed /= {} - THEN - /\ SendReqs({[type |-> "resolve_committed", - start_ts |-> start_ts, - primary |-> pk, - commit_ts |-> w.ts] : w \in committed}) - /\ UNCHANGED <> - ELSE - /\ rollback(pk, start_ts) - /\ SendReqs({[type |-> "resolve_rollbacked", - start_ts |-> start_ts, - primary |-> pk]}) - /\ UNCHANGED <> + \/ \E l \in key_lock[pk]: + IF start_ts = l.start_ts + THEN + check_txn_status_has_lock(l, req.caller_start_ts, req.resolving_pessimistic_lock) + ELSE + check_txn_status_missing_lock(start_ts, pk, req.resolving_pessimistic_lock) + \/ /\ key_lock[pk] = {} + /\ check_txn_status_missing_lock(start_ts, pk, req.resolving_pessimistic_lock) ServerResolveCommitted == \E req \in req_msgs : @@ -421,7 +723,7 @@ ServerResolveCommitted == \E k \in KEY: \E l \in key_lock[k] : /\ l.primary = req.primary - /\ l.ts = start_ts + /\ l.start_ts = start_ts /\ commit(k, start_ts, req.commit_ts) /\ UNCHANGED <> @@ -434,43 +736,41 @@ ServerResolveRollbacked == \E k \in KEY: \E l \in key_lock[k] : /\ l.primary = req.primary - /\ l.ts = start_ts + /\ l.start_ts = start_ts /\ rollback(k, start_ts) /\ UNCHANGED <> ----------------------------------------------------------------------------- \* Specification -Init == +Init == /\ next_ts = 1 /\ req_msgs = {} /\ resp_msgs = {} - /\ client_state = [c \in CLIENT |-> "init"] - /\ client_key = [c \in CLIENT |-> [locking |-> {}, prewriting |-> {}]] + /\ client_stage = [c \in CLIENT |-> "init"] + /\ client_key = [c \in CLIENT |-> [reading |-> {}, locking |-> {}, prewriting |-> {}]] /\ client_ts = [c \in CLIENT |-> [start_ts |-> NoneTs, commit_ts |-> NoneTs, for_update_ts |-> NoneTs]] + /\ client_read = [c \in CLIENT |-> [k \in KEY |-> [type |-> "not_read_yet"]]] /\ key_lock = [k \in KEY |-> {}] /\ key_data = [k \in KEY |-> {}] /\ key_write = [k \in KEY |-> {}] Next == - \/ \E c \in OPTIMISTIC_CLIENT : - \/ ClientPrewriteOptimistic(c) - \/ ClientPrewrited(c) - \/ ClientCommit(c) - \/ \E c \in PESSIMISTIC_CLIENT : - \/ ClientLockKey(c) - \/ ClientLockedKey(c) - \/ ClientRetryLockKey(c) - \/ ClientPrewritePessimistic(c) - \/ ClientPrewrited(c) - \/ ClientCommit(c) + \/ \E c \in OPTIMISTIC_CLIENT: + \/ ClientReadOptimistic(c) + \/ ClientPrewriteOptimistic(c) + \/ ClientCommit(c) + \/ \E c \in PESSIMISTIC_CLIENT: + \/ ClientLockKey(c) + \/ ClientPrewritePessimistic(c) + \/ ClientCommit(c) + \/ ServerReadKey \/ ServerLockKey \/ ServerPrewritePessimistic \/ ServerPrewriteOptimistic \/ ServerCommit - \/ ServerCleanupStaleLock - \/ ServerCleanup + \/ ServerCheckTxnStatus \/ ServerResolveCommitted \/ ServerResolveRollbacked @@ -478,12 +778,12 @@ Spec == Init /\ [][Next]_vars ----------------------------------------------------------------------------- \* Consistency Invariants -\* Check whether there is a "write" record in key_write[k] corresponding +\* Check whether there is a "commit" record in key_write[k] corresponding \* to start_ts. keyCommitted(k, start_ts) == - \E w \in key_write[k] : + \E w \in key_write[k] : /\ w.start_ts = start_ts - /\ w.type = "write" + /\ w.type = "commit" \* A transaction can't be both committed and aborted. UniqueCommitOrAbort == @@ -503,11 +803,11 @@ CommitConsistency == /\ keyCommitted(CLIENT_PRIMARY[c], resp.start_ts) \* Secondary key must be either committed or locked by the \* start_ts of the transaction. - /\ \A k \in CLIENT_KEY[c] : - (~ \E l \in key_lock[k] : l.ts = resp.start_ts) = + /\ \A k \in CLIENT_WRITE_KEY[c] : + (~ \E l \in key_lock[k]: l.start_ts = resp.start_ts) = keyCommitted(k, resp.start_ts) -\* If a transaction is aborted, all key of that transaction must be not +\* If a transaction is aborted, all key of that transaction must not be \* committed. AbortConsistency == \A resp \in resp_msgs : @@ -517,12 +817,12 @@ AbortConsistency == ~ keyCommitted(CLIENT_PRIMARY[c], resp.start_ts) \* For each write, the commit_ts should be strictly greater than the -\* start_ts and have data written into key_data[k]. For each rollback, +\* start_ts and have data written into key_data[k]. For each rollback, \* the commit_ts should equals to the start_ts. WriteConsistency == \A k \in KEY : \A w \in key_write[k] : - \/ /\ w.type = "write" + \/ /\ w.type = "commit" /\ w.ts > w.start_ts /\ w.start_ts \in key_data[k] \/ /\ w.type = "rollback" @@ -534,7 +834,7 @@ UniqueLockOrWrite == \A k \in KEY : \A l \in key_lock[k] : \A w \in key_write[k] : - w.start_ts /= l.ts + w.start_ts /= l.start_ts \* For each key, ecah record in write column should have a unique start_ts. UniqueWrite == @@ -544,40 +844,38 @@ UniqueWrite == ----------------------------------------------------------------------------- \* Snapshot Isolation -\* Asserts that next_ts is monotonically increasing. -NextTsMonotonicity == [][next_ts' >= next_ts]_vars - -\* Asserts that no msg would be deleted once sent. -MsgMonotonicity == - /\ [][\A req \in req_msgs : req \in req_msgs']_vars - /\ [][\A resp \in resp_msgs : resp \in resp_msgs']_vars - \* Asserts that all messages sent should have ts less than next_ts. MsgTsConsistency == /\ \A req \in req_msgs : /\ req.start_ts <= next_ts /\ req.type \in {"commit", "resolve_committed"} => req.commit_ts <= next_ts - /\ \A resp \in resp_msgs : resp.start_ts <= next_ts + /\ \A resp \in resp_msgs: resp.start_ts <= next_ts -\* SnapshotIsolation is implied from the following assumptions (but is not -\* necessary) because SnapshotIsolation means that: -\* (1) Once a transaction is committed, all keys of the transaction should -\* be always readable or have a lock on secondary keys(eventually readable). -\* PROOF BY CommitConsistency, MsgMonotonicity -\* (2) For a given transaction, all transaction that commits after that -\* transaction should have greater commit_ts than the next_ts at the -\* time that the given transaction commits, so as to be able to -\* distinguish the transactions that have committed before and after -\* from all transactions that preserved by (1). -\* PROOF BY NextTsConsistency, MsgTsConsistency -\* (3) All aborted transactions would be always not readable. -\* PROOF BY AbortConsistency, MsgMonotonicity -SnapshotIsolation == /\ CommitConsistency - /\ AbortConsistency - /\ NextTsMonotonicity - /\ MsgMonotonicity - /\ MsgTsConsistency +OptimisticReadSnapshotIsolation == + \A c \in OPTIMISTIC_CLIENT: + \A k \in CLIENT_READ_KEY[c]: + client_read[c][k].type = "read_succeed" => + LET + readable_commit == find_readable_commit(k, client_ts[c].start_ts) + IN + \/ /\ readable_commit = {} + /\ client_read[c][k].value_ts = NoneTs + \/ \E committed_record \in readable_commit: + client_read[c][k].value_ts = committed_record.ts + +PessimisticReadSnapshotIsolation == + \A c \in PESSIMISTIC_CLIENT: + (\E resp \in resp_msgs: resp.start_ts = client_ts[c].start_ts /\ resp.type = "committed") => + \A k \in CLIENT_WRITE_KEY[c]: + client_read[c][k].type = "read_succeed" => + LET + readable_commit == find_readable_commit(k, client_ts[c].for_update_ts) + IN + \/ /\ readable_commit = {} + /\ client_read[c][k].value_ts = NoneTs + \/ \E committed_record \in readable_commit: + client_read[c][k].value_ts = committed_record.ts ----------------------------------------------------------------------------- THEOREM Safety == Spec => [](/\ TypeOK @@ -587,5 +885,7 @@ THEOREM Safety == /\ WriteConsistency /\ UniqueLockOrWrite /\ UniqueWrite - /\ SnapshotIsolation) + /\ OptimisticReadSnapshotIsolation + /\ PessimisticReadSnapshotIsolation + /\ MsgTsConsistency) ============================================================================= diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch index aec9d79..a609b01 100644 --- a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch @@ -1,60 +1,62 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch index 3e2e636..33d94a0 100644 --- a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch @@ -1,42 +1,60 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test3.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test3.launch new file mode 100644 index 0000000..5f533fb --- /dev/null +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test3.launch @@ -0,0 +1,60 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test4.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test4.launch new file mode 100644 index 0000000..779d76d --- /dev/null +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test4.launch @@ -0,0 +1,65 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/Test1.cfg b/DistributedTransaction/Test1.cfg index 93f0ac2..9ac3a63 100644 --- a/DistributedTransaction/Test1.cfg +++ b/DistributedTransaction/Test1.cfg @@ -6,10 +6,11 @@ CONSTANT c3 = c3 CONSTANT - KEY <- Key + KEY <- Keys OPTIMISTIC_CLIENT <- OptimistiicClient PESSIMISTIC_CLIENT <- PessimisticClient - CLIENT_KEY <- ClientKey + CLIENT_READ_KEY <- ClientReadKeys + CLIENT_WRITE_KEY <- ClientWriteKeys CLIENT_PRIMARY <- ClientPrimary INIT @@ -26,4 +27,6 @@ INVARIANT WriteConsistency UniqueLockOrWrite UniqueWrite + OptimisticReadSnapshotIsolation + PessimisticReadSnapshotIsolation MsgTsConsistency diff --git a/DistributedTransaction/Test1.tla b/DistributedTransaction/Test1.tla index d267bbd..1b8f5ea 100644 --- a/DistributedTransaction/Test1.tla +++ b/DistributedTransaction/Test1.tla @@ -4,9 +4,10 @@ EXTENDS DistributedTransaction, TLC CONSTANT k1, k2 CONSTANT c1, c2, c3 -Key == {k1, k2} +Keys == {k1, k2} OptimistiicClient == {c3} PessimisticClient == {c1, c2} -ClientKey == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k1, k2} +ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k2} +ClientWriteKeys == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k1, k2} ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k2 ================================================================================ diff --git a/DistributedTransaction/Test2.cfg b/DistributedTransaction/Test2.cfg index 1473b5d..0949218 100644 --- a/DistributedTransaction/Test2.cfg +++ b/DistributedTransaction/Test2.cfg @@ -7,10 +7,11 @@ CONSTANT c3 = c3 CONSTANT - KEY <- Key + KEY <- Keys OPTIMISTIC_CLIENT <- OptimistiicClient PESSIMISTIC_CLIENT <- PessimisticClient - CLIENT_KEY <- ClientKey + CLIENT_READ_KEY <- ClientReadKeys + CLIENT_WRITE_KEY <- ClientWriteKeys CLIENT_PRIMARY <- ClientPrimary INIT @@ -27,4 +28,6 @@ INVARIANT WriteConsistency UniqueLockOrWrite UniqueWrite + OptimisticReadSnapshotIsolation + PessimisticReadSnapshotIsolation MsgTsConsistency diff --git a/DistributedTransaction/Test2.tla b/DistributedTransaction/Test2.tla index f36a89e..e31dd23 100644 --- a/DistributedTransaction/Test2.tla +++ b/DistributedTransaction/Test2.tla @@ -4,9 +4,10 @@ EXTENDS DistributedTransaction, TLC CONSTANT k1, k2, k3 CONSTANT c1, c2, c3 -Key == {k1, k2, k3} +Keys == {k1, k2, k3} OptimistiicClient == {c3} PessimisticClient == {c1, c2} -ClientKey == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3} +ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3} +ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3} ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3 ================================================================================ diff --git a/DistributedTransaction/Test3.cfg b/DistributedTransaction/Test3.cfg new file mode 100644 index 0000000..9ec8364 --- /dev/null +++ b/DistributedTransaction/Test3.cfg @@ -0,0 +1,31 @@ +CONSTANT + k1 = k1 + k2 = k2 + c1 = c1 + c2 = c2 + +CONSTANT + KEY <- Keys + OPTIMISTIC_CLIENT <- OptimistiicClient + PESSIMISTIC_CLIENT <- PessimisticClient + CLIENT_READ_KEY <- ClientReadKeys + CLIENT_WRITE_KEY <- ClientWriteKeys + CLIENT_PRIMARY <- ClientPrimary + +INIT + Init + +NEXT + Next + +INVARIANT + TypeOK + UniqueCommitOrAbort + CommitConsistency + AbortConsistency + WriteConsistency + UniqueLockOrWrite + UniqueWrite + OptimisticReadSnapshotIsolation + PessimisticReadSnapshotIsolation + MsgTsConsistency diff --git a/DistributedTransaction/Test3.tla b/DistributedTransaction/Test3.tla new file mode 100644 index 0000000..f9ba94b --- /dev/null +++ b/DistributedTransaction/Test3.tla @@ -0,0 +1,13 @@ +--------------------------------- MODULE Test3 --------------------------------- +EXTENDS DistributedTransaction, TLC + +CONSTANT k1, k2 +CONSTANT c1, c2 + +Keys == {k1, k2} +OptimistiicClient == {c2} +PessimisticClient == {c1} +ClientReadKeys == c1 :> {} @@ c2 :> {k1, k2} +ClientWriteKeys == c1 :> {k1, k2} @@ c2 :> {k1, k2} +ClientPrimary == c1 :> k1 @@ c2 :> k1 +================================================================================ diff --git a/DistributedTransaction/Test4.cfg b/DistributedTransaction/Test4.cfg new file mode 100644 index 0000000..fff2207 --- /dev/null +++ b/DistributedTransaction/Test4.cfg @@ -0,0 +1,30 @@ +CONSTANT + k1 = k1 + c1 = c1 + c2 = c2 + +CONSTANT + KEY <- Keys + OPTIMISTIC_CLIENT <- OptimistiicClient + PESSIMISTIC_CLIENT <- PessimisticClient + CLIENT_READ_KEY <- ClientReadKeys + CLIENT_WRITE_KEY <- ClientWriteKeys + CLIENT_PRIMARY <- ClientPrimary + +INIT + Init + +NEXT + Next + +INVARIANT + TypeOK + UniqueCommitOrAbort + CommitConsistency + AbortConsistency + WriteConsistency + UniqueLockOrWrite + UniqueWrite + OptimisticReadSnapshotIsolation + PessimisticReadSnapshotIsolation + MsgTsConsistency diff --git a/DistributedTransaction/Test4.tla b/DistributedTransaction/Test4.tla new file mode 100644 index 0000000..7878525 --- /dev/null +++ b/DistributedTransaction/Test4.tla @@ -0,0 +1,13 @@ +--------------------------------- MODULE Test3 --------------------------------- +EXTENDS DistributedTransaction, TLC + +CONSTANT k1 +CONSTANT c1, c2 + +Keys == {k1} +OptimistiicClient == {c2} +PessimisticClient == {c1} +ClientReadKeys == c1 :> {} @@ c2 :> {k1} +ClientWriteKeys == c1 :> {k1} @@ c2 :> {k1} +ClientPrimary == c1 :> k1 @@ c2 :> k1 +================================================================================ diff --git a/DistributedTransaction/Test5.cfg b/DistributedTransaction/Test5.cfg new file mode 100644 index 0000000..0949218 --- /dev/null +++ b/DistributedTransaction/Test5.cfg @@ -0,0 +1,33 @@ +CONSTANT + k1 = k1 + k2 = k2 + k3 = k3 + c1 = c1 + c2 = c2 + c3 = c3 + +CONSTANT + KEY <- Keys + OPTIMISTIC_CLIENT <- OptimistiicClient + PESSIMISTIC_CLIENT <- PessimisticClient + CLIENT_READ_KEY <- ClientReadKeys + CLIENT_WRITE_KEY <- ClientWriteKeys + CLIENT_PRIMARY <- ClientPrimary + +INIT + Init + +NEXT + Next + +INVARIANT + TypeOK + UniqueCommitOrAbort + CommitConsistency + AbortConsistency + WriteConsistency + UniqueLockOrWrite + UniqueWrite + OptimisticReadSnapshotIsolation + PessimisticReadSnapshotIsolation + MsgTsConsistency diff --git a/DistributedTransaction/Test5.tla b/DistributedTransaction/Test5.tla new file mode 100644 index 0000000..a5e076c --- /dev/null +++ b/DistributedTransaction/Test5.tla @@ -0,0 +1,13 @@ +--------------------------------- MODULE Test5 --------------------------------- +EXTENDS DistributedTransaction, TLC + +CONSTANT k1, k2, k3 +CONSTANT c1, c2, c3 + +Keys == {k1, k2, k3} +OptimistiicClient == {c3} +PessimisticClient == {c1, c2} +ClientReadKeys == c1 :> {} @@ c2 :> {} @@ c3 :> {k1, k3} +ClientWriteKeys == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k2, k3} +ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3 +================================================================================