<!-- canonical: https://efficientnewlanguage.org/eml-p/projects/P116-deadlock-detector/ | updated: 2026-10-16 -->

# P116 Deadlock detector

Threads taking and releasing locks by a schedule, turn by turn, with the wait-for cycle that is a deadlock; every interleaving counted, the serial ones that never deadlock, and one lock order that removes it.

EML-P project `projects/deadlock-detector` in the EML language repo: 2 module(s), entry `main.eml`, terminal UI. There, `eml project run projects/deadlock-detector` runs it and `eml project verify projects/deadlock-detector` replays every session under CPython (two hash seeds) and in the interpreter; the site build replays every session in the interpreter again and publishes a session only if its screen matches.

Built on verified corpus cases: deadlock-by-lock-order (https://efficientnewlanguage.org/cases/251-deadlock-by-lock-order/).

## Sessions

### bad-input - interpreter: byte-equal to the golden

Input:

```text
0
x
2

2
1 3
2
1 a
2
1 12
2
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
4

4
circle
2
2 2 2 2 2
5
```

Screen:

```text
== Deadlock detector ==
Threads taking and releasing locks by a schedule; a thread waits while its next lock is held, and a cycle of waiting is a deadlock.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 0
Pick a number from 1 to 5.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> x
Pick a number from 1 to 5.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 
Cancelled.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 3
Type thread numbers from 1 to 2, separated by spaces.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 a
Type thread numbers from 1 to 2, separated by spaces.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 12
Type thread numbers from 1 to 2, separated by spaces.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
Up to 30 turns.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 4
threads (opposite, ordered, ring or ring-ordered)> 
Cancelled.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 4
threads (opposite, ordered, ring or ring-ordered)> circle
Type opposite, ordered, ring or ring-ordered.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 2 2 2 2 2
  T2 takes B
  T2 takes A
  T2 releases A
  T2 releases B
  T2 has finished
No deadlock; 1 thread still to finish, and running the rest, lowest thread first, finishes every thread.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 5
Bye.
```

### basic - interpreter: byte-equal to the golden

Input:

```text
1
2
1 1 1 1 2 2 2 2
2
1 2 1 2
2
1 2
3
4
ordered
2
1 2 1 2 1 2 1 2
3
4
ring
2
1 2 3 1 2 3
3
4
ring-ordered
2
1 2 3 1 2 3 1 2 3 1 2 3
3
5
```

Screen:

```text
== Deadlock detector ==
Threads taking and releasing locks by a schedule; a thread waits while its next lock is held, and a cycle of waiting is a deadlock.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 1
Threads (opposite):
  T1: lock A, lock B, unlock B, unlock A
  T2: lock B, lock A, unlock A, unlock B

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 1 1 1 2 2 2 2
  T1 takes A
  T1 takes B
  T1 releases B
  T1 releases A
  T2 takes B
  T2 takes A
  T2 releases A
  T2 releases B
Every thread finished and every lock is free.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 2 1 2
  T1 takes A
  T2 takes B
  T1 waits for B, held by T2
  T2 waits for A, held by T1
Deadlock: T1 waits for B held by T2; T2 waits for A held by T1. No turn of theirs can ever move.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 2
  T1 takes A
  T2 takes B
No deadlock yet; 2 threads still to finish, and running the rest, lowest thread first, ends in deadlock.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 3
Every interleaving of the opposite threads, each blocked thread trying again on its next turn and the rest run out at the end:
  70 interleavings, 40 end in deadlock, 30 with every lock free.
  Serial ones, one thread finishing before the other starts: 2, of which 0 deadlock.
A test that does not force the threads to overlap sees only the serial schedules, and they never deadlock.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 4
threads (opposite, ordered, ring or ring-ordered)> ordered
Threads (ordered):
  T1: lock A, lock B, unlock B, unlock A
  T2: lock A, lock B, unlock B, unlock A

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 2, up to 30 turns).
schedule> 1 2 1 2 1 2 1 2
  T1 takes A
  T2 waits for A, held by T1
  T1 takes B
  T2 waits for A, held by T1
  T1 releases B
  T2 waits for A, held by T1
  T1 releases A
  T2 takes A
No deadlock; 1 thread still to finish, and running the rest, lowest thread first, finishes every thread.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 3
Every interleaving of the ordered threads, each blocked thread trying again on its next turn and the rest run out at the end:
  70 interleavings, 0 end in deadlock, 70 with every lock free.
  Serial ones, one thread finishing before the other starts: 2, of which 0 deadlock.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 4
threads (opposite, ordered, ring or ring-ordered)> ring
Threads (ring):
  T1: lock A, lock B, unlock B, unlock A
  T2: lock B, lock C, unlock C, unlock B
  T3: lock C, lock A, unlock A, unlock C

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 3, up to 30 turns).
schedule> 1 2 3 1 2 3
  T1 takes A
  T2 takes B
  T3 takes C
  T1 waits for B, held by T2
  T2 waits for C, held by T3
  T3 waits for A, held by T1
Deadlock: T1 waits for B held by T2; T2 waits for C held by T3; T3 waits for A held by T1. No turn of theirs can ever move.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 3
Three threads of four steps have 34,650 interleavings, too many to run here. Every one was run in the cross-check:
  14,400 of them end in deadlock; the 6 serial ones do not.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 4
threads (opposite, ordered, ring or ring-ordered)> ring-ordered
Threads (ring-ordered):
  T1: lock A, lock B, unlock B, unlock A
  T2: lock B, lock C, unlock C, unlock B
  T3: lock A, lock C, unlock C, unlock A

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 2
A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to 3, up to 30 turns).
schedule> 1 2 3 1 2 3 1 2 3 1 2 3
  T1 takes A
  T2 takes B
  T3 waits for A, held by T1
  T1 waits for B, held by T2
  T2 takes C
  T3 waits for A, held by T1
  T1 waits for B, held by T2
  T2 releases C
  T3 waits for A, held by T1
  T1 waits for B, held by T2
  T2 releases B
  T3 waits for A, held by T1
No deadlock; 2 threads still to finish, and running the rest, lowest thread first, finishes every thread.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 3
Three threads of four steps have 34,650 interleavings, too many to run here. Every one was run in the cross-check:
  none of them ends in deadlock: every thread takes its locks in the order A, B, C.

1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit
choice> 5
Bye.
```

## Modules

### main.eml

```eml
# P116 deadlock detector: threads taking locks, one schedule step by step
# with its wait-for graph, every interleaving counted, and one global lock
# order that removes the deadlock.
import locks

def plain(s):
    0 => i
    len(s) => j
    while i < j and s[i] == " ":
        i + 1 => i
    while j > i and s[j - 1] == " ":
        j - 1 => j
    return s[i:j]

def program_text(p):
    "" => out
    for s in p:
        if out != "":
            out + ", " => out
        out + s[0] + " " + s[1] => out
    return out

def show(name, progs):
    ("Threads (" + name + "):") ^0
    for t in [0:len(progs) - 1]:
        ("  T" + str(t + 1) + ": " + program_text(progs[t])) ^0

def run_one(progs):
    ("A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to " + str(len(progs)) + ", up to 30 turns).") ^0
    plain(input("schedule> ")) => t
    if t == "":
        "Cancelled." ^0
        return
    [] => sched
    "" => w
    for c in t + " ":
        if c == " ":
            if w != "":
                if len(w) != 1 or w[0] < "1" or w[0] > str(len(progs)):
                    ("Type thread numbers from 1 to " + str(len(progs)) + ", separated by spaces.") ^0
                    return
                sched + [int(w) - 1] => sched
            "" => w
        else:
            w + c => w
    if len(sched) == 0 or len(sched) > 30:
        "Up to 30 turns." ^0
        return
    locks.run(progs, sched, False) => r
    for e in r[0]:
        "T" + str(e[0] + 1) => who
        if e[2] == "done":
            ("  " + who + " has finished") ^0
        else:
            progs[e[0]][e[1]] => s
            if e[2] == "take":
                ("  " + who + " takes " + s[1]) ^0
            elif e[2] == "release":
                ("  " + who + " releases " + s[1]) ^0
            else:
                ("  " + who + " waits for " + s[1] + ", held by T" + str(e[3] + 1)) ^0
    r[1] => st
    locks.cycle(progs, st) => c
    if len(c) > 0:
        "" => line
        for i in [0:len(c) - 1]:
            c[i] => x
            c[(i + 1) % len(c)] => y
            if line != "":
                line + "; " => line
            line + "T" + str(x + 1) + " waits for " + st[2][x] + " held by T" + str(y + 1) => line
        ("Deadlock: " + line + ". No turn of theirs can ever move.") ^0
        return
    0 => left
    for i in [0:len(progs) - 1]:
        if st[0][i] < len(progs[i]):
            left + 1 => left
    if left == 0:
        "Every thread finished and every lock is free." ^0
        return
    locks.run(progs, sched, True) => after
    if after[2]:
        ("No deadlock yet; " + str(left) + " thread" + plural(left) + " still to finish, and running the rest, lowest thread first, ends in deadlock.") ^0
    else:
        ("No deadlock; " + str(left) + " thread" + plural(left) + " still to finish, and running the rest, lowest thread first, finishes every thread.") ^0

def plural(n):
    if n == 1:
        return ""
    return "s"

def census(name, progs):
    if len(progs) > 2:
        "Three threads of four steps have 34,650 interleavings, too many to run here. Every one was run in the cross-check:" ^0
        if name == "ring":
            "  14,400 of them end in deadlock; the 6 serial ones do not." ^0
        else:
            "  none of them ends in deadlock: every thread takes its locks in the order A, B, C." ^0
        return
    locks.census(progs) => c
    ("Every interleaving of the " + name + " threads, each blocked thread trying again on its next turn and the rest run out at the end:") ^0
    ("  " + str(c[0]) + " interleavings, " + str(c[1]) + " end in deadlock, " + str(c[0] - c[1]) + " with every lock free.") ^0
    ("  Serial ones, one thread finishing before the other starts: " + str(c[2]) + ", of which " + str(c[3]) + " deadlock.") ^0
    if c[1] > 0:
        "A test that does not force the threads to overlap sees only the serial schedules, and they never deadlock." ^0

"opposite" => name
locks.presets(name) => progs

"== Deadlock detector ==" ^0
"Threads taking and releasing locks by a schedule; a thread waits while its next lock is held, and a cycle of waiting is a deadlock." ^0
True => running
while running:
    "" ^0
    "1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit" ^0
    plain(input("choice> ")) => choice
    if choice == "1":
        show(name, progs)
    elif choice == "2":
        run_one(progs)
    elif choice == "3":
        census(name, progs)
    elif choice == "4":
        plain(input("threads (opposite, ordered, ring or ring-ordered)> ")) => n
        if n == "":
            "Cancelled." ^0
        elif len(locks.presets(n)) == 0:
            "Type opposite, ordered, ring or ring-ordered." ^0
        else:
            n => name
            locks.presets(n) => progs
            show(name, progs)
    elif choice == "5":
        False => running
    else:
        "Pick a number from 1 to 5." ^0
"Bye." ^0
```

Python projection of main.eml:

```python
import locks

def plain(s):
    i = 0
    j = len(s)
    while i < j and s[i] == " ":
        i = i + 1
    while j > i and s[j - 1] == " ":
        j = j - 1
    return s[i:j]

def program_text(p):
    out = ""
    for s in p:
        if out != "":
            out = out + ", "
        out = out + s[0] + " " + s[1]
    return out

def show(name, progs):
    print("Threads (" + name + "):")
    for t in range(0, len(progs)):
        print("  T" + str(t + 1) + ": " + program_text(progs[t]))

def run_one(progs):
    print("A schedule: whose turn it is, such as 1 2 1 2 (threads 1 to " + str(len(progs)) + ", up to 30 turns).")
    t = plain(input("schedule> "))
    if t == "":
        print("Cancelled.")
        return
    sched = []
    w = ""
    for c in t + " ":
        if c == " ":
            if w != "":
                if len(w) != 1 or w[0] < "1" or w[0] > str(len(progs)):
                    print("Type thread numbers from 1 to " + str(len(progs)) + ", separated by spaces.")
                    return
                sched = sched + [int(w) - 1]
            w = ""
        else:
            w = w + c
    if len(sched) == 0 or len(sched) > 30:
        print("Up to 30 turns.")
        return
    r = locks.run(progs, sched, False)
    for e in r[0]:
        who = "T" + str(e[0] + 1)
        if e[2] == "done":
            print("  " + who + " has finished")
        else:
            s = progs[e[0]][e[1]]
            if e[2] == "take":
                print("  " + who + " takes " + s[1])
            elif e[2] == "release":
                print("  " + who + " releases " + s[1])
            else:
                print("  " + who + " waits for " + s[1] + ", held by T" + str(e[3] + 1))
    st = r[1]
    c = locks.cycle(progs, st)
    if len(c) > 0:
        line = ""
        for i in range(0, len(c)):
            x = c[i]
            y = c[(i + 1) % len(c)]
            if line != "":
                line = line + "; "
            line = line + "T" + str(x + 1) + " waits for " + st[2][x] + " held by T" + str(y + 1)
        print("Deadlock: " + line + ". No turn of theirs can ever move.")
        return
    left = 0
    for i in range(0, len(progs)):
        if st[0][i] < len(progs[i]):
            left = left + 1
    if left == 0:
        print("Every thread finished and every lock is free.")
        return
    after = locks.run(progs, sched, True)
    if after[2]:
        print("No deadlock yet; " + str(left) + " thread" + plural(left) + " still to finish, and running the rest, lowest thread first, ends in deadlock.")
    else:
        print("No deadlock; " + str(left) + " thread" + plural(left) + " still to finish, and running the rest, lowest thread first, finishes every thread.")

def plural(n):
    if n == 1:
        return ""
    return "s"

def census(name, progs):
    if len(progs) > 2:
        print("Three threads of four steps have 34,650 interleavings, too many to run here. Every one was run in the cross-check:")
        if name == "ring":
            print("  14,400 of them end in deadlock; the 6 serial ones do not.")
        else:
            print("  none of them ends in deadlock: every thread takes its locks in the order A, B, C.")
        return
    c = locks.census(progs)
    print("Every interleaving of the " + name + " threads, each blocked thread trying again on its next turn and the rest run out at the end:")
    print("  " + str(c[0]) + " interleavings, " + str(c[1]) + " end in deadlock, " + str(c[0] - c[1]) + " with every lock free.")
    print("  Serial ones, one thread finishing before the other starts: " + str(c[2]) + ", of which " + str(c[3]) + " deadlock.")
    if c[1] > 0:
        print("A test that does not force the threads to overlap sees only the serial schedules, and they never deadlock.")

name = "opposite"
progs = locks.presets(name)
print("== Deadlock detector ==")
print("Threads taking and releasing locks by a schedule; a thread waits while its next lock is held, and a cycle of waiting is a deadlock.")
running = True
while running:
    print("")
    print("1) threads  2) run a schedule  3) every interleaving  4) other threads  5) quit")
    choice = plain(input("choice> "))
    if choice == "1":
        show(name, progs)
    elif choice == "2":
        run_one(progs)
    elif choice == "3":
        census(name, progs)
    elif choice == "4":
        n = plain(input("threads (opposite, ordered, ring or ring-ordered)> "))
        if n == "":
            print("Cancelled.")
        elif len(locks.presets(n)) == 0:
            print("Type opposite, ordered, ring or ring-ordered.")
        else:
            name = n
            progs = locks.presets(n)
            show(name, progs)
    elif choice == "5":
        running = False
    else:
        print("Pick a number from 1 to 5.")
print("Bye.")
```

### locks.eml

```eml
# P116 deadlock detector - threads that take and release locks, run by a
# schedule that says whose turn it is. A thread whose next lock is held
# waits, and tries again on its next turn. A deadlock is a cycle in the
# wait-for graph: each thread waiting for a lock held by the next. As in
# the corpus case deadlock-by-lock-order, two threads that take the same
# two locks in opposite orders deadlock on most interleavings, and taking
# every lock in one global order removes it.
#
# A program is a list of steps [action, lock]: action "lock" or "unlock".

def presets(name):
    if name == "opposite":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "A"], ["unlock", "A"], ["unlock", "B"]]]
    if name == "ordered":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]]]
    if name == "ring":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "C"], ["unlock", "C"], ["unlock", "B"]], [["lock", "C"], ["lock", "A"], ["unlock", "A"], ["unlock", "C"]]]
    if name == "ring-ordered":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "C"], ["unlock", "C"], ["unlock", "B"]], [["lock", "A"], ["lock", "C"], ["unlock", "C"], ["unlock", "A"]]]
    return []

def new_state(progs):
    # [pc per thread, holder per lock, lock waited for per thread ("" if none)]
    [] => pc
    [] => waiting
    for p in progs:
        pc + [0] => pc
        waiting + [""] => waiting
    return [pc, {}, waiting]

def step(progs, st, t):
    # thread t takes its turn: [what happened, thread that holds it or -1]
    st[0] => pc
    st[1] => holder
    if pc[t] >= len(progs[t]):
        return ["done", 0 - 1]
    progs[t][pc[t]] => s
    if s[0] == "lock":
        if s[1] in holder and holder[s[1]] != t:
            s[1] => st[2][t]
            return ["wait", holder[s[1]]]
        t => holder[s[1]]
        "" => st[2][t]
        pc[t] + 1 => pc[t]
        return ["take", 0 - 1]
    {} => rest
    for k in holder:
        if k != s[1]:
            holder[k] => rest[k]
    rest => st[1]
    pc[t] + 1 => pc[t]
    return ["release", 0 - 1]

def can_go(progs, st, t):
    if st[0][t] >= len(progs[t]):
        return False
    progs[t][st[0][t]] => s
    if s[0] == "unlock":
        return True
    return not (s[1] in st[1]) or st[1][s[1]] == t

def cycle(progs, st):
    # a cycle in the wait-for graph, as a list of threads, or []
    [] => edges
    for t in [0:len(progs) - 1]:
        0 - 1 => to
        if st[2][t] != "" and st[0][t] < len(progs[t]) and st[2][t] in st[1]:
            st[1][st[2][t]] => to
        edges + [to] => edges
    for s in [0:len(progs) - 1]:
        [s] => path
        edges[s] => x
        while x != 0 - 1 and len(path) <= len(progs):
            if x == s:
                return path
            path + [x] => path
            edges[x] => x
    return []

def run(progs, schedule, drain):
    # [log, state, deadlocked]: each turn of the schedule, then - with
    # drain - every thread that can still go, lowest number first, until
    # none can
    new_state(progs) => st
    [] => log
    for t in schedule:
        st[0][t] => at
        step(progs, st, t) => r
        log + [[t, at, r[0], r[1]]] => log
    if drain:
        True => moving
        while moving:
            False => moving
            for t in [0:len(progs) - 1]:
                if not moving and can_go(progs, st, t):
                    step(progs, st, t)
                    True => moving
    False => stuck
    for t in [0:len(progs) - 1]:
        if st[0][t] < len(progs[t]):
            True => stuck
    return [log, st, stuck]

def interleavings(lengths):
    # every order of the threads' turns, thread t appearing lengths[t] times
    [[[], lengths]] => frontier
    [] => out
    while len(frontier) > 0:
        frontier[len(frontier) - 1] => item
        frontier[0:len(frontier) - 1] => frontier
        item[0] => seq
        item[1] => left
        0 => total
        for n in left:
            total + n => total
        if total == 0:
            out + [seq] => out
        else:
            for t in [0:len(left) - 1]:
                if left[t] > 0:
                    [] => nl
                    for i in [0:len(left) - 1]:
                        if i == t:
                            nl + [left[i] - 1] => nl
                        else:
                            nl + [left[i]] => nl
                    frontier + [[seq + [t], nl]] => frontier
    return out

def census(progs):
    # over every interleaving: [interleavings, deadlocked, serial ones,
    # serial ones deadlocked]
    [] => lengths
    for p in progs:
        lengths + [len(p)] => lengths
    0 => n
    0 => dead
    0 => serial
    0 => serial_dead
    for seq in interleavings(lengths):
        n + 1 => n
        run(progs, seq, True)[2] => stuck
        if stuck:
            dead + 1 => dead
        0 => changes
        for i in [1:len(seq) - 1]:
            if seq[i] != seq[i - 1]:
                changes + 1 => changes
        if changes == len(progs) - 1:
            serial + 1 => serial
            if stuck:
                serial_dead + 1 => serial_dead
    return [n, dead, serial, serial_dead]
```

Python projection of locks.eml:

```python
def presets(name):
    if name == "opposite":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "A"], ["unlock", "A"], ["unlock", "B"]]]
    if name == "ordered":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]]]
    if name == "ring":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "C"], ["unlock", "C"], ["unlock", "B"]], [["lock", "C"], ["lock", "A"], ["unlock", "A"], ["unlock", "C"]]]
    if name == "ring-ordered":
        return [[["lock", "A"], ["lock", "B"], ["unlock", "B"], ["unlock", "A"]], [["lock", "B"], ["lock", "C"], ["unlock", "C"], ["unlock", "B"]], [["lock", "A"], ["lock", "C"], ["unlock", "C"], ["unlock", "A"]]]
    return []

def new_state(progs):
    pc = []
    waiting = []
    for p in progs:
        pc = pc + [0]
        waiting = waiting + [""]
    return [pc, {}, waiting]

def step(progs, st, t):
    pc = st[0]
    holder = st[1]
    if pc[t] >= len(progs[t]):
        return ["done", 0 - 1]
    s = progs[t][pc[t]]
    if s[0] == "lock":
        if s[1] in holder and holder[s[1]] != t:
            st[2][t] = s[1]
            return ["wait", holder[s[1]]]
        holder[s[1]] = t
        st[2][t] = ""
        pc[t] = pc[t] + 1
        return ["take", 0 - 1]
    rest = {}
    for k in holder:
        if k != s[1]:
            rest[k] = holder[k]
    st[1] = rest
    pc[t] = pc[t] + 1
    return ["release", 0 - 1]

def can_go(progs, st, t):
    if st[0][t] >= len(progs[t]):
        return False
    s = progs[t][st[0][t]]
    if s[0] == "unlock":
        return True
    return not s[1] in st[1] or st[1][s[1]] == t

def cycle(progs, st):
    edges = []
    for t in range(0, len(progs)):
        to = 0 - 1
        if st[2][t] != "" and st[0][t] < len(progs[t]) and st[2][t] in st[1]:
            to = st[1][st[2][t]]
        edges = edges + [to]
    for s in range(0, len(progs)):
        path = [s]
        x = edges[s]
        while x != 0 - 1 and len(path) <= len(progs):
            if x == s:
                return path
            path = path + [x]
            x = edges[x]
    return []

def run(progs, schedule, drain):
    st = new_state(progs)
    log = []
    for t in schedule:
        at = st[0][t]
        r = step(progs, st, t)
        log = log + [[t, at, r[0], r[1]]]
    if drain:
        moving = True
        while moving:
            moving = False
            for t in range(0, len(progs)):
                if not moving and can_go(progs, st, t):
                    step(progs, st, t)
                    moving = True
    stuck = False
    for t in range(0, len(progs)):
        if st[0][t] < len(progs[t]):
            stuck = True
    return [log, st, stuck]

def interleavings(lengths):
    frontier = [[[], lengths]]
    out = []
    while len(frontier) > 0:
        item = frontier[len(frontier) - 1]
        frontier = frontier[0:len(frontier) - 1]
        seq = item[0]
        left = item[1]
        total = 0
        for n in left:
            total = total + n
        if total == 0:
            out = out + [seq]
        else:
            for t in range(0, len(left)):
                if left[t] > 0:
                    nl = []
                    for i in range(0, len(left)):
                        if i == t:
                            nl = nl + [left[i] - 1]
                        else:
                            nl = nl + [left[i]]
                    frontier = frontier + [[seq + [t], nl]]
    return out

def census(progs):
    lengths = []
    for p in progs:
        lengths = lengths + [len(p)]
    n = 0
    dead = 0
    serial = 0
    serial_dead = 0
    for seq in interleavings(lengths):
        n = n + 1
        stuck = run(progs, seq, True)[2]
        if stuck:
            dead = dead + 1
        changes = 0
        for i in range(1, len(seq)):
            if seq[i] != seq[i - 1]:
                changes = changes + 1
        if changes == len(progs) - 1:
            serial = serial + 1
            if stuck:
                serial_dead = serial_dead + 1
    return [n, dead, serial, serial_dead]
```

## README

# P116 - Deadlock detector

Threads take and release locks in the order a schedule gives them turns.
A thread whose next lock is held waits; when every thread in a cycle waits
for a lock the next one holds, none of them can ever move.

- `main.eml` - the menu, the threads, one schedule turn by turn, and every
  interleaving counted
- `locks.eml` - the four sets of threads, a turn, the wait-for cycle, a run
  of a schedule, and the count over every interleaving

How each part works:

- A thread is a list of steps: lock A, lock B, unlock B, unlock A. On its
  turn it takes its next step. A lock held by another thread makes it
  wait, and it tries the same step again on its next turn.
- The wait-for graph has an arrow from each waiting thread to the thread
  that holds its lock. A cycle in it is a deadlock: each thread in it
  waits for the next, so no turn of theirs can move. Two threads can
  already be stuck before either waits: after 1 2, T1 holds A and T2 holds
  B, and the program runs the rest to show it ends in deadlock.
- As in the corpus case `deadlock-by-lock-order`, every interleaving of
  the two opposite threads is run, the rest run out at the end:
  - 40 of the 70 deadlock, exactly those that start 1 2 or 2 1;
  - the 2 serial ones, one thread finishing before the other starts, never
    do, and they are all that a test without forced overlap sees.
- Taking locks in one order, A before B before C, removes the deadlock on
  every interleaving. Three threads in a ring deadlock on 14,400 of 34,650
  interleavings; with T3 taking A before C, on none. Those two counts were
  run in the cross-check; the program states them.

What is checked: menu choices 1 to 5; a schedule of thread numbers from 1
to the number of threads, separated by spaces, up to 30 turns; one of the
four sets of threads. An empty answer cancels.

Sessions: `sessions/basic.in` gives:
- the opposite threads one after the other, then 1 2 1 2 (a deadlock),
  then 1 2 (no one waits yet, and the rest deadlock), and the count;
- the ordered threads with 1 2 1 2 1 2 1 2 (T2 waits, and both finish)
  and the count;
- the ring with 1 2 3 1 2 3 (a deadlock of three) and its count;
- the ordered ring with turns 1 2 3 four times, and its count.

`sessions/bad-input.in` gives:
- menu choices 0 and x;
- schedules: a cancel, 1 3, 1 a, 1 12 and 31 turns;
- other threads: a cancel and circle;
- the schedule 2 2 2 2 2, a turn for T2 after it has finished.

Built on the verified corpus case `deadlock-by-lock-order` (two threads
taking two locks in opposite orders, and one global order that removes the
deadlock).