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

refine distributed transaction

Browse Source 
Signed-off-by: andylokandy <andylokandy@hotmail.com>
This commit is contained in:
andylokandy 2020-04-08 02:36:57 +08:00
parent c108f8d201
commit 84639c0422
17 changed files with 819 additions and 826 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

BIN
DistributedTransaction/DistributedTransaction.pdf Normal file
View File

Binary file not shown.

596
DistributedTransaction/DistributedTransaction.tla Normal file
View File

@ -0,0 +1,596 @@
----------------------- 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 strat_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 four 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, MsgConsistency
\* (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, MsgConsistency
SnapshotIsolation == /\ CommitConsistency
/\ AbortConsistency
/\ NextTsMonotonicity
/\ MsgMonotonicity
-----------------------------------------------------------------------------
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
=============================================================================

10
DistributedTransaction/README.md Normal file
View File

@ -0,0 +1,10 @@
# 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 only have an interest in `DistributedTransaction.tla`, where the whole specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some proofs, which are supposed to be build up gradually, to the safety invariants.
To run formal proofs in `DistributedTransactionProofs.tla`, you'd better install [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
================================================================================

621
PessimisticTransaction/PessimisticTransaction.tla
View File

@ -1,621 +0,0 @@
----------------------- MODULE PessimisticTransaction -----------------------
EXTENDS Integers, FiniteSets, TLC
\* The set of transaction keys.
CONSTANTS KEY
ASSUME KEY /= {} \* Keys cannot be empty.
\* The set of pessimistic clients
CONSTANTS PESSIMISTIC_CLIENT
\* The set of optimistic clients
CONSTANTS OPTIMISTIC_CLIENT
\* The set of clients to execute a transaction.
CLIENT == PESSIMISTIC_CLIENT \union OPTIMISTIC_CLIENT
\* CLIENT_KEY is a set of [c -> SUBSET KEY],
\* representing involved keys of each client
CONSTANTS CLIENT_KEY
ASSUME \A c \in CLIENT: CLIENT_KEY[c] \subseteq KEY
CONSTANTS CLIENT_PRIMARY
ASSUME \A c \in CLIENT: CLIENT_PRIMARY[c] \in CLIENT_KEY[c]
\* 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, protected].
\* 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.
\* The commit_ts of a successful commit should greater then the last read_ts.
VARIABLES key_last_read_ts
\* The set of all messages sent by clients. To simulate message resending,
\* client messages are inserted into the set and never deleted. The server can
\* pick any message in the set to execute.
VARIABLES msg
client_vars == <<client_state, client_ts, client_key>>
key_vars == <<key_data, key_lock, key_write, key_last_read_ts>>
vars == <<next_ts, client_vars, key_vars, msg>>
-----------------------------------------------------------------------------
Pos == Nat \ {0}
-----------------------------------------------------------------------------
\* Find a stale lock which blocks the read for key k.
findStaleLock(k, ts) ==
{l \in key_lock[k] : l.pessimistic = FALSE /\ l.ts < ts}
\* Get the write records of k before or at timestamp ts
historyWrites(k, ts) ==
{w \in key_write[k] : w.ts <= ts}
\* Get the set of the latest write record of k before or at timestamp ts
latestHistoryWrite(k, ts) ==
{w \in historyWrites(k, ts) :
\A w2 \in historyWrites(k, ts) : w.ts >= w2.ts}
\* Rollback key k in the transaction starting at ts
rollback(k, ts) ==
LET
\* rollback the primary key of a pessimistic transaction needs be protected from being collapsed
protected == \E l \in key_lock[k] : l.for_update_ts > 0 /\ k = l.primary
latest_write == latestHistoryWrite(k, ts)
IN
\* If the existing lock has the same ts, unlock it.
/\ IF \E l \in key_lock[k] : l.ts = ts
THEN key_lock' = [key_lock EXCEPT ![k] = {}]
ELSE UNCHANGED key_lock
/\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> ts]}]
\* Write a rollback in the write column.
/\ key_write' = [key_write EXCEPT
![k] = IF ~ \E w \in latest_write: w.ts = ts
THEN (@ \ {w \in latest_write: w.type = "rollback" /\ ~w.protected }) \* collapse rollback
\union {[ts |-> ts, type |-> "rollback", start_ts |-> ts, protected |-> protected]}
ELSE @
]
\* Commit key k
commit(k, start_ts, commit_ts) ==
/\ IF \E l \in key_lock[k] : l.ts = start_ts
THEN
\* Write the write column and unlock the lock iff the lock exists
/\ key_lock' = [key_lock EXCEPT ![k] = {}]
/\ key_write' = [key_write EXCEPT ![k] = @ \union {[ts |-> commit_ts, type |-> "write", start_ts |-> start_ts]}]
\* Assert we don't violate snapshot isolation
\* TODO
/\ Assert(key_last_read_ts[k] < commit_ts, <<key_last_read_ts[k], commit_ts>>)
ELSE
UNCHANGED <<key_lock, key_write>>
/\ UNCHANGED key_data
\* Change the state of client c to aborted
abortTxn(c) ==
/\ client_state[c] /= "committed"
/\ client_state' = [client_state EXCEPT ![c] = "aborted"]
-----------------------------------------------------------------------------
StartOptimistic(c) ==
/\ client_state[c] = "init"
/\ next_ts' = next_ts + 1
/\ client_key' =
[client_key EXCEPT
![c] = [primary |-> CLIENT_PRIMARY[c],
secondary |-> CLIENT_KEY[c] \ {CLIENT_PRIMARY[c]},
pessimistic |-> {}, \* An optimistic transaction has no pessimistic lock to acquire
pending |-> CLIENT_KEY[c]]]
/\ client_state' = [client_state EXCEPT ![c] = "prewriting"]
\* The for_update_ts is initialized to be 0 in optimistic transactions.
/\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts', ![c].for_update_ts = 0]
/\ UNCHANGED <<key_vars, msg>>
StartPessimistic(c) ==
/\ client_state[c] = "init"
/\ next_ts' = next_ts + 1
/\ client_key' =
[client_key EXCEPT
![c] = [primary |-> CLIENT_PRIMARY[c],
secondary |-> CLIENT_KEY[c] \ {CLIENT_PRIMARY[c]},
pessimistic |-> CLIENT_KEY[c], \* Assume we need to acquire pessimistic locks for all keys
pending |-> CLIENT_KEY[c]]]
/\ client_state' = [client_state EXCEPT ![c] = "working"]
\* The for_update_ts is initialized to be the same as start_ts.
/\ client_ts' = [client_ts EXCEPT ![c].start_ts = next_ts', ![c].for_update_ts = next_ts']
/\ UNCHANGED <<key_vars, msg>>
LockKey(c) ==
/\ client_state[c] = "working"
/\ IF client_key[c].pessimistic = {}
THEN
\* The client can prewrite after all pessimistic locks have been acquired.
/\ client_state' = [client_state EXCEPT ![c] = "prewriting"]
/\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
ELSE
\* Select any unlocked key and acquire its pessimistic lock
\E k \in client_key[c].pessimistic :
/\ msg' = msg \union
{[c |-> c, type |-> "lock", key |-> k, primary |-> client_key[c].primary,
start_ts |-> client_ts[c].start_ts, for_update_ts |-> client_ts[c].for_update_ts]}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
Prewrite(c) ==
/\ client_state[c] = "prewriting"
/\ IF client_key[c].pending = {}
THEN
\* The client can commit the primary key after prewriting all keys.
/\ client_state' = [client_state EXCEPT ![c] = "committing"]
/\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
ELSE
\* Select any pending key to prewrite
\E k \in client_key[c].pending :
/\ msg' = msg \union
{[c |-> c, type |-> "prewrite", key |-> k, primary |-> client_key[c].primary,
start_ts |-> client_ts[c].start_ts, for_update_ts |-> client_ts[c].for_update_ts]}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
Commit(c) ==
/\ client_state[c] = "committing"
\* Get a new ts as commit_ts
/\ IF client_ts[c].commit_ts = 0
THEN
/\ next_ts' = next_ts + 1
/\ client_ts' = [client_ts EXCEPT ![c].commit_ts = next_ts']
ELSE
UNCHANGED <<next_ts, client_ts>>
\* Commit the primary key
/\ msg' = msg \union
{[c |-> c, type |-> "commit", key |-> client_key[c].primary,
start_ts |-> client_ts[c].start_ts, commit_ts |-> client_ts'[c].commit_ts]}
/\ UNCHANGED <<client_state, client_key, key_vars>>
OptimisticClientOp(c) ==
\/ StartOptimistic(c)
\/ Prewrite(c)
\/ Commit(c)
\* Committing secondary keys is ommitted
PessimisticClientOp(c) ==
\/ StartPessimistic(c)
\/ LockKey(c)
\/ Prewrite(c)
\/ Commit(c)
\* Committing secondary keys is ommitted
DoRead ==
\E cmd \in msg :
/\ cmd.type = "read"
/\ LET
k == cmd.key
ts == cmd.ts
IN
LET
stale_lock == findStaleLock(k, ts)
IN
IF stale_lock = {}
\* Successfully read
THEN
\* The client receives the read response, update the last read ts
/\ IF key_last_read_ts[k] < ts
THEN key_last_read_ts' = [key_last_read_ts EXCEPT ![k] = ts]
ELSE UNCHANGED key_last_read_ts
\* To simulate the client fails to receive the read response
/\ UNCHANGED <<client_vars, key_data, key_lock, key_write, next_ts, msg>>
ELSE
\* When there is a blocking lock, the client may resolve the lock by cleanup.
/\ msg' = msg \union
{[type |-> "cleanup", primary |-> l.primary, start_ts |-> l.ts] : l \in stale_lock}
/\ UNCHANGED <<client_state, client_ts, client_key, key_vars, next_ts>>
\* Response loss leads to no state change
DoCleanup ==
\E cmd \in msg :
/\ cmd.type = "cleanup"
/\ LET
k == cmd.primary
ts == cmd.start_ts
IN
LET
lock == {l \in key_lock[k] : l.ts = ts}
committed == {w \in key_write[k] : w.start_ts = ts /\ w.type = "write"}
IN
IF committed /= {}
\* The transaction is already committed, so resolve locks using its commit_ts
THEN
/\ msg' = msg \union
{[type |-> "resolve", primary |-> k, start_ts |-> ts, commit_ts |-> t.ts] : t \in committed}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
ELSE
\* The transaction is not committed, so rollback the primary key.
/\ rollback(k, ts)
/\ UNCHANGED <<key_last_read_ts, next_ts, client_vars>>
\* The client may resolve locks using 0 as commit_ts. When the cleanup response is lost,
\* msg remains unchanged.
/\ \/ msg' = msg \union
{[type |-> "resolve", primary |-> k, start_ts |-> ts, commit_ts |-> 0]}
\/ UNCHANGED msg
DoResolve ==
\E cmd \in msg :
/\ cmd.type = "resolve"
/\ IF cmd.commit_ts = 0
THEN
\* rollback locks when commit_ts = 0
\E k \in KEY :
\E l \in key_lock[k] :
/\ l.primary = cmd.primary
/\ l.ts = cmd.start_ts
/\ rollback(k, cmd.start_ts)
ELSE
\* commit locks when commit_ts > 0
\E k \in KEY :
\E l \in key_lock[k] :
/\ l.primary = cmd.primary
/\ l.ts = cmd.start_ts
/\ commit(k, cmd.start_ts, cmd.commit_ts)
/\ UNCHANGED <<next_ts, client_vars, key_last_read_ts, msg>>
\* This action is too complex and concrete. Maybe simplify it?
DoLockKey ==
\E cmd \in msg :
/\ cmd.type = "lock"
/\ LET
c == cmd.c
k == cmd.key
primary == cmd.primary
ts == cmd.start_ts
for_update_ts == cmd.for_update_ts
\* Write or overwrite the pessimistic lock
writeLock ==
/\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> ts, for_update_ts |-> for_update_ts, primary |-> primary, pessimistic |-> TRUE]}]
/\ UNCHANGED <<client_state, client_ts, key_data, key_write, key_last_read_ts, next_ts, msg>>
\* Inform the client that the key is locked
/\ \/ client_key' = [client_key EXCEPT ![c].pessimistic = @ \ {k}]
\* client_key remains the same when the response is lost
\/ UNCHANGED client_key
\* Update the for_update_ts in the client with new_ts
updateForUpdateTs(new_ts) ==
IF new_ts > client_ts[c].for_update_ts
THEN
/\ client_ts' = [client_ts EXCEPT ![c].for_update_ts = for_update_ts]
/\ UNCHANGED <<client_state, client_key, next_ts, key_vars, msg>>
ELSE UNCHANGED vars
IN
IF key_lock[k] = {}
THEN
IF key_write[k] = {}
\* If no lock or write exists, we can always lock the key
THEN writeLock
ELSE
LET
\* Find the write record with biggest commit_ts
latest == CHOOSE w \in key_write[k] : \A w2 \in key_write[k] : w.ts >= w2.ts
IN
IF latest.ts > for_update_ts
\* Update the client's for_update_ts when there is a newer commit.
\* Response loss causes no state change.
THEN updateForUpdateTs(latest.ts)
ELSE
IF \E w \in key_write[k] : w.start_ts = ts /\ w.type = "rollback"
\* If any key to be locked is rollbacked, abort the transaction.
\* TODO: Maybe it needn't be included in the spec.
THEN abortTxn(c) /\ UNCHANGED <<next_ts, client_ts, client_key, key_vars, msg>>
\* Otherwise we can lock the key.
ELSE writeLock
ELSE
LET
l == CHOOSE l \in key_lock[k] : TRUE
IN
IF l.ts /= ts
\* If there is a lock from another transaction, the client may cleanup the lock.
\* Response loss causes no state change.
THEN
/\ msg' = msg \union
{[type |-> "cleanup", primary |-> l.primary, start_ts |-> l.ts]}
/\ UNCHANGED <<client_state, client_ts, client_key, key_vars, next_ts>>
ELSE
\* Only overwrite the lock when it's a pessimistic lock with smaller for_update_ts
/\ l.pessimistic
/\ l.for_update_ts < for_update_ts
/\ writeLock
DoOptimisticPrewrite ==
\E cmd \in msg :
/\ cmd.type = "prewrite"
/\ cmd.for_update_ts = 0
/\ LET
c == cmd.c
k == cmd.key
primary == cmd.primary
ts == cmd.start_ts
lock == { l \in key_lock[k] : l.ts /= ts }
IN
IF \E w \in key_write[k] : w.ts >= ts
THEN
/\ abortTxn(c)
/\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
ELSE IF lock /= {}
THEN
\* When there is another transaction's lock, the client may resolve the lock by cleanup.
/\ msg' = msg \union
{[type |-> "cleanup", primary |-> l.primary, start_ts |-> l.ts] : l \in lock}
/\ UNCHANGED <<client_state, client_ts, client_key, key_vars, next_ts>>
\* Response loss leads to no state change
ELSE
\* Otherwise prewrite
/\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> ts, for_update_ts |-> 0, primary |-> primary, pessimistic |-> FALSE]}]
/\ key_data' = [key_data EXCEPT ![k] = @ \union {[ts |-> ts]}]
\* Inform the client that the key is successfully prewritten
/\ \/ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}]
\* Simulate response loss
\/ UNCHANGED client_key
/\ UNCHANGED <<client_state, client_ts, key_write, key_last_read_ts, next_ts, msg>>
DoPessimisticPrewrite ==
\E cmd \in msg :
/\ cmd.type = "prewrite"
/\ cmd.for_update_ts > 0
/\ LET
c == cmd.c
k == cmd.key
primary == cmd.primary
ts == cmd.start_ts
for_update_ts == cmd.for_update_ts
IN
IF
\/ key_lock[k] = {}
\/ \E l \in key_lock[k] : l.ts /= ts
THEN
\* Abort the transaction when its lock doesn't exist
/\ abortTxn(c)
/\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
ELSE
\* Otherwise rewrite the existing lock to an optimistic lock
/\ key_lock' = [key_lock EXCEPT ![k] = {[ts |-> ts, for_update_ts |-> for_update_ts, primary |-> primary, pessimistic |-> FALSE]}]
/\ key_data' = [key_data EXCEPT ![k] = @ \union {[ts |-> ts]}]
\* Inform the client that the key is successfully prewritten
/\ \/ client_key' = [client_key EXCEPT ![c].pending = @ \ {k}]
\* Simulate response loss
\/ UNCHANGED client_key
/\ UNCHANGED <<client_state, client_ts, key_write, key_last_read_ts, next_ts, msg>>
DoCommit ==
\E cmd \in msg :
/\ cmd.type = "commit"
/\ LET
c == cmd.c
k == cmd.key
start_ts == cmd.start_ts
commit_ts == cmd.commit_ts
IN
IF \/ \E l \in key_lock[k] : l.ts = start_ts
\/ \E w \in key_write[k] : w.start_ts = start_ts /\ w.type = "write"
\* Commit the key iff the prewritten key exists or it's a repeated commit
THEN
/\ commit(k, start_ts, commit_ts)
\* Change client state to committed.
/\ client_state' = [client_state EXCEPT ![c] = "committed"]
/\ UNCHANGED <<client_ts, client_key, next_ts, key_last_read_ts, msg>>
ELSE
\* The lock doesn't exist and the key is not committed, so commit fails.
/\ Assert(client_state[c] /= "committed", client_state[c])
/\ abortTxn(c)
/\ UNCHANGED <<client_ts, client_key, next_ts, key_vars, msg>>
ServerOp ==
\/ DoRead
\/ DoCleanup
\/ DoResolve
\/ DoLockKey
\/ DoOptimisticPrewrite
\/ DoPessimisticPrewrite
\/ DoCommit
Read ==
\E ts \in 0..next_ts :
\E k \in KEY :
/\ msg' = msg \union {[type |-> "read", key |-> k, ts |-> next_ts]}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
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 ==
\/ ServerOp
\/ \E c \in OPTIMISTIC_CLIENT : OptimisticClientOp(c)
\/ \E c \in PESSIMISTIC_CLIENT : PessimisticClientOp(c)
\/ Read
PessimisticSpec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
NextTsTypeOK == next_ts \in Pos
ClientStateTypeOK ==
client_state \in [
CLIENT -> {"init", "working", "prewriting",
"committing", "committed", "aborted"}
]
ClientTsTypeOK ==
client_ts \in
[CLIENT -> [start_ts : Nat, for_update_ts : Nat, commit_ts : Nat]]
ClientKeyTypeOK ==
\A c \in CLIENT :
\/ client_state[c] = "init"
\/ client_key[c] \in [primary : KEY,
secondary : SUBSET KEY,
pessimistic : SUBSET KEY,
pending : SUBSET KEY]
KeyDataTypeOK ==
key_data \in [KEY -> SUBSET [ts : Pos]]
KeyLockTypeOK ==
key_lock \in [KEY -> SUBSET [ts : Pos, for_update_ts : Nat, primary : KEY, pessimistic : BOOLEAN]]
KeyWriteTypeOK ==
key_write \in [KEY -> SUBSET ([ts : Pos, type : {"write"}, start_ts : Pos] \union
[ts : Pos, type : {"rollback"}, start_ts : Pos, protected : BOOLEAN])]
KeyLastReadTsTypeOK ==
key_last_read_ts \in [KEY -> Nat]
MsgTypeOK ==
msg \subseteq (
[c : CLIENT, type : {"lock", "prewrite"}, key : KEY, primary: KEY,
start_ts : Pos, for_update_ts : Nat] \union
[c : CLIENT, type : {"commit"}, key : KEY, start_ts : Pos, commit_ts : Pos] \union
[type : {"read"}, key : KEY, ts : Nat] \union
[type : {"cleanup"}, primary : KEY, start_ts : Pos] \union
[type : {"resolve"}, primary : KEY, start_ts : Pos, commit_ts : Nat]
)
TypeOK ==
/\ NextTsTypeOK
/\ ClientStateTypeOK
/\ ClientTsTypeOK
/\ ClientKeyTypeOK
/\ KeyDataTypeOK
/\ KeyLockTypeOK
/\ KeyWriteTypeOK
/\ KeyLastReadTsTypeOK
/\ MsgTypeOK
-----------------------------------------------------------------------------
\* For each write, the commit_ts should be strictly greater than
\* the start_ts. For each rollback, the commit_ts should equals to
\* the start_ts.
WriteConsistency ==
\A k \in KEY:
\A rec \in key_write[k] :
\/ /\ rec.type = "write"
/\ rec.ts > rec.start_ts
/\ \E d \in key_data[k] : rec.start_ts = d.ts
\/ /\ rec.type = "rollback"
/\ rec.ts = rec.start_ts
LockConsistency ==
\A k \in KEY :
\* There should be at most one lock for each key.
/\ Cardinality(key_lock[k]) <= 1
\* When the lock exists, there cannot be a corresponding commit record
/\ \A l \in key_lock[k] :
~ \E w \in key_write[k] : w.start_ts = l.ts
CommittedClientConsistency ==
\A c \in CLIENT :
LET
start_ts == client_ts[c].start_ts
commit_ts == client_ts[c].commit_ts
primary == client_key[c].primary
IN
\* When the client considers it's committed, its primary key must be committed
client_state[c] = "committed" =>
\E w \in key_write[primary] :
/\ w.start_ts = start_ts
/\ w.type = "write"
/\ w.commit_ts = commit_ts
\* If a client is aborted, there should be no committed primary key.
AbortedClientConsistency ==
\A c \in CLIENT :
client_state[c] = "aborted" =>
~ \E w \in key_write[client_key[c].primary] :
/\ w.start_ts = client_ts[c].start_ts
/\ w.type = "write"
CommittedTxnConsistency ==
\A c \in CLIENT :
client_state[c] /= "init" =>
LET
primary == client_key[c].primary
secondary == client_key[c].secondary
start_ts == client_ts[c].start_ts
IN
\A wp \in key_write[primary] :
\* If the primary key is committed, the secondary keys of the same transaction
\* must be either committed or locked
wp.start_ts = start_ts /\ wp.type = "write" =>
\A s \in secondary :
\/ \E l \in key_lock[s] : l.ts = start_ts
\/ \E ws \in key_write[s] : ws.start_ts = start_ts /\ ws.type = "write"
\* For each transaction, we cannot have both committed and rolled back keys.
RollbackConsistency ==
\A start_ts \in {client_ts[c].start_ts : c \in CLIENT} :
(\E k \in KEY :
\E w \in key_write[k] : w.start_ts = start_ts /\ w.type = "rollback") =>
\A k2 \in KEY :
~ \E w2 \in key_write[k2] : w2.start_ts = start_ts /\ w2.type = "write"
\* For each key, each write or rollback record in write column should have a
\* unique start_ts.
UniqueWrite ==
\A k \in KEY :
Cardinality({w.start_ts : w \in key_write[k]}) = Cardinality(key_write[k])
-----------------------------------------------------------------------------
THEOREM Safety ==
PessimisticSpec => [](/\ TypeOK
/\ WriteConsistency
/\ LockConsistency
/\ CommittedTxnConsistency
/\ AbortedClientConsistency
/\ RollbackConsistency
/\ UniqueWrite)
=============================================================================

69
PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test1.launch
View File

@ -1,69 +0,0 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.lamport.tla.toolbox.tool.tlc.modelCheck">
<stringAttribute key="TLCCmdLineParameters" value=""/>
<intAttribute key="collectCoverage" value="1"/>
<stringAttribute key="configurationName" value="Test1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
<booleanAttribute key="dfidMode" value="false"/>
<intAttribute key="distributedFPSetCount" value="0"/>
<stringAttribute key="distributedNetworkInterface" value="10.0.75.1"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="3"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="63"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value="Init"/>
<stringAttribute key="modelBehaviorNext" value="Next"/>
<stringAttribute key="modelBehaviorSpec" value=""/>
<intAttribute key="modelBehaviorSpecType" value="2"/>
<stringAttribute key="modelBehaviorVars" value="msg, key_data, key_lock, next_ts, client_state, key_last_read_ts, client_key, client_ts, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="false"/>
<listAttribute key="modelCorrectnessInvariants">
<listEntry value="0TypeOK"/>
<listEntry value="1WriteConsistency"/>
<listEntry value="1LockConsistency"/>
<listEntry value="1CommittedTxnConsistency"/>
<listEntry value="1AbortedClientConsistency"/>
<listEntry value="1RollbackConsistency"/>
<listEntry value="1NextTsTypeOK"/>
<listEntry value="1&#13;&#10;ClientStateTypeOK"/>
<listEntry value="1&#13;&#10;ClientTsTypeOK"/>
<listEntry value="1&#13;&#10;ClientKeyTypeOK"/>
<listEntry value="1&#13;&#10;KeyDataTypeOK"/>
<listEntry value="1&#13;&#10;KeyLockTypeOK"/>
<listEntry value="1&#13;&#10;KeyWriteTypeOK"/>
<listEntry value="1UniqueWrite"/>
</listAttribute>
<listAttribute key="modelCorrectnessProperties"/>
<intAttribute key="modelEditorOpenTabs" value="14"/>
<stringAttribute key="modelExpressionEval" value=""/>
<stringAttribute key="modelParameterActionConstraint" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;1"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k2};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1, c2};1;1"/>
<listEntry value="OPTIMISTIC_CLIENT;;{};0;0"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k2;0;0"/>
</listAttribute>
<stringAttribute key="modelParameterContraint" value=""/>
<listAttribute key="modelParameterDefinitions"/>
<stringAttribute key="modelParameterModelValues" value="{}"/>
<stringAttribute key="modelParameterNewDefinitions" value=""/>
<intAttribute key="modelVersion" value="20191005"/>
<intAttribute key="numberOfWorkers" value="10"/>
<booleanAttribute key="recover" value="false"/>
<stringAttribute key="result.mail.address" value=""/>
<intAttribute key="simuAril" value="-1"/>
<intAttribute key="simuDepth" value="100"/>
<intAttribute key="simuSeed" value="-1"/>
<stringAttribute key="specName" value="PessimisticTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
<stringAttribute key="view" value=""/>
<booleanAttribute key="visualizeStateGraph" value="false"/>
</launchConfiguration>

31
PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test2.launch
View File

@ -1,31 +0,0 @@
<?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="192.168.220.40"/>
<intAttribute key="distributedNodesCount" value="1"/>
<stringAttribute key="distributedTLC" value="off"/>
<intAttribute key="fpIndex" value="27"/>
<intAttribute key="maxHeapSize" value="25"/>
<stringAttribute key="modelBehaviorInit" value="Init"/>
<stringAttribute key="modelBehaviorNext" value="Next"/>
<stringAttribute key="modelBehaviorSpec" value=""/>
<intAttribute key="modelBehaviorSpecType" value="2"/>
<stringAttribute key="modelBehaviorVars" value="msg, key_data, key_lock, next_ts, client_state, key_last_read_ts, client_key, client_ts, key_write"/>
<stringAttribute key="modelComments" value=""/>
<booleanAttribute key="modelCorrectnessCheckDeadlock" value="true"/>
<listAttribute key="modelCorrectnessInvariants"/>
<listAttribute key="modelCorrectnessProperties"/>
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;1"/>
<listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1} @@ c3 :&gt; {k2};0;0"/>
<listEntry value="PESSIMISTIC_CLIENT;;{c1};1;1"/>
<listEntry value="OPTIMISTIC_CLIENT;;{c2, c3};1;1"/>
<listEntry value="CLIENT_PRIMARY;;c1 :&gt; k1 @@ c2 :&gt; k1 @@ c3 :&gt; k2;0;0"/>
</listAttribute>
<intAttribute key="numberOfWorkers" value="6"/>
<stringAttribute key="result.mail.address" value=""/>
<stringAttribute key="specName" value="PessimisticTransaction"/>
<stringAttribute key="tlcResourcesProfile" value="local custom"/>
</launchConfiguration>

33
PessimisticTransaction/Test1.cfg
View File

@ -1,33 +0,0 @@
\* See Test1.tla.
CONSTANT
KEY <- Key
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_KEY <- ClientKey
CLIENT_PRIMARY <- ClientPrimary
INIT
Init
NEXT
Next
INVARIANT
NextTsTypeOK
ClientStateTypeOK
ClientTsTypeOK
ClientKeyTypeOK
KeyDataTypeOK
KeyLockTypeOK
KeyWriteTypeOK
KeyLastReadTsTypeOK
MsgTypeOK
INVARIANT
WriteConsistency
LockConsistency
CommittedTxnConsistency
AbortedClientConsistency
RollbackConsistency
UniqueWrite

19
PessimisticTransaction/Test1.tla
View File

@ -1,19 +0,0 @@
--------------------------------- MODULE Test1 ---------------------------------
EXTENDS PessimisticTransaction, TLC
\* Model value is not used to avoid unnecessary state space
\* checked by TLC. Symmetry should not be used if we are supposed
\* to check liveness.
k1 == 1
k2 == 2
c1 == 1
c2 == 2
Key == {k1, k2}
OptimistiicClient == {}
PessimisticClient == {c1, c2}
ClientKey == c1 :> {k1, k2} @@ c2 :> {k2}
ClientPrimary == c1 :> k1 @@ c2 :> k2
================================================================================

33
PessimisticTransaction/Test2.cfg
View File

@ -1,33 +0,0 @@
\* See Test2.tla.
CONSTANT
KEY <- Key
OPTIMISTIC_CLIENT <- OptimistiicClient
PESSIMISTIC_CLIENT <- PessimisticClient
CLIENT_KEY <- ClientKey
CLIENT_PRIMARY <- ClientPrimary
INIT
Init
NEXT
Next
INVARIANT
NextTsTypeOK
ClientStateTypeOK
ClientTsTypeOK
ClientKeyTypeOK
KeyDataTypeOK
KeyLockTypeOK
KeyWriteTypeOK
KeyLastReadTsTypeOK
MsgTypeOK
INVARIANT
WriteConsistency
LockConsistency
CommittedTxnConsistency
AbortedClientConsistency
RollbackConsistency
UniqueWrite

20
PessimisticTransaction/Test2.tla
View File

@ -1,20 +0,0 @@
--------------------------------- MODULE Test2 ---------------------------------
EXTENDS PessimisticTransaction, TLC
\* Model value is not used to avoid unnecessary state space
\* checked by TLC. Symmetry should not be used if we are supposed
\* to check liveness.
k1 == 1
k2 == 2
c1 == 1
c2 == 2
c3 == 3
Key == {k1, k2}
OptimistiicClient == {c2, c3}
PessimisticClient == {c1}
ClientKey == c1 :> {k1, k2} @@ c2 :> {k1} @@ c3 :> {k2}
ClientPrimary == c1 :> k1 @@ c2 :> k1 @@ c3 :> k2
================================================================================