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

Re: [tlaplus] Understanding why specification hits deadlock upon initialization


remember that you are trying to check an implication of the form

DLSpec => Property

I am assuming that the liveness property that you are interested in is DLStarvationFree, which asserts that for every worker w, infinitely often you have wState[w] = "acquired". Your fairness property DLFairness is expressed in terms of the action AcquiredAllLocks(w), defined as

AcquiredAllLocks(w) == wState' = [wState EXCEPT ![w] = "acquired"]

Note that this action has a trivial enabledness condition, hence the fairness condition boils down to

\A w \in workers : []<><< wState' = [wState EXCEPT ![w] = "acquired"] >>_wState

and this trivially implies property DLStarvationFree, whatever the rest of your specification may be.

The problem is that your fairness condition is too strong: you wouldn't know how to implement it in the actual system. It is good practice to assert only fairness conditions that appear as disjuncts of the next-state relation. In your example, a reasonable fairness condition could be

  /\ \A w \in workers, l \in locks : WF_Vars(AcquireLock(w,l))
  /\ \A w \in workers, l \in locks : WF_Vars(ReleaseLock(w,l))

When you use this, TLC will generate a useful (though quite obvious) counter-example, even for the unmodified specification.


On 17 Jul 2018, at 05:51, Somesh Chandra <chandra...@xxxxxxxxx> wrote:

Thanks. That makes sense and fixed the problem. While the safety checks work now, i don't think the liveness check is working as expected.'

In the same spec, i have the following function to ensure that eventually all workers should have acquired all locks.

  DLFairness == \A w \in workers : WF_<<wState>>(AcquiredAllLocks(w))

I have the fairness check added in the spec as following.
  DLSpec == /\ DLInit
         /\ [][DLNext]_Vars
         /\ DLFairnes

I intentionally added a bug in the AcquireLock function to skip "w1"
  AcquireLock(w,l) == CanAcquire(w,l) /\
                   w # "w1" /\  \* Intentional bug to verify liveness check
                   lState' = [lState EXCEPT ![l] = "acquired"] /\
                   lOwner' = [lOwner EXCEPT ![l] = w] /\
                   IF (\A l1 \in locks: (\/ lOwner[l1] = w))
                           THEN AcquiredAllLocks(w)
                           ELSE wState' = wState

However TLC successfully evaluated the spec "DLSpec" without catching the violation of fairness _expression_ for "w1" worker. Why so?

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.