Deadlock reach without invocation of main actions.

Tung Nguyen

unread,

Apr 19, 2024, 12:02:46 AM4/19/24

to tlaplus

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

idivyans...@gmail.com

unread,

Apr 19, 2024, 1:43:05 AM4/19/24

to tlaplus

There are problems in how atomic actions are defined in spec.

Take for example

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)

AddWaiter and PromoteWaiter should be different actions. From initial state

it is not possible to get an execution trace which satisfies LockAcquire action.

AddWaiter says that in the next state `tx` will be added in waiters of `tuple` but
PromoteWaiter expects that `tx` is in waiters of `tuple` in current state by usage of
tx = Min(tupleWaiters[tuple]).

Thanks and regards

Divyanshu Ranjan

idivyans...@gmail.com

unread,

Apr 19, 2024, 2:19:18 AM4/19/24

to tlaplus

There are problems in how atomic actions are defined in spec.

Take for example

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)

AddWaiter and PromoteWaiter should be different actions. From initial state
it is not possible to get an execution trace which satisfies LockAcquire action.
AddWaiter says that in the next state `tx` will be added in waiters of `tuple` but
PromoteWaiter expects that `tx` is in waiters of `tuple` in current state by usage of
tx = Min(tupleWaiters[tuple]).

Correction : But there is no transaction to promote as tupleWaiters[tuple] is empty. PromoteWaiter
is evaluates to FALSE for any state transition (s, s') where s is initial state. Hence it is deadlock

Tung Nguyen

unread,

Apr 19, 2024, 2:49:02 AM4/19/24

to tlaplus

Hi! Thank you for your answer and clarification!

I have modified the LockAcquire action so that it will directly add tx to the tupleWaiters[tuple] if the waitlist is empty:

LockAcquire(tx, req, tuple) == 
    \/ /\ tupleWaiters[tuple] = {}
       /\ AddWaiter(tx, tuple)
    \/ /\ tupleWaiters[tuple] # {}

       /\  \A tx1 \in tupleOwners[tuple]: 
            /\ HasConflict(req,txRequest[tx1]) 
            /\ (tx < tx1)
            /\ SetAbort(tx1)
            /\ UNCHANGED <<txActive, txRequest, tupleOwners, tupleWaiters>>
        /\ AddWaiter(tx, tuple)
        /\ PromoteWaiter(tuple)

The deadlock situation has disappeared and it ran successfully. However, when I checked the traces, only the LockAcquire action was invoked and there was no LockReLease. Even when I used the FairSpec with week fairness. Can you kindly let me know why did this behavior happen?

Best regards,
Tung Nguyen

Stephan Merz

unread,

Apr 19, 2024, 2:57:04 AM4/19/24

to tlaplus

As pointed out in the previous reply, the conjunction AddWaiter(tx, tuple) /\ PromoteWaiter(tuple) can never be true:

AddWaiter adds an element to tupleWaiters whereas PromoteWaiter implies RemoveWaiter, which makes an

incompatible change to the same variable. Moreover, the first disjunct of the new version of LockAcquire does

not define values for all state variables in the successor state.

There are more problems with this spec, for example Sort(set) may always yield {}, which is probably not what

you intend.

Tung Nguyen

unread,

Apr 19, 2024, 9:55:37 AM4/19/24

to tlaplus

Thank you very much for your input! I am learning a lot from this process!
Here is my silly attempt to not let AddWaiter(tx, tuple) and PromoteWaiter(tuple) be in atomic conjunctions.
Also, values for all state variables are added in the AddWaiter function.

The TLC still does not show any of LockRelease in the traces and just acquires all the lock and idling I think. Can kindly you help me understand these behaviors?

Updated 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) == 

    /\ 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)
*)
=============================================================================

Best regards,
Tung Nguyen

Message has been deleted

Stephan Merz

unread,

Apr 20, 2024, 2:57:08 AM4/20/24

to tla...@googlegroups.com

Another advice: in the initial condition, instead of

    /\ txRequest = [tx \in txs |-> RandomElement(RequestType)] 

write

    /\ txRequest \in [txs -> RequestType] 

This will cause the model checker to consider all possible combinations of requests instead of just one randomly chosen one.

On Apr 20, 2024, at 08:31, idivyans...@gmail.com <idivyans...@gmail.com> wrote:

These are issues I am facing when I am trying to run this spec.

- Definition of sort is wrong; it can always return {} as pointed out by Stephan Merz.
- Definition of Min is wrong as this is conjunction of boolean expression and integer
- In HasConflict(txRequest[tx],txRequest[tupleOwners[tuple]]) , tupleOwners[tuple] is set whereas txRequest is mapping from integer to RequestTypes

That is how far I looked. I advise you to check the expression you are writing with TLA+ Evaluate Expression tool to check if this is what you intend.

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/921bb42d-d870-4ba1-b2a0-efc322e80f4an%40googlegroups.com.

Reply all

Reply to author

Forward