From 33e2a8362731b042ba434d0ec80c9ae97434def7 Mon Sep 17 00:00:00 2001 From: Yilin Chen Date: Mon, 21 Oct 2019 16:36:56 +0800 Subject: [PATCH] pessimistic init Signed-off-by: Yilin Chen --- .../PessimisticTransaction.tla | 153 ++++++++++++++++++ .../PessimisticTransaction___Test1.launch | 30 ++++ 2 files changed, 183 insertions(+) create mode 100644 PessimisticTransaction/PessimisticTransaction.tla create mode 100644 PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch diff --git a/PessimisticTransaction/PessimisticTransaction.tla b/PessimisticTransaction/PessimisticTransaction.tla new file mode 100644 index 0000000..6c1beff --- /dev/null +++ b/PessimisticTransaction/PessimisticTransaction.tla @@ -0,0 +1,153 @@ +----------------------- MODULE PessimisticTransaction ----------------------- + +EXTENDS Integers + +\* The set of transaction keys. +CONSTANTS KEY +ASSUME KEY # {} \* Keys cannot be empty. + +\* The set of clients 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, for_update_ts, commit_ts]. +VARIABLES client_ts + +\* client_key[c] is a record of [primary: key, secondary: {key}, +\* pessimistic: {key}, pending: {key}]. Hereby, "pessimistic" denotes +\* the keys whose pessimistic locks haven't been acquired, "pending" +\* denotes the keys that are pending for prewrite. +VARIABLES client_key + +\* 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 record of +\* [ts: start_ts] is sufficient to represent one data version. +VARIABLES key_data + +\* key_lock[k] is the set of lock. A lock is of a record of [ts: start_ts, +\* for_update_ts, primary: key]. If primary equals to k, it is a primary +\* lock, otherwise secondary lock. If for_update_ts > 0, it belongs to a +\* pessimistic transaction. +VARIABLES key_lock + +\* key_write[k] is a sequence of committed version of the key. +\* A committed version of the key is a record of [ts, type, start_ts]. +\* type can be "write" or "rollback" depending on record type. start_ts +\* field only exists if type is "write". For "write" record, ts denotes +\* commit_ts; for "rollback" record, $ts$ denotes start_ts. +VARIABLES key_write + +\* key_last_read_ts is for verifying snapshot isolation invariant. It should +\* not appear in a real-world implementation. +\* +\* key_last_read_ts[k] denotes the last read timestamp for key k, this +\* should be monotonic. +VARIABLES key_last_read_ts + +\* The set of all messages sent by clients. To simulate message resending, +\* client messages are inserted to the set and never deleted. The server can +\* pick any message in the set to execute. +VARIABLES msg + +client_vars == <> +key_vars == <> +vars == <> + +----------------------------------------------------------------------------- + +Pos == {x \in Nat : x > 0} + +----------------------------------------------------------------------------- + +Init == + /\ next_ts = 1 + /\ client_state = [c \in CLIENT |-> "init"] + /\ client_ts = [c \in CLIENT |-> [start_ts |-> 0, + for_update_ts |-> 0, + commit_ts |-> 0] + ] + /\ client_key = [c \in CLIENT |-> {}] + /\ key_lock = [k \in KEY |-> {}] + /\ key_data = [k \in KEY |-> {}] + /\ key_write = [k \in KEY |-> {}] + /\ key_last_read_ts = [k \in KEY |-> 0] + /\ msg = {} + +Next == + UNCHANGED <> + +----------------------------------------------------------------------------- + +NextTsTypeInv == next_ts \in Pos + +ClientStateTypeInv == + client_state \in [ + CLIENT -> {"init", "working", "prewriting", + "committing", "committed", "aborted"} + ] + +ClientTsTypeInv == + client_ts \in + [CLIENT -> [start_ts : Nat, for_update_ts: Nat, commit_ts : Nat]] + +ClientKeyTypeInv == + client_key \in [ + CLIENT -> {{}} \union [ + primary: KEY, + secondary: SUBSET KEY, + pessimistic: SUBSET KEY, + pending : SUBSET KEY + ] + ] + +KeyDataTypeInv == + key_data \in [KEY -> SUBSET [ts: Pos]] + +KeyLockTypeInv == + key_lock \in [KEY -> SUBSET [ts: Pos, for_update_ts: Nat, primary: KEY]] + +KeyWriteTypeInv == + key_write \in [KEY -> + SUBSET [ts: Pos, type: {"write", "rollback"}, start_ts: Pos] + ] + +KeyWriteStartTsInv == + \A k \in DOMAIN key_write: + LET + rec == key_write[k] + IN + \/ rec = {} + \/ IF rec.type = "write" + THEN rec.ts > rec.start_ts + ELSE rec.type = "rollback" /\ rec.ts = rec.start_ts + +KeyLastReadTsTypeInv == + key_last_read_ts \in [KEY -> Nat] + +MsgTypeInv == + msg \subseteq ( + [c: CLIENT, type: {"lock", "prewrite"}, key: KEY, + start_ts: Pos, for_update_ts: Pos] \union + [c: CLIENT, type: {"commit"}, key: KEY, commit_ts: Pos] \union + [c: CLIENT, type: {"rollback"}, key: KEY] + ) + +TypeInvariant == + /\ NextTsTypeInv + /\ ClientStateTypeInv + /\ ClientTsTypeInv + /\ ClientKeyTypeInv + /\ KeyDataTypeInv + /\ KeyLockTypeInv + /\ KeyWriteTypeInv + /\ KeyWriteStartTsInv + /\ KeyLastReadTsTypeInv + /\ MsgTypeInv + +============================================================================= diff --git a/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch new file mode 100644 index 0000000..ff25b25 --- /dev/null +++ b/PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch @@ -0,0 +1,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +