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

[tlaplus] Re: Reproducing deadlock in TLA+

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.

On Friday, November 15, 2019 at 1:45:30 PM UTC-8, dmitry.neverov@g... wrote:
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 ------------------------------
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?

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/7c6f17db-7ae5-4669-b859-a82be39cefc8%40googlegroups.com.