在 TLA+ 中重现死锁

Question

我正在尝试在 TLA+ 中重现 Herlihy 的 "The Art of Multiprocessor Programming" 中的死锁。在下面的代码中，当一个线程想要获取锁时，它会将自己标记为受害者，并且只有在另一个线程成为受害者时才会继续。如果另一个线程永远不会出现，这里就会出现死锁。

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() {}
}

TLA+规范如下：

------------------------------ 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 规范在 Thread = {t1, t2} 中运行良好，其中 t1 和 t2 是模型值。

如何让TLA报告死锁？

Answer 1

请参阅 Leslie Lamport 在半官方 Google 群组上的回答：https://groups.google.com/forum/#!topic/tlaplus/rp5cE4IzEnM

（镜像：http://discuss.tlapl.us/msg03229.html）

在 TLA+ 中重现死锁

Reproducing deadlock in TLA+

tla+