implement optimistic transaction

Signed-off-by: Yilin Chen <sticnarf@gmail.com>

PessimisticTransaction/PessimisticTransaction.tla

@@ -109,7 +109,6 @@ rollback(k, ts) ==
   /\ key_write' = [key_write EXCEPT
        ![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) ==
@@ -136,6 +135,20 @@ undetermine(c) ==
   
 -----------------------------------------------------------------------------
 
+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
@@ -165,7 +178,7 @@ LockKey(c) ==
                start_ts |-> client_ts[c].start_ts, for_update_ts |-> client_ts[c].for_update_ts]}
          /\ UNCHANGED <<next_ts, client_vars, key_vars>>
        
-PessimisticPrewrite(c) ==
+Prewrite(c) ==
   /\ client_state[c] = "prewriting"
   /\ IF client_key[c].pending = {}
      THEN
@@ -195,11 +208,16 @@ Commit(c) ==
          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)
-  \/ PessimisticPrewrite(c)
+  \/ Prewrite(c)
   \/ Commit(c)
   \* Committing secondary keys is ommitted
   
@@ -339,7 +357,39 @@ DoLockKey ==
               /\ 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"
@@ -400,6 +450,7 @@ ServerOp ==
   \/ DoCleanup
   \/ DoResolve
   \/ DoLockKey
+  \/ DoOptimisticPrewrite
   \/ DoPessimisticPrewrite
   \/ DoCommit
  
@@ -424,6 +475,7 @@ Init ==
 
 Next == 
   \/ ServerOp
+  \/ \E c \in OPTIMISTIC_CLIENT : OptimisticClientOp(c)
   \/ \E c \in PESSIMISTIC_CLIENT : PessimisticClientOp(c)
   \/ Read
   
@@ -468,7 +520,7 @@ KeyLastReadTsTypeInv ==
 MsgTypeInv ==
   msg \subseteq (
     [c : CLIENT, type : {"lock", "prewrite"}, key : KEY, primary: KEY,
-     start_ts : Pos, for_update_ts : Pos] \union
+     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

PessimisticTransaction/PessimisticTransaction.toolbox/PessimisticTransaction___Test2.launch

@@ -0,0 +1,57 @@
+<?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="Test2"/>
+    <booleanAttribute key="deferLiveness" value="false"/>
+    <intAttribute key="dfidDepth" value="100"/>
+    <booleanAttribute key="dfidMode" value="false"/>
+    <intAttribute key="distributedFPSetCount" value="0"/>
+    <stringAttribute key="distributedNetworkInterface" value="192.168.220.40"/>
+    <intAttribute key="distributedNodesCount" value="1"/>
+    <stringAttribute key="distributedTLC" value="off"/>
+    <stringAttribute key="distributedTLCVMArgs" value=""/>
+    <intAttribute key="fpBits" value="1"/>
+    <intAttribute key="fpIndex" value="0"/>
+    <booleanAttribute key="fpIndexRandom" value="true"/>
+    <intAttribute key="maxHeapSize" value="75"/>
+    <intAttribute key="maxSetSize" value="1000000"/>
+    <booleanAttribute key="mcMode" value="true"/>
+    <stringAttribute key="modelBehaviorInit" value="Init"/>
+    <stringAttribute key="modelBehaviorNext" value="Next"/>
+    <stringAttribute key="modelBehaviorSpec" value="PessimisticSpec"/>
+    <intAttribute key="modelBehaviorSpecType" value="1"/>
+    <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">
+        <listEntry value="1TypeInvariant"/>
+        <listEntry value="1WriteConsistency"/>
+        <listEntry value="1LockConsistency"/>
+        <listEntry value="1CommittedTxnConsistency"/>
+        <listEntry value="1RollbackConsistency"/>
+        <listEntry value="1UniqueWrite"/>
+        <listEntry value="1AbortedClientConsistency"/>
+    </listAttribute>
+    <listAttribute key="modelCorrectnessProperties"/>
+    <intAttribute key="modelEditorOpenTabs" value="4"/>
+    <stringAttribute key="modelExpressionEval" value=""/>
+    <listAttribute key="modelParameterConstants">
+        <listEntry value="KEY;;{k1, k2};1;1"/>
+        <listEntry value="CLIENT;;{c1, c2};1;1"/>
+        <listEntry value="PESSIMISTIC_CLIENT;;{};0;0"/>
+        <listEntry value="OPTIMISTIC_CLIENT;;{c1, c2};0;0"/>
+        <listEntry value="CLIENT_KEY;;c1 :&gt; {k1, k2} @@ c2 :&gt; {k1};0;0"/>
+        <listEntry value="CLIENT_PRIMARY;;c1 :&gt; k2 @@ c2 :&gt; k1;0;0"/>
+    </listAttribute>
+    <intAttribute key="numberOfWorkers" value="12"/>
+    <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>