github-repos/tla-plus
1
0
Fork 0
mirror of https://github.com/pingcap/tla-plus.git synced 2024-12-26 12:30:10 +08:00
Code Issues Packages Projects Releases Wiki Activity

optimized commit ts: remove the cost of getting commitTS (#20)

Browse Source
This commit is contained in:
Haibin Xie 2018-05-14 17:55:33 +08:00 committed by siddontang
parent 13ef759c38
commit 2b1c387bbb
1 changed files with 21 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
OptimizedCommitTS/OptimizedCommitTS.tla
View File

@ -14,13 +14,15 @@ CONSTANTS CLIENT_PRIMARY_KEY
ASSUME CLIENT_PRIMARY_KEY \in [CLIENT -> KEY] ASSUME CLIENT_PRIMARY_KEY \in [CLIENT -> KEY]
\* $next_ts$ is the timestamp for transaction. It is increased monotonically, \* $next_ts$ is the timestamp for transaction. It is increased monotonically,
\* so every transaction must have a unique start and commit ts. \* so every transaction must have a unique start ts.
VARIABLES next_ts VARIABLES next_ts
\* $client_state[c]$ is the state of client. \* $client_state[c]$ is the state of client.
VARIABLES client_state VARIABLES client_state
\* $client_ts[c]$ is a record of [start_ts: ts, commit_ts: ts]. \* $client_ts[c]$ is a record of [start_ts: ts, commit_ts: ts].
\* The $commit_ts$ is set to $start_ts$ at first, then updated at every prewrite,
\* and finally increased by 1.
VARIABLES client_ts VARIABLES client_ts
\* $client_key[c]$ is a record of [primary: key, secondary: {key}, \* $client_key[c]$ is a record of [primary: key, secondary: {key},
@ -45,15 +47,15 @@ VARIABLES key_lock
\* $ts$ denotes commit_ts; for "rollback" record, $ts$ denotes start_ts. \* $ts$ denotes commit_ts; for "rollback" record, $ts$ denotes start_ts.
VARIABLES key_write VARIABLES key_write
\* Two auxiliary variables for verifying snapshot isolation invariant. These
\* variables should not appear in a real-world implementation.
\*
\* $key_last_read_ts[k]$ denotes the last read timestamp for key $k$, this \* $key_last_read_ts[k]$ denotes the last read timestamp for key $k$, this
\* should be monotonic. \* should be monotonic. It can be used to verfiy snapshot isolation invariant
\* \* and calculate commit ts. In a real-world implementation, each region will have
\* one $region_last_read_ts$.
VARIABLES key_last_read_ts
\* $key_si[k]$ denotes if the snapshot isolation invariant is preserved for \* $key_si[k]$ denotes if the snapshot isolation invariant is preserved for
\* key $k$ so far. \* key $k$ so far. This will not appear in a real-world implementation.
VARIABLES key_last_read_ts, key_si VARIABLES key_si
client_vars == <<client_state, client_ts, client_key>> client_vars == <<client_state, client_ts, client_key>>
key_vars == <<key_data, key_lock, key_write, key_last_read_ts, key_si>> key_vars == <<key_data, key_lock, key_write, key_last_read_ts, key_si>>
@ -63,6 +65,8 @@ vars == <<next_ts, client_vars, key_vars>>
Range(m) == Range(m) ==
{m[i] : i \in DOMAIN m} {m[i] : i \in DOMAIN m}
Max(a, b) == IF a < b THEN b ELSE a
-------------------------------------------------------------------------------- --------------------------------------------------------------------------------
\* Checks whether there is a lock of key $k$, whose $ts$ is less or equal than \* Checks whether there is a lock of key $k$, whose $ts$ is less or equal than
\* $ts$. \* $ts$.
@ -185,9 +189,10 @@ canLockKey(k, ts) ==
/\ writes = {} \* no any newer writes or rollbacks. /\ writes = {} \* no any newer writes or rollbacks.
\* Locks the key and places the data. \* Locks the key and places the data.
lockKey(k, start_ts, primary) == lockKey(c, k, start_ts, primary) ==
/\ key_lock' = [key_lock EXCEPT ![k] = @ \union {[ts |-> start_ts, primary |-> primary]}] /\ key_lock' = [key_lock EXCEPT ![k] = @ \union {[ts |-> start_ts, primary |-> primary]}]
/\ key_data' = [key_data EXCEPT ![k] = @ \union {[ts |-> start_ts]}] /\ key_data' = [key_data EXCEPT ![k] = @ \union {[ts |-> start_ts]}]
/\ client_ts' = [client_ts EXCEPT ![c].commit_ts = Max(client_ts[c].commit_ts, key_last_read_ts[k])]
/\ UNCHANGED <<key_write, key_last_read_ts, key_si>> /\ UNCHANGED <<key_write, key_last_read_ts, key_si>>
\* Tries to lock primary key first, then the secondary key. \* Tries to lock primary key first, then the secondary key.
@ -203,9 +208,9 @@ lock(c) ==
\* ensures its correctness. \* ensures its correctness.
\E k \in pending : \E k \in pending :
/\ canLockKey(k, start_ts) /\ canLockKey(k, start_ts)
/\ lockKey(k, start_ts, primary) /\ lockKey(c, k, start_ts, primary)
/\ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}] /\ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}]
/\ UNCHANGED <<client_state, client_ts>> /\ UNCHANGED <<client_state>>
\* Commits the primary key. \* Commits the primary key.
commitPrimary(c) == commitPrimary(c) ==
@ -229,7 +234,7 @@ Start(c) ==
/\ client_state[c] = "init" /\ client_state[c] = "init"
/\ next_ts' = next_ts + 1 /\ next_ts' = next_ts + 1
/\ client_state' = [client_state EXCEPT ![c] = "working"] /\ client_state' = [client_state EXCEPT ![c] = "working"]
/\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts'] /\ client_ts' = [client_ts EXCEPT ![c] = [start_ts |-> next_ts', commit_ts |-> next_ts']]
/\ UNCHANGED <<key_vars, client_key>> /\ UNCHANGED <<key_vars, client_key>>
\* Does either one thing from these following threes. \* Does either one thing from these following threes.
@ -251,10 +256,9 @@ Prewrite(c) ==
/\ client_state[c] = "prewriting" /\ client_state[c] = "prewriting"
/\ IF client_key[c].pending = {} /\ IF client_key[c].pending = {}
THEN \* all keys have been pre-written THEN \* all keys have been pre-written
/\ next_ts' = next_ts + 1
/\ client_state' = [client_state EXCEPT ![c] = "committing"] /\ client_state' = [client_state EXCEPT ![c] = "committing"]
/\ client_ts' = [client_ts EXCEPT ![c].commit_ts = next_ts'] /\ client_ts' = [client_ts EXCEPT ![c].commit_ts = client_ts[c].commit_ts + 1]
/\ UNCHANGED <<key_vars, client_key>> /\ UNCHANGED <<key_vars, client_key, next_ts>>
ELSE ELSE
/\ lock(c) /\ lock(c)
/\ UNCHANGED <<next_ts>> /\ UNCHANGED <<next_ts>>
@ -414,7 +418,7 @@ AbortedConsistency ==
(/\ client_state[c] = "aborted" (/\ client_state[c] = "aborted"
/\ client_ts[c].commit_ts # 0 /\ client_ts[c].commit_ts # 0
) => ) =>
findWriteWithCommitTS(client_key[c].primary, client_ts[c].commit_ts) = {} findWriteWithStartTS(client_key[c].primary, client_ts[c].start_ts) = {}
\* For each transaction, we cannot have both committed and rolled back keys. \* For each transaction, we cannot have both committed and rolled back keys.
RollbackConsistency == RollbackConsistency ==