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

Merge pull request #30 from andylokandy/dis

Browse Source 
Add a refined spec for distributed transaction
This commit is contained in:
Andy Lok 2020-07-10 18:55:18 +08:00 committed by GitHub
commit b9806173e6
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 821 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
.gitignore vendored
View File

@ -1,5 +1,6 @@
states/
*.out
*.tlaps
**/*.toolbox/*/
**/*.toolbox/*___*_SnapShot_*.launch
**/*.toolbox/.project

BIN
DistributedTransaction/DistributedTransaction.pdf Normal file
View File

Binary file not shown.

597
DistributedTransaction/DistributedTransaction.tla Normal file
View File

@ -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 == <<req_msgs, resp_msgs>>
client_vars == <<client_state, client_ts, client_key>>
key_vars == <<key_data, key_lock, key_write>>
vars == <<msg_vars, client_vars, key_vars, next_ts>>
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 <<resp_msgs, key_vars>>
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 <<msg_vars, key_vars, client_ts, client_state, next_ts>>
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 <<resp_msgs, key_vars, client_state, client_key, next_ts>>
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 <<resp_msgs, key_vars, client_ts, next_ts>>
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 <<resp_msgs, key_vars>>
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 <<msg_vars, key_vars, client_ts, client_state, next_ts>>
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 <<resp_msgs, key_vars, client_key>>
-----------------------------------------------------------------------------
\* 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 <<key_write>>
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 <<req_msgs, client_vars, key_vars, next_ts>>
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 <<req_msgs, client_vars, key_data, key_write, next_ts>>
\* 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 <<req_msgs, client_vars, key_vars, next_ts>>
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 <<req_msgs, client_vars, key_write, next_ts>>
ELSE
/\ SendResp([start_ts |-> start_ts, type |-> "prewrite_aborted"])
/\ UNCHANGED <<req_msgs, client_vars, key_vars, next_ts>>
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 <<req_msgs, client_vars, key_vars, next_ts>>
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 <<req_msgs, client_vars, key_write, next_ts>>
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 <<req_msgs, client_vars, key_vars, next_ts>>
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 <<req_msgs, client_vars, key_data, next_ts>>
ELSE
\* Otherwise, abort the transaction.
/\ SendResp([start_ts |-> start_ts, type |-> "commit_aborted"])
/\ UNCHANGED <<req_msgs, client_vars, key_vars, next_ts>>
\* 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 <<resp_msgs, client_vars, key_vars, next_ts>>
\* 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 <<resp_msgs, client_vars, key_vars, next_ts>>
ELSE
/\ rollback(pk, start_ts)
/\ SendReqs({[type |-> "resolve_rollbacked",
start_ts |-> start_ts,
primary |-> pk]})
/\ UNCHANGED <<resp_msgs, client_vars, next_ts>>
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 <<msg_vars, client_vars, key_data, next_ts>>
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 <<msg_vars, client_vars, next_ts>>
-----------------------------------------------------------------------------
\* 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)
=============================================================================

41
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test1.launch Normal file
View File

@ -0,0 +1,41 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Test1"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="8"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="8"/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;0"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1} @@ c3 :&gt; {k1, k2};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k2;0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="6"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

42
DistributedTransaction/DistributedTransaction.toolbox/DistributedTransaction___Test2.launch Normal file
View File

@ -0,0 +1,42 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="configurationName" value="Test2"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="64"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value=""/>
<stringAttribute key="modelBehaviorNext" value=""/>
<stringAttribute key="modelBehaviorSpec" value="Spec"/>
<intAttribute key="modelBehaviorSpecType" value="1"/>
<stringAttribute key="modelBehaviorVars" value="key_data, key_lock, next_ts, req_msgs, client_state, client_key, client_ts, resp_msgs, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="1TypeOK"/>
<listEntry value="1UniqueCommitOrAbort"/>
<listEntry value="1CommitConsistency"/>
<listEntry value="1AbortConsistency"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1UniqueLockOrWrite"/>
<listEntry value="1UniqueWrite"/>
<listEntry value="1MsgTsConsistency"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="8"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2, k3};1;0"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2, k3} @@ c2 :&gt; {k1, k2} @@ c3 :&gt; {k1, k3};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;0"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c3};1;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k3;0;0"/>
</listAttribute>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="6"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="DistributedTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

47
DistributedTransaction/DistributedTransactionProofs.tla Normal file
View File

@ -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
=============================================================================

9
DistributedTransaction/README.md Normal file
View File

@ -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.

29
DistributedTransaction/Test1.cfg Normal file
View File

@ -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

12
DistributedTransaction/Test1.tla Normal file
View File

@ -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
================================================================================

30
DistributedTransaction/Test2.cfg Normal file
View File

@ -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

12
DistributedTransaction/Test2.tla Normal file
View File

@ -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
================================================================================