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 NguyenOn 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 stateit 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