Understanding why specification hits deadlock upon initialization

[Somesh Chandra]

Hello,

I am attempting to write my first example specification using TLA+, for which TLC immediately reports deadlock at the initial state.

My specification is pasted below and i provided following input.

workers: { "w1" , "w2" }
locks: { "l1", "l2" }

---------------------------- MODULE Liveness ----------------------------
\* Specification for multiple workers, which will attempt to acquire all free locks.
\* We need to ensure that
\* 1) Safety: At most one worker can acquire all locks at any give time.
\* 2) Liveness: All workers should eventualy acquire all locks.
EXTENDS TLC, FiniteSets

CONSTANT workers, locks \* The set of participating resources
VARIABLE wState, lState, lOwner \* Track state of resources.

DLTypeOK == \A w \in workers : wState[w] \in { "free", "acquired" } /\
\A l1 \in locks : lState[l1] \in { "free", "acquired" } /\
\A l2 \in locks : lOwner[l2] \in workers \cup { "none" }

DLInit == wState = [ w \in workers |-> "free" ] /\
lState = [ l \in locks |-> "free" ] /\
lOwner = [ l \in locks |-> "none" ]

CanAcquire(w,l) == lState[l] = "free" \/ \* Lock is free to be acquired by any worker
(lState[l] = "acquired" /\ lOwner[l] = w ) \* Renew: Lock re-acquired by same worker.

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

AcquireLock(w,l) == CanAcquire(w,l) /\
lState' = [lState EXCEPT ![l] = "acquired"] /\
lOwner' = [lOwner EXCEPT ![l] = w] /\
IF (\A l1 \in locks: (\/ lOwner[l1] = w))
THEN AcquiredAllLocks(w)
ELSE wState' = wState

ReleaseLock(w,l) == lOwner[l] = w /\
lOwner' = [lOwner EXCEPT ![l] = "none"] /\
lState' = [lState EXCEPT ![l] = "free"] /\
wState' = [wState EXCEPT ![w] = "free"] \* As soon as a single lock is released, we should assume that the worker is free.

\* One or more worker can attempt to acquire or release all locks, if possible.
DLNext == \/ \E w \in workers : \A l \in locks : (\/ AcquireLock(w,l) \/ ReleaseLock(w,l))

\* No 2 workers can be in "acquired" state at the same time
DLMutualExclusion == \A w1, w2 \in workers : ~ ([](/\ w1 # w2
/\ wState[w1] = "acquired"
/\ wState[w2] = "acquired"))

\* Eventually all workers should get a chance to acquire lock
\* TODO: How should TLC be told to check this?
DLStarvationFree == \A w \in workers : []<>(wState[w] = "acquired")

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

Vars == <<wState, lState, lOwner>>

DLSpec == /\ DLInit
/\ [][DLNext]_Vars
/\ DLStarvationFree
=============================================================================

My assumption is that TLC should pick first worker and then attempt to acquire all locks and then release all locks, and repeat the same for second worker.

What am i doing wrong to hit a deadlock during the init state itself?

Thanks
Somesh

[Stephan Merz]

Hello,

your next-state relation is defined as

DLNext == \/ \E w \in workers : \A l \in locks : (\/ AcquireLock(w,l) \/ ReleaseLock(w,l))

I presume that "\A" should be "\E". For example, action AcquireLock attempts to acquire one lock but cannot acquire all of them.

Hope this helps,
Stephan

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

[Somesh Chandra]

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?

[Stephan Merz]

Hello,

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.

Regards,

Stephan