diff --git a/.gitignore b/.gitignore index 3fc9e3a..6e72a9c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,6 @@ states/ - +*.out +*.tlaps **/*.toolbox/*/ **/*.toolbox/*___*_SnapShot_*.launch **/*.toolbox/.project diff --git a/DistributedTransaction/DistributedTransaction.pdf b/DistributedTransaction/DistributedTransaction.pdf new file mode 100644 index 0000000..ef6fe03 Binary files /dev/null and b/DistributedTransaction/DistributedTransaction.pdf differ diff --git a/DistributedTransaction/DistributedTransaction.tla b/DistributedTransaction/DistributedTransaction.tla new file mode 100644 index 0000000..d008e4c --- /dev/null +++ b/DistributedTransaction/DistributedTransaction.tla @@ -0,0 +1,597 @@ +----------------------- MODULE DistributedTransaction ----------------------- +EXTENDS Integers + +\* The set of all keys. +CONSTANTS KEY + +\* The sets of optiimistic clients and pessimistic clients. +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 + +\* CLIENT_PRIMARY is the primary key of each client. +CONSTANTS CLIENT_PRIMARY +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 +\* 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 +\* 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 +\* 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 +\* 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 +\* 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: +\* {"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" +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 eihter +\* "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 +\* 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]. +\* 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. +VARIABLES client_key + +\* next_ts is a globally monotonically increasing integer, respresenting +\* 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 == <> +key_vars == <> +vars == <> + +SendReqs(msgs) == req_msgs' = req_msgs \union msgs +SendResp(msg) == resp_msgs' = resp_msgs \union {msg} +----------------------------------------------------------------------------- +\* Type Definitions + +ReqMessages == + [start_ts : Ts, primary : KEY, type : {"lock_key"}, key : KEY, + for_update_ts : Ts] + \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"}] + +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, + type : {"prewrite_optimistic", + "prewrite_pessimistic", + "lock_key"}]] + /\ \A k \in KEY : + \* At most one lock in key_lock[k] + \A l, l2 \in key_lock[k] : + l = l2 + /\ 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_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]] + /\ 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] + /\ 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 |-> "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 <> + +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 <> + +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_key[c].locking = {} + /\ client_state' = [client_state EXCEPT ![c] = "prewriting"] + /\ client_key' = [client_key EXCEPT ![c].prewriting = CLIENT_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 <> + +ClientPrewriteOptimisistic(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 <> + +ClientCommit(c) == + /\ client_state[c] = "prewriting" + /\ client_key[c].prewriting = {} + /\ client_state' = [client_state 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 <> +----------------------------------------------------------------------------- +\* Server Actions + +\* Write the write column and unlock the lock iff the lock exists. +commit(pk, start_ts, commit_ts) == + \E l \in key_lock[pk] : + /\ l.ts = start_ts + /\ key_lock' = [key_lock EXCEPT ![pk] = {}] + /\ key_write' = [key_write EXCEPT ![pk] = @ \union {[ts |-> commit_ts, + type |-> "write", + 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] = {} + 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] = {}] + ELSE UNCHANGED key_lock + /\ key_data' = [key_data EXCEPT ![k] = @ \ {start_ts}] + /\ IF + /\ ~ \E w \in key_write[k]: w.ts = start_ts + THEN + key_write' = [key_write EXCEPT + ![k] = + \* collapse rollback + (@ \ {w \in @ : w.type = "rollback" /\ ~w.protected /\ w.ts < start_ts}) + \* write rollback record + \union {[ts |-> start_ts, + start_ts |-> start_ts, + type |-> "rollback", + protected |-> protected]}] + ELSE + UNCHANGED <> + +ServerLockKey == + \E req \in req_msgs : + /\ req.type = "lock_key" + /\ LET + k == req.key + start_ts == req.start_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"]) + /\ 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 <> + +ServerPrewritePessimistic == + \E req \in req_msgs : + /\ req.type = "prewrite_pessimistic" + /\ LET + 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 <> + +ServerCommit == + \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" + THEN + \* 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 <> + +\* 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]}) + /\ 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 == + \E req \in req_msgs : + /\ req.type = "cleanup" + /\ LET + pk == req.primary + start_ts == req.start_ts + committed == {w \in key_write[pk] : w.start_ts = start_ts /\ w.type = "write"} + 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 <> + +ServerResolveCommitted == + \E req \in req_msgs : + /\ req.type = "resolve_committed" + /\ LET + start_ts == req.start_ts + IN + \E k \in KEY: + \E l \in key_lock[k] : + /\ l.primary = req.primary + /\ l.ts = start_ts + /\ commit(k, start_ts, req.commit_ts) + /\ UNCHANGED <> + +ServerResolveRollbacked == + \E req \in req_msgs : + /\ req.type = "resolve_rollbacked" + /\ LET + start_ts == req.start_ts + IN + \E k \in KEY: + \E l \in key_lock[k] : + /\ l.primary = req.primary + /\ l.ts = start_ts + /\ rollback(k, start_ts) + /\ UNCHANGED <> +----------------------------------------------------------------------------- +\* Specification + +Init == + /\ next_ts = 1 + /\ req_msgs = {} + /\ resp_msgs = {} + /\ client_state = [c \in CLIENT |-> "init"] + /\ client_key = [c \in CLIENT |-> [locking |-> {}, prewriting |-> {}]] + /\ client_ts = [c \in CLIENT |-> [start_ts |-> NoneTs, + commit_ts |-> NoneTs, + for_update_ts |-> NoneTs]] + /\ key_lock = [k \in KEY |-> {}] + /\ key_data = [k \in KEY |-> {}] + /\ key_write = [k \in KEY |-> {}] + +Next == + \/ \E c \in OPTIMISTIC_CLIENT : + \/ ClientPrewriteOptimisistic(c) + \/ ClientPrewrited(c) + \/ ClientCommit(c) + \/ \E c \in PESSIMISTIC_CLIENT : + \/ ClientLockKey(c) + \/ ClientLockedKey(c) + \/ ClientRetryLockKey(c) + \/ ClientPrewritePessimistic(c) + \/ ClientPrewrited(c) + \/ ClientCommit(c) + \/ ServerLockKey + \/ ServerPrewritePessimistic + \/ ServerPrewriteOptimistic + \/ ServerCommit + \/ ServerCleanupStaleLock + \/ ServerCleanup + \/ ServerResolveCommitted + \/ ServerResolveRollbacked + +Spec == Init /\ [][Next]_vars +----------------------------------------------------------------------------- +\* Consistency Invariants + +\* Check whether there is a "write" record in key_write[k] corresponding +\* to start_ts. +keyCommitted(k, start_ts) == + \E w \in key_write[k] : + /\ w.start_ts = start_ts + /\ w.type = "write" + +\* A transaction can't be both committed and aborted. +UniqueCommitOrAbort == + \A resp, resp2 \in resp_msgs : + (resp.type = "committed") /\ (resp2.type = "commit_aborted") => + resp.start_ts /= resp2.start_ts + +\* If a transaction is committed, the primary key must be committed and +\* the secondary keys of the same transaction must be either committed +\* or locked. +CommitConsistency == + \A resp \in resp_msgs : + (resp.type = "committed") => + \E c \in CLIENT : + /\ client_ts[c].start_ts = resp.start_ts + \* Primary key must be committed + /\ 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) = + keyCommitted(k, resp.start_ts) + +\* If a transaction is aborted, all key of that transaction must be not +\* committed. +AbortConsistency == + \A resp \in resp_msgs : + (resp.type = "commit_aborted") => + \A c \in CLIENT : + (client_ts[c].start_ts = resp.start_ts) => + ~ 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, +\* the commit_ts should equals to the start_ts. +WriteConsistency == + \A k \in KEY : + \A w \in key_write[k] : + \/ /\ w.type = "write" + /\ w.ts > w.start_ts + /\ w.start_ts \in key_data[k] + \/ /\ w.type = "rollback" + /\ w.ts = w.start_ts + +\* When the lock exists, there can't be a corresponding commit record, +\* vice versa. +UniqueLockOrWrite == + \A k \in KEY : + \A l \in key_lock[k] : + \A w \in key_write[k] : + w.start_ts /= l.ts + +\* For each key, ecah record in write column should have a unique start_ts. +UniqueWrite == + \A k \in KEY : + \A w, w2 \in key_write[k] : + (w.start_ts = w2.start_ts) => (w = w2) +----------------------------------------------------------------------------- +\* Snapshot Isolation + +\* Asserts that next_ts is monotonically increasing. +NextTsMonotonicity == + \A ts \in Ts : + (ts <= next_ts) => [](ts <= next_ts) + +\* Asserts that no msg would be deleted once sent. +MsgMonotonicity == + /\ \A req \in ReqMessages : + req \in req_msgs => [](req \in req_msgs) + /\ \A resp \in RespMessages : + resp \in resp_msgs => [](resp \in resp_msgs) + +\* 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 + +\* SnapshotIsolation is implied from the following assumptions (but is not +\* nessesary), because SnapshotIsolation means that: +\* (1) Once a transcation is committed, all keys of the transaction should +\* be always readable or have 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 commits 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 +----------------------------------------------------------------------------- +THEOREM Safety == + Spec => [](/\ TypeOK + /\ UniqueCommitOrAbort + /\ CommitConsistency + /\ AbortConsistency + /\ WriteConsistency + /\ UniqueLockOrWrite + /\ UniqueWrite + /\ SnapshotIsolation) +============================================================================= diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch new file mode 100644 index 0000000..acb55a8 --- /dev/null +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch @@ -0,0 +1,41 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch new file mode 100644 index 0000000..3e2e636 --- /dev/null +++ b/DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch @@ -0,0 +1,42 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/DistributedTransaction/DistributedTransactionProofs.tla b/DistributedTransaction/DistributedTransactionProofs.tla new file mode 100644 index 0000000..0a1b1af --- /dev/null +++ b/DistributedTransaction/DistributedTransactionProofs.tla @@ -0,0 +1,47 @@ +--------------------- MODULE DistributedTransactionProofs ------------------- +EXTENDS DistributedTransaction, TLAPS + +THEOREM SpecTypeOK == Spec => TypeOK + PROOF OMITTED + +LEMMA NextInv == + Next => + /\ next_ts' = next_ts + 1 \/ UNCHANGED next_ts + /\ \E reqs : SendReqs(reqs) \/ UNCHANGED req_msgs + /\ \E resp : SendResp(resp) \/ UNCHANGED resp_msgs + BY DEF Next, vars, msg_vars, + ClientPrewriteOptimisistic, ClientPrewrited, ClientCommit, ClientLockKey, + ClientLockedKey, ClientRetryLockKey, ClientPrewritePessimistic, + ClientPrewrited, ClientCommit, ServerLockKey, ServerPrewritePessimistic, + ServerPrewriteOptimistic, ServerCommit, ServerCleanupStaleLock, + ServerCleanup, ServerResolveCommitted, ServerResolveRollbacked + +LEMMA SpecNextTsMonotonicity == Spec => NextTsMonotonicity + <1> SUFFICES ASSUME NEW ts \in Ts, TypeOK + PROVE (ts <= next_ts) /\ [][Next]_vars => [](ts <= next_ts) + BY SpecTypeOK DEF NextTsMonotonicity, Spec + <1>2. (ts <= next_ts) /\ [Next]_vars => (ts <= next_ts)' + BY NextInv DEF TypeOK, Ts, vars + <1>3. QED + BY <1>2, PTL + +LEMMA SpecMsgMonotonicity == Spec => MsgMonotonicity + <1>1. ASSUME NEW req \in ReqMessages + PROVE req \in req_msgs /\ [][Next]_vars => [](req \in req_msgs) + <2>1. req \in req_msgs /\ (\E reqs : SendReqs(reqs)) => (req \in req_msgs)' + BY DEF SendReqs + <2>2. req \in req_msgs /\ [Next]_vars => (req \in req_msgs)' + BY <2>1, NextInv DEF vars, msg_vars + <2>3. QED + BY <2>2, PTL + <1>2. ASSUME NEW resp \in RespMessages + PROVE resp \in resp_msgs /\ [][Next]_vars => [](resp \in resp_msgs) + <3>1. resp \in resp_msgs /\ (\E resp2 : SendResp(resp2)) => (resp \in resp_msgs)' + BY DEF SendResp + <3>2. resp \in resp_msgs /\ [Next]_vars => (resp \in resp_msgs)' + BY <3>1, NextInv DEF vars, msg_vars + <3>3. QED + BY <3>2, PTL + <1>3. QED + BY <1>1, <1>2, SpecTypeOK DEF MsgMonotonicity, Spec +============================================================================= diff --git a/DistributedTransaction/README.md b/DistributedTransaction/README.md new file mode 100644 index 0000000..1d4a4b4 --- /dev/null +++ b/DistributedTransaction/README.md @@ -0,0 +1,9 @@ +# TLA+ for Distributed Transaction + +The module contains a abstract specification of the transaction system implemented in TiKV. The implementation can be found in [TiKV Transaction Module](https://github.com/tikv/tikv/blob/master/src/storage/mvcc/txn.rs). + +The module contains two TLA+ files: `DistributedTransaction.tla` and `DistributedTransactionProofs.tla`. + +In most cases you will likely have an interest in only `DistributedTransaction.tla`, where the specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some formal proofs, which are supposed to be build up gradually (so it's not completed yet), to the safety invariants. + +To run the formal proofs in `DistributedTransactionProofs.tla`, you'd like to install the [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox. diff --git a/DistributedTransaction/Test1.cfg b/DistributedTransaction/Test1.cfg new file mode 100644 index 0000000..93f0ac2 --- /dev/null +++ b/DistributedTransaction/Test1.cfg @@ -0,0 +1,29 @@ +CONSTANT + k1 = k1 + k2 = k2 + c1 = c1 + c2 = c2 + c3 = c3 + +CONSTANT + KEY <- Key + OPTIMISTIC_CLIENT <- OptimistiicClient + PESSIMISTIC_CLIENT <- PessimisticClient + CLIENT_KEY <- ClientKey + CLIENT_PRIMARY <- ClientPrimary + +INIT + Init + +NEXT + Next + +INVARIANT + TypeOK + UniqueCommitOrAbort + CommitConsistency + AbortConsistency + WriteConsistency + UniqueLockOrWrite + UniqueWrite + MsgTsConsistency diff --git a/DistributedTransaction/Test1.tla b/DistributedTransaction/Test1.tla new file mode 100644 index 0000000..d267bbd --- /dev/null +++ b/DistributedTransaction/Test1.tla @@ -0,0 +1,12 @@ +--------------------------------- MODULE Test1 --------------------------------- +EXTENDS DistributedTransaction, TLC + +CONSTANT k1, k2 +CONSTANT c1, c2, c3 + +Key == {k1, k2} +OptimistiicClient == {c3} +PessimisticClient == {c1, c2} +ClientKey == 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 new file mode 100644 index 0000000..1473b5d --- /dev/null +++ b/DistributedTransaction/Test2.cfg @@ -0,0 +1,30 @@ +CONSTANT + k1 = k1 + k2 = k2 + k3 = k3 + c1 = c1 + c2 = c2 + c3 = c3 + +CONSTANT + KEY <- Key + OPTIMISTIC_CLIENT <- OptimistiicClient + PESSIMISTIC_CLIENT <- PessimisticClient + CLIENT_KEY <- ClientKey + CLIENT_PRIMARY <- ClientPrimary + +INIT + Init + +NEXT + Next + +INVARIANT + TypeOK + UniqueCommitOrAbort + CommitConsistency + AbortConsistency + WriteConsistency + UniqueLockOrWrite + UniqueWrite + MsgTsConsistency diff --git a/DistributedTransaction/Test2.tla b/DistributedTransaction/Test2.tla new file mode 100644 index 0000000..f36a89e --- /dev/null +++ b/DistributedTransaction/Test2.tla @@ -0,0 +1,12 @@ +--------------------------------- MODULE Test2 --------------------------------- +EXTENDS DistributedTransaction, TLC + +CONSTANT k1, k2, k3 +CONSTANT c1, c2, c3 + +Key == {k1, k2, k3} +OptimistiicClient == {c3} +PessimisticClient == {c1, c2} +ClientKey == c1 :> {k1, k2, k3} @@ c2 :> {k1, k2} @@ c3 :> {k1, k3} +ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k3 +================================================================================