[tlaplus] Deadlock reach without invocation of main actions.

[Tung Nguyen <tungnguyen173371@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/151bc74d-c21d-45dc-934a-2dba7c837eaen%40googlegroups.com.