----------------------------- MODULE WoundWait -----------------------------
EXTENDS TLC, FiniteSets, Integers, Sequences
CONSTANT txs, tuples
VARIABLE txActive, txAbort, txRequest, tupleOwners, tupleWaiters
----------------------------------------------------------------------------
Vars == <<txActive, txAbort, txRequest, tupleOwners, tupleWaiters>>
RequestType == {"SH", "EX"}
TypeOK ==
/\ \A tx \in txs: txRequest[tx] \in RequestType
/\ \A tuple1 \in tuples: tupleOwners[tuple1] \subseteq txs
/\ \A tuple2 \in tuples: tupleWaiters[tuple2] \subseteq txs
/\ txActive \subseteq txs
/\ txAbort \subseteq txs
Init ==
/\ txActive = {}
/\ txAbort = {}
/\ txRequest = [tx \in txs |-> RandomElement(RequestType)]
/\ tupleOwners = [tuple1 \in tuples |-> {}]
/\ tupleWaiters = [tuple2 \in tuples |-> {}]
----------------------------------------------------------------------------
HasConflict(req1, req2) == (req1 = "EX") \/ (req2 = "EX")
Min(W) ==
/\ W # {}
/\ CHOOSE tx \in W: \A tx2 \in W: tx <= tx2
SetAbort(tx) ==
/\ txAbort' = txAbort \cup {tx}
/\ \E tx1 \in txActive:
/\ tx = tx1
/\ txActive' = txActive \ {tx1}
SetActive(tx) ==
/\ IF \E tx0 \in txActive: tx = tx0
THEN UNCHANGED <<txActive>>
ELSE txActive' = txActive \cup {tx}
/\ \E tx1 \in txAbort: tx = tx1
/\ txAbort' = txAbort \ {tx1}
----------------------------------------------------------------------------
Sort(set) ==
IF set = {} THEN {}
ELSE
CHOOSE sortedSet \in SUBSET set :
/\ sortedSet \subseteq set
/\ \A x \in sortedSet, y \in sortedSet : x <= y
AddWaiter(tx, tuple) ==
/\ tupleWaiters' = [tupleWaiters EXCEPT ![tuple]
= Sort(tupleWaiters[tuple] \cup {tx})]
/\ UNCHANGED <<tupleOwners, txAbort, txActive, txRequest>>
RemoveWaiter(tx, tuple) ==
tupleWaiters' = [tupleWaiters EXCEPT ![tuple]
= tupleWaiters[tuple] \ {tx}]
AddOwner(tx, tuple) ==
/\ tupleOwners' = [tupleOwners EXCEPT ![tuple]
= tupleOwners[tuple] \cup {tx}]
/\ UNCHANGED <<tupleWaiters, txAbort, txRequest>>
RemoveOwner(tx, tuple) ==
tupleOwners' = [tupleOwners EXCEPT ![tuple]
= tupleOwners[tuple] \ {tx}]
PromoteWaiter(tuple) == \E tx \in tupleWaiters[tuple]:
/\ tx = Min(tupleWaiters[tuple])
/\ HasConflict(txRequest[tx],txRequest[tupleOwners[tuple]]) = FALSE
/\ RemoveWaiter(tx, tuple)
/\ AddOwner(tx, tuple)
/\ SetActive(tx)
LockAcquire(tx, req, tuple) ==
\/ /\ tupleOwners[tuple] = {}
/\ AddWaiter(tx, tuple)
\/ /\ tupleOwners[tuple] # {}
/\ \A tx1 \in tupleOwners[tuple]:
/\ HasConflict(req,txRequest[tx1])
/\ (tx < tx1)
/\ SetAbort(tx1)
/\ UNCHANGED <<txActive, txRequest, tupleOwners, tupleWaiters>>
/\ AddWaiter(tx, tuple)
/\ HasConflict(txRequest[Min(tupleWaiters'[tuple])],
txRequest[tupleOwners[tuple]]) = FALSE
/\ RemoveWaiter(Min(tupleWaiters'[tuple]), tuple)
/\ AddOwner(Min(tupleWaiters'[tuple]), tuple)
/\ SetActive(Min(tupleWaiters'[tuple]))
LockRelease(tx, tuple) ==
/\ RemoveOwner(tx, tuple)
/\ PromoteWaiter(tuple)
/\ tx' = tx + Len(txActive)
----------------------------------------------------------------------------
Next == \E tx \in txs: \E tuple \in tuples:
\/ LockAcquire(tx, txRequest[tx], tuple)
\/ LockRelease(tx, tuple)
Spec ==
/\ Init
/\ [][Next]_Vars
(*
FairSpec ==
Spec /\ \A tx1 \in txs, tuple1 \in tuples:
WF_Vars(LockAcquire(tx1, txRequest[tx1], tuple1))
/\ \A tx2 \in txs, tuple2 \in tuples:
SF_Vars(LockRelease(tx2, tuple2))
*)
----------------------------------------------------------------------------
DeadLock == \A tuple \in tuples: tupleWaiters[tuple] # txs
(*
BaitInva == \A tuple \in tuples: tupleOwners[tuple] # txs
Starvation ==
/\ \A tx1 \in txs, tuple1 \in tuples:
[]<>(<<LockAcquire(tx1, txRequest[tx1], tuple1)>>_Vars)
/\ \A tx2 \in txs, tuple2 \in tuples:
[]<>(<<LockRelease(tx2,tuple2)>>_Vars)
*)
=============================================================================