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

[Stephan Merz <stepha...@xxxxxxxxx>]

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

> On 15 Jul 2018, at 08:04, Somesh Chandra <chandra...@xxxxxxxxx> wrote:
> 
> 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
> 
> -- 
> 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.