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

implement collapse rollback

Browse Source 
Signed-off-by: Yilin Chen <sticnarf@gmail.com>
This commit is contained in:
Yilin Chen 2019-10-25 16:45:24 +08:00
parent be9ddc9e7a
commit c9af93cee7
No known key found for this signature in database
GPG Key ID: 353E7ED34BF326E0
2 changed files with 21 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
PessimisticTransaction/PessimisticTransaction.tla
View File

@ -71,6 +71,15 @@ Range(m) == {m[i] : i \in DOMAIN m}
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) ==
\* If the existing lock has the same ts, unlock it.
@ -79,9 +88,10 @@ rollback(k, ts) ==
ELSE UNCHANGED key_lock
/\ key_data' = [key_data EXCEPT ![k] = @ \ {[ts |-> ts]}]
\* Write a rollback in the write column.
\* TODO: collapse rollback
/\ key_write' = [key_write EXCEPT
![k] = @ \union {[ts |-> ts, type |-> "rollback", start_ts |-> ts]}]
![k] = (@ \ {w \in latestHistoryWrite(k, ts) : w.type = "rollback"}) \* collapse rollback
\union {[ts |-> ts, type |-> "rollback", start_ts |-> ts]}]
\* Commit key k
commit(k, start_ts, commit_ts) ==
@ -377,19 +387,10 @@ ServerOp ==
\/ DoCommit
Read ==
\* Read by a running transaction
\/ \E c \in CLIENT :
/\ client_state[c] = "working"
/\ \E k \in KEY :
msg' = msg \union
{[type |-> "read", key |-> k, ts |-> client_ts[c].start_ts]}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
\* When all transactions are finished, we read all keys with latest TS
\/ /\ \A c \in CLIENT : client_state[c] \in {"committed", "aborted", "undetermined"}
/\ \E k \in KEY :
msg' = msg \union
{[type |-> "read", key |-> k, ts |-> next_ts]}
/\ UNCHANGED <<next_ts, client_vars, key_vars>>
\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
@ -454,8 +455,7 @@ MsgTypeInv ==
[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] \union
[type : {"rollback"}, key : SUBSET KEY, start_ts: Pos]
[type : {"resolve"}, primary : KEY, start_ts : Pos, commit_ts : Nat]
)
TypeInvariant ==

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

@ -1,7 +1,7 @@
<?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"/>
<intAttribute key="collectCoverage" value="0"/>
<stringAttribute key="configurationName" value="Test1"/>
<booleanAttribute key="deferLiveness" value="false"/>
<intAttribute key="dfidDepth" value="100"/>
@ -12,9 +12,9 @@
<stringAttribute key="distributedTLC" value="off"/>
<stringAttribute key="distributedTLCVMArgs" value=""/>
<intAttribute key="fpBits" value="1"/>
<intAttribute key="fpIndex" value="122"/>
<intAttribute key="fpIndex" value="84"/>
<booleanAttribute key="fpIndexRandom" value="true"/>
<intAttribute key="maxHeapSize" value="73"/>
<intAttribute key="maxHeapSize" value="75"/>
<intAttribute key="maxSetSize" value="1000000"/>
<booleanAttribute key="mcMode" value="true"/>
<stringAttribute key="modelBehaviorInit" value="Init"/>
@ -38,7 +38,7 @@
<stringAttribute key="modelExpressionEval" value=""/>
<listAttribute key="modelParameterConstants">
<listEntry value="KEY;;{k1, k2};1;1"/>
<listEntry value="CLIENT;;{c1};1;1"/>
<listEntry value="CLIENT;;{c1, c2};1;1"/>
</listAttribute>
<intAttribute key="numberOfWorkers" value="12"/>
<booleanAttribute key="recover" value="false"/>