[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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

On Friday, April 19, 2024 at 3:19:18 PM UTC+9 idivyans...@xxxxxxxxx wrote:
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

--
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/a15b587f-f61a-476f-bfc9-2bb88cf051f3n%40googlegroups.com.