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

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

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/6eefc83f-e957-4e79-93fd-c6469512d34cn%40googlegroups.com.