Project 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.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-16
Every screen below was recorded under CPython. When this page was built, the EML interpreter replayed each session from the same input and printed the same bytes.
About
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 countedlocks.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).
Recorded sessions
What the screen shows while someone uses the program. Each typed line appears after its prompt, the way a terminal shows it.
bad-input
interpreter: byte-equal== 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.
What was typed (19 lines)
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
basic
interpreter: byte-equal== 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.
What was typed (24 lines)
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
Modules
The program as written, entry module first. Each module transpiles to its own Python file, which is what eml project run executes.
main.eml(entry)
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 (main.py)
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 (locks.py)
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]