[tlaplus] Re: Deadlock reach without invocation of main actions.

On Friday, April 19, 2024 at 9:32:46 AM UTC+5:30 Tung Nguyen wrote:

Hi!

I am trying to specify a preemptive locking protocol for multiple transactions and tuples. In which, a transaction with a smaller ID is allowed to preempt the current lock holder, and a transaction with a larger ID needs to wait for the current lock holder to release.

I want to check the liveness property of it but before that, the specification ran into a Deadlock reach but the error trace shows no invocation of any actions in Next at all (I commented out all liveness checking code). I am quite confused... Can you please kindly let me know if there is anything I did wrong?

Here is my spec:
----------------------------- 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) == 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) ==
/\ 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})]

RemoveWaiter(tx, tuple) ==
tupleWaiters' = [tupleWaiters EXCEPT ![tuple] = tupleWaiters[tuple] \ {tx}]

AddOwner(tx, tuple) ==
tupleOwners' = [tupleOwners EXCEPT ![tuple] = tupleOwners[tuple] \cup {tx}]

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) ==
/\ \A tx1 \in tupleOwners[tuple]:
/\ HasConflict(req,txRequest[tx1])
/\ (tx < tx1)
/\ SetAbort(tx1)
/\ UNCHANGED <<txActive, txRequest, tupleOwners, tupleWaiters>>
/\ AddWaiter(tx, tuple)
/\ PromoteWaiter(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:
WF_Vars(LockRelease(tx2, tuple2))
*)
----------------------------------------------------------------------------

DeadLock == \A tuple \in tuples: tupleWaiters[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)
*)
=============================================================================

And here are the cfg:
CONSTANTS
tuples = {t1, t2, t3, t4}
txs = {1, 2, 3}

INVARIANT TypeOK DeadLock
\*SPECIFICATION FairSpec
SPECIFICATION Spec
\*CHECK_DEADLOCK FALSE
\*PROPERTY Starvation

Thank you very much!
Best,
Tung Nguyen