Reproducing deadlock in TLA+

[dmitry....@gmail.com]

I'm trying to reproduce a deadlock from Herlihy's "The Art of Multiprocessor Programming" in TLA+. In the following code when a thread wants to acquire a lock it marks itself as a victim and proceed only when another thread becomes a victim. There is a deadlock here if another thread never comes.

```
class LockTwo implements Lock {
  private int victim;
 
  public void lock() {
    int i = ThreadID.get();
    victim = i; // let the other go first
    while (victim == i) {} // wait
  }
 
  public void unlock() {}
}
```

The TLA+ spec is as follows:

```
------------------------------ MODULE LockTwo ------------------------------
 
CONSTANT Thread
 
VARIABLE victim, owner, wasVictim
 
Null == CHOOSE v: v \notin Thread
 
Init ==
  /\ victim = Null
  /\ owner = [t \in Thread |-> FALSE]
  /\ wasVictim = [t \in Thread |-> FALSE]
 
TypeOK ==
  /\ victim \in Thread \cup {Null}
  /\ owner \in [Thread -> BOOLEAN]
  /\ wasVictim \in [Thread -> BOOLEAN]
 
BecomeVictim(t) ==
  /\ wasVictim[t] = FALSE
  /\ owner[t] = FALSE
  /\ victim' = t
  /\ wasVictim' = [wasVictim EXCEPT ![t] = TRUE]
  /\ UNCHANGED owner
 
AcquireLock(t) ==
  /\ wasVictim[t] = TRUE
  /\ victim # t
  /\ owner' = [owner EXCEPT ![t] = TRUE]
  /\ wasVictim' = [wasVictim EXCEPT ![t] = FALSE]
  /\ UNCHANGED victim
 
ReleaseLock(t) ==
  /\ owner[t] = TRUE
  /\ owner' = [owner EXCEPT ![t] = FALSE]
  /\ UNCHANGED <<victim, wasVictim>>
 
Next ==
  \E t \in Thread: BecomeVictim(t) \/ AcquireLock(t) \/ ReleaseLock(t)
 
MutualExclusion ==
  \A t1, t2 \in Thread: (t1 # t2) => ~ (owner[t1] /\ owner[t2])
 
EventualSuccess ==
  \A t \in Thread: (victim = t) ~> owner[t]
 
Spec == Init /\ [][Next]_<<victim, owner, wasVictim>> /\ EventualSuccess
 
=============================================================================
```

TLA spec runs fine with Thread = {t1, t2} where t1 and t2 are model values.

How to make TLA to report a deadlock when one thread wants to lock but another one never comes?

[Leslie Lamport]

Deadlock means reaching a state in which Next is not enabled.  A little simple logic shows that, for all t in Thread, in any state in which wasVictim[t] and owner[t] are Booleans, at least one of BecomeVictim(t), AcquireLock(t), and ReleaseLock(t) is enabled.

[Markus Kuppe]

On 15.11.19 17:10, Leslie Lamport wrote:
> Deadlock means reaching a state in which Next is not enabled.  A little
> simple logic shows that, for all t in Thread, in any state in which
> wasVictim[t] and owner[t] are Booleans, at least one of BecomeVictim(t),
> AcquireLock(t), and ReleaseLock(t) is enabled.
>

For such a small model, the Toolbox can also visualize the state graph
that shows no deadlock states.

M.

[Dmitry Neverov]

I'm new to TLA and it looks like deadlock was a wrong term to use. What I wanted to see is a report of EventualSuccess violation. My reasoning was that it is violated when only stuttering steps occur. I thought that maybe TLA needs non-stuttering steps. To check I've added a 'time' variable and an action which increments it.  It didn't work: model checking doesn't finish. I'm clearly doing something wrong.

I was able to reproduce the situation when one of the treads never tries to lock by by introducing an additional variable 'dead' (a function from Thread to BOOLEAN), an additional step for thread to die, and an enabling condition that a dead thread cannot become a victim. Is it the right way to model the situation when one of the threads never tries to lock? Is the EventualSuccess formula a wrong thing to check in this spec? Are there any examples of the spec where a similar property is violated?

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/rp5cE4IzEnM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d64cf80a-43d0-e114-1f53-29aa49762034%40lemmster.de.

[Stephan Merz]

According to the TLA+ module in the original post, you define

Spec == Init /\ [][Next]_<<victim, owner, wasVictim>> /\ EventualSuccess
 

Since it is part of the specification, the property EventualSuccess can never be violated.

–––

By adding a counter variable that can be incremented without bound, you get an infinite state space, so model checking will not finish. You could add a state constraint to instruct TLC to ignore states where the value of the counter exceeds some bound, but it is not clear to me what exactly you are trying to achieve with this extra variable.

–––

Adding variable `dead' may be useful. However, nothing in the original specification requires a thread to initiate the process of acquiring a lock (through action BecomeVictim). So, again it is not clear to me why this would be the right way to proceed.

–––

I suspect that you want to change your specification so that instead of the conjunct EventualSuccess, it only includes lower-level liveness conditions (typically, fairness hypotheses on actions), and then check property EventualSuccess for that modified specification. A starting point could be to conjoin the formula Fairness defined as

Fairness ==

  /\ \A t \in Thread : WF_vars(AcquireLock(t))

  /\ \A t \in Thread : WF_vars(ReleaseLock(t))

where vars is the tuple formed of the three variables declared in the module.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC%2BL6n09md_5UN6rxKTsj6zG%3Dc2DSAdbQvwoTp-fZ-AguupZ%3Dg%40mail.gmail.com.