Project P128
Connection pool
Jobs leaving their bodies at the end, by break, by return or by raise, giving their connections back by hand or by a with block; and when users borrowing one connection after another can leave the whole pool held.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-17
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
A fixed number of connections, borrowed by jobs and given back - or not. Jobs leave their bodies in four ways, and users borrowing one connection after another can leave the whole pool held and nobody able to finish.
main.eml- the menu, jobs under both ways of giving back, the deadlock table, and one casepool.eml- the pool and its with-block lease, the jobs, and the search over every order of borrowing
How each part works:
- As in the corpus case
connection-pool-release, a body can leave at its end, by break, by return or by raise. Given back by hand at the end of the body, the connection is kept on the other three ways out, and the pool runs dry: later jobs find none free and would wait forever. Given back by a with block, it comes back on all four. - As in the corpus case
pool-reentrancy-deadlock, a user that needs several connections borrows them one at a time and holds each until it has them all. Some order of borrowing leaves every connection held by users that each need one more exactly when users × (need - 1) is at least the pool: 4 users needing 2 each deadlock a pool of 4, 3 do not. Needing one at a time never deadlocks. One user needing more than the pool holds can never finish. - Every reachable state of who holds how many is searched, users with the same count taken as one.
What is checked: menu choices 1 to 4; a pool from 1 to 6 for jobs and 1 to 8 for a case; up to 12 jobs, each end, break, return or raise; a need from 1 to 4 and 1 to 8 users. An empty answer cancels.
Sessions: sessions/basic.in gives: - end, break, return, raise, end and end on a pool of 3: by hand the pool is empty after the fourth job; - the deadlock table; - a pool of 4 with 4 users needing 2 (a deadlock) and 3 users (none).
sessions/bad-input.in gives: - menu choices 0 and x; - jobs: a cancel, a pool of 7, then a pool of 3 with a cancel, loop and 13 jobs, and three ends on a pool of 2; - cases: a cancel, a pool of 9, a need of 5, 9 users, and 8 users needing 1 from a pool of 1.
Built on the verified corpus cases connection-pool-release (a with block releases on every way out) and pool-reentrancy-deadlock (holding one connection while borrowing the next).
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== Connection pool ==
A fixed number of connections, borrowed by jobs and given back - or not.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 0
Pick a number from 1 to 4.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> x
Pick a number from 1 to 4.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)>
Cancelled.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 7
Type a whole number from 1 to 6.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 3
Each job leaves its body at the end, by break, by return or by raise.
jobs (such as end break return raise end, up to 12)>
Cancelled.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 3
Each job leaves its body at the end, by break, by return or by raise.
jobs (such as end break return raise end, up to 12)> end loop
Each job is end, break, return or raise.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 3
Each job leaves its body at the end, by break, by return or by raise.
jobs (such as end break return raise end, up to 12)> end end end end end end end end end end end end end
Up to 12 jobs.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 2
Each job leaves its body at the end, by break, by return or by raise.
jobs (such as end break return raise end, up to 12)> end end end
Pool of 2; connections out after each job:
job leaves given back by hand with a with block
1 end 0 out 0 out
2 end 0 out 0 out
3 end 0 out 0 out
By hand: every connection given back.
With a with block: every connection given back, however the body left.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)>
Cancelled.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 9
Type a whole number from 1 to 8.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 4
connections each user needs (1 to 4)> 5
Type a whole number from 1 to 4.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 4
connections each user needs (1 to 4)> 2
users (1 to 8)> 9
Type a whole number from 1 to 8.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 1
connections each user needs (1 to 4)> 1
users (1 to 8)> 8
No order of borrowing deadlocks: 8 users needing 1 each, pool of 1.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 4
Bye.
What was typed (34 lines)
0
x
1
1
7
1
3
1
3
end loop
1
3
end end end end end end end end end end end end end
1
2
end end end
3
3
9
3
4
5
3
4
2
9
3
1
1
8
4
basic
interpreter: byte-equal== Connection pool ==
A fixed number of connections, borrowed by jobs and given back - or not.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 1
pool size (1 to 6)> 3
Each job leaves its body at the end, by break, by return or by raise.
jobs (such as end break return raise end, up to 12)> end break return raise end end
Pool of 3; connections out after each job:
job leaves given back by hand with a with block
1 end 0 out 0 out
2 break 1 out 0 out
3 return 2 out 0 out
4 raise 3 out 0 out
5 end none free: waits forever 0 out
6 end none free: waits forever 0 out
By hand: 3 of 3 never given back, by the jobs that left early.
2 later jobs found no connection free.
With a with block: every connection given back, however the body left.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 2
Users borrowing one connection after another, holding each until they have all they need:
the fewest users for which some order of borrowing deadlocks (- for none up to 12).
needs pool 2 pool 3 pool 4 pool 5 pool 6
1 - - - - -
2 2 3 4 5 6
3 1 2 2 3 3
4 1 1 2 2 2
Every count is the smallest number of users that, holding need - 1 each, can hold the whole pool; one connection at a time never deadlocks.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 4
connections each user needs (1 to 4)> 2
users (1 to 8)> 4
Deadlock: every connection held, the waiting users holding 1, 1, 1, 1 of the 2 each needs, and none can borrow another.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 3
pool size (1 to 8)> 4
connections each user needs (1 to 4)> 2
users (1 to 8)> 3
No order of borrowing deadlocks: 3 users needing 2 each, pool of 4.
1) jobs 2) deadlock table 3) one deadlock 4) quit
choice> 4
Bye.
What was typed (13 lines)
1
3
end break return raise end end
2
3
4
2
4
3
4
2
3
4
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# P128 connection pool: jobs leaving in four ways under give-back by hand
# and by a with block, and when borrowing a second connection deadlocks.
import pool
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 pad(s, n):
s => out
while len(out) < n:
out + " " => out
return out
def lpad(s, n):
s => out
while len(out) < n:
" " + out => out
return out
def ask_int(prompt, low, high):
plain(input(prompt)) => t
if t == "":
"Cancelled." ^0
return 0 - 1
if len(t) > 2:
("Type a whole number from " + str(low) + " to " + str(high) + ".") ^0
return 0 - 1
for c in t:
if c < "0" or c > "9":
("Type a whole number from " + str(low) + " to " + str(high) + ".") ^0
return 0 - 1
if int(t) < low or int(t) > high:
("Type a whole number from " + str(low) + " to " + str(high) + ".") ^0
return 0 - 1
return int(t)
def jobs():
ask_int("pool size (1 to 6)> ", 1, 6) => size
if size < 0:
return
"Each job leaves its body at the end, by break, by return or by raise." ^0
plain(input("jobs (such as end break return raise end, up to 12)> ")) => t
if t == "":
"Cancelled." ^0
return
[] => js
"" => w
for c in t + " ":
if c == " ":
if w != "":
if w != "end" and w != "break" and w != "return" and w != "raise":
"Each job is end, break, return or raise." ^0
return
js + [w] => js
"" => w
else:
w + c => w
if len(js) > 12:
"Up to 12 jobs." ^0
return
pool.run_jobs(size, js, "by hand") => a
pool.run_jobs(size, js, "with") => b
("Pool of " + str(size) + "; connections out after each job:") ^0
" job leaves given back by hand with a with block" ^0
for k in [0:len(js) - 1]:
(" " + lpad(str(k + 1), 3) + " " + pad(js[k], 7) + " " + pad(cell(a[k]), 30) + " " + cell(b[k])) ^0
0 => stuck
for r in a:
if not r[2]:
stuck + 1 => stuck
a[len(a) - 1][1] => left
if left == 0:
"By hand: every connection given back." ^0
else:
("By hand: " + str(left) + " of " + str(size) + " never given back, by the jobs that left early.") ^0
if stuck > 0:
(" " + str(stuck) + " later jobs found no connection free.") ^0
"With a with block: every connection given back, however the body left." ^0
def cell(r):
if not r[2]:
return "none free: waits forever"
return str(r[1]) + " out"
def table():
"Users borrowing one connection after another, holding each until they have all they need:" ^0
"the fewest users for which some order of borrowing deadlocks (- for none up to 12)." ^0
" needs pool 2 pool 3 pool 4 pool 5 pool 6" ^0
True => formula
for need in [1:4]:
" " + pad(str(need), 6) => line
for size in [2:6]:
pool.first_deadlock(size, need, 12) => c
if c == 0:
line + lpad("-", 8) => line
if need > 1:
False => formula
else:
line + lpad(str(c), 8) => line
if need == 1 or c * (need - 1) < size or (c - 1) * (need - 1) >= size:
False => formula
line ^0
if formula:
"Every count is the smallest number of users that, holding need - 1 each, can hold the whole pool; one connection at a time never deadlocks." ^0
def one():
ask_int("pool size (1 to 8)> ", 1, 8) => size
if size < 0:
return
ask_int("connections each user needs (1 to 4)> ", 1, 4) => need
if need < 0:
return
ask_int("users (1 to 8)> ", 1, 8) => users
if users < 0:
return
pool.deadlock_possible(size, need, users) => r
if not r[0]:
("No order of borrowing deadlocks: " + str(users) + " users needing " + str(need) + " each, pool of " + str(size) + ".") ^0
return
"" => held
for h in r[1]:
if held != "":
held + ", " => held
held + str(h) => held
("Deadlock: every connection held, the waiting users holding " + held + " of the " + str(need) + " each needs, and none can borrow another.") ^0
"== Connection pool ==" ^0
"A fixed number of connections, borrowed by jobs and given back - or not." ^0
True => running
while running:
"" ^0
"1) jobs 2) deadlock table 3) one deadlock 4) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
jobs()
elif choice == "2":
table()
elif choice == "3":
one()
elif choice == "4":
False => running
else:
"Pick a number from 1 to 4." ^0
"Bye." ^0
Python projection (main.py)
import pool
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 pad(s, n):
out = s
while len(out) < n:
out = out + " "
return out
def lpad(s, n):
out = s
while len(out) < n:
out = " " + out
return out
def ask_int(prompt, low, high):
t = plain(input(prompt))
if t == "":
print("Cancelled.")
return 0 - 1
if len(t) > 2:
print("Type a whole number from " + str(low) + " to " + str(high) + ".")
return 0 - 1
for c in t:
if c < "0" or c > "9":
print("Type a whole number from " + str(low) + " to " + str(high) + ".")
return 0 - 1
if int(t) < low or int(t) > high:
print("Type a whole number from " + str(low) + " to " + str(high) + ".")
return 0 - 1
return int(t)
def jobs():
size = ask_int("pool size (1 to 6)> ", 1, 6)
if size < 0:
return
print("Each job leaves its body at the end, by break, by return or by raise.")
t = plain(input("jobs (such as end break return raise end, up to 12)> "))
if t == "":
print("Cancelled.")
return
js = []
w = ""
for c in t + " ":
if c == " ":
if w != "":
if w != "end" and w != "break" and w != "return" and w != "raise":
print("Each job is end, break, return or raise.")
return
js = js + [w]
w = ""
else:
w = w + c
if len(js) > 12:
print("Up to 12 jobs.")
return
a = pool.run_jobs(size, js, "by hand")
b = pool.run_jobs(size, js, "with")
print("Pool of " + str(size) + "; connections out after each job:")
print(" job leaves given back by hand with a with block")
for k in range(0, len(js)):
print(" " + lpad(str(k + 1), 3) + " " + pad(js[k], 7) + " " + pad(cell(a[k]), 30) + " " + cell(b[k]))
stuck = 0
for r in a:
if not r[2]:
stuck = stuck + 1
left = a[len(a) - 1][1]
if left == 0:
print("By hand: every connection given back.")
else:
print("By hand: " + str(left) + " of " + str(size) + " never given back, by the jobs that left early.")
if stuck > 0:
print(" " + str(stuck) + " later jobs found no connection free.")
print("With a with block: every connection given back, however the body left.")
def cell(r):
if not r[2]:
return "none free: waits forever"
return str(r[1]) + " out"
def table():
print("Users borrowing one connection after another, holding each until they have all they need:")
print("the fewest users for which some order of borrowing deadlocks (- for none up to 12).")
print(" needs pool 2 pool 3 pool 4 pool 5 pool 6")
formula = True
for need in range(1, 5):
line = " " + pad(str(need), 6)
for size in range(2, 7):
c = pool.first_deadlock(size, need, 12)
if c == 0:
line = line + lpad("-", 8)
if need > 1:
formula = False
else:
line = line + lpad(str(c), 8)
if need == 1 or c * (need - 1) < size or (c - 1) * (need - 1) >= size:
formula = False
print(line)
if formula:
print("Every count is the smallest number of users that, holding need - 1 each, can hold the whole pool; one connection at a time never deadlocks.")
def one():
size = ask_int("pool size (1 to 8)> ", 1, 8)
if size < 0:
return
need = ask_int("connections each user needs (1 to 4)> ", 1, 4)
if need < 0:
return
users = ask_int("users (1 to 8)> ", 1, 8)
if users < 0:
return
r = pool.deadlock_possible(size, need, users)
if not r[0]:
print("No order of borrowing deadlocks: " + str(users) + " users needing " + str(need) + " each, pool of " + str(size) + ".")
return
held = ""
for h in r[1]:
if held != "":
held = held + ", "
held = held + str(h)
print("Deadlock: every connection held, the waiting users holding " + held + " of the " + str(need) + " each needs, and none can borrow another.")
print("== Connection pool ==")
print("A fixed number of connections, borrowed by jobs and given back - or not.")
running = True
while running:
print("")
print("1) jobs 2) deadlock table 3) one deadlock 4) quit")
choice = plain(input("choice> "))
if choice == "1":
jobs()
elif choice == "2":
table()
elif choice == "3":
one()
elif choice == "4":
running = False
else:
print("Pick a number from 1 to 4.")
print("Bye.")
pool.eml
eml# P128 connection pool - a fixed number of connections, borrowed and given
# back. As in the corpus case connection-pool-release, a body can leave in
# four ways - at its end, by break, by return, by raise - and only a with
# block gives the connection back on all four; giving it back by hand at the
# end of the body leaks it on the other three. As in pool-reentrancy-
# deadlock, a request that holds one connection while it borrows the next
# can leave every connection held and nobody able to finish.
class Pool:
def __init__(self, size):
size => self.size
0 => self.out
0 => self.leaked
def take(self):
if self.out >= self.size:
return False
self.out + 1 => self.out
return True
def give(self):
self.out - 1 => self.out
def lease(self):
return Lease(self)
class Lease:
def __init__(self, pool):
pool => self.pool
def __enter__(self):
return self.pool
def __exit__(self, exc_type, exc_value, tb):
self.pool.give()
return False
def body_by_hand(pool, how):
# the job: borrow, work, give back at the end - unless it leaves first
for attempt in [1:2]:
if how == "break":
break
if how == "return":
return "returned"
if how == "raise":
raise ValueError("failed")
pool.give()
return "done"
return "broke out"
def by_hand(pool, how):
# [what happened, whether it ran]
if not pool.take():
return ["no connection free: it would wait forever", False]
try:
body_by_hand(pool, how) => r
except ValueError:
"raised" => r
return [r, True]
def body_with(pool, how):
for attempt in [1:2]:
with pool.lease():
if how == "break":
break
if how == "return":
return "returned"
if how == "raise":
raise ValueError("failed")
return "done"
return "broke out"
def with_block(pool, how):
if not pool.take():
return ["no connection free: it would wait forever", False]
try:
body_with(pool, how) => r
except ValueError:
"raised" => r
return [r, True]
def run_jobs(size, jobs, style):
# per job [how it left, connections out after, ran]
Pool(size) => p
[] => out
for how in jobs:
if style == "by hand":
by_hand(p, how) => r
else:
with_block(p, how) => r
out + [[r[0], p.out, r[1]]] => out
return out
def deadlock_possible(size, need, users):
# can some order of borrowing leave all connections held, each user
# holding fewer than it needs? Every state of how many each holds is
# searched; a user that reaches its need finishes and gives all back.
[0] * users => start
{} => seen
1 => seen[str(start)]
[start] => todo
while len(todo) > 0:
todo[len(todo) - 1] => st
todo[0:len(todo) - 1] => todo
0 => held
for h in st:
held + h => held
size - held => free
if free == 0 and len(st) > 0:
return [True, st]
if free > 0:
for i in [0:len(st) - 1]:
if i == 0 or st[i] != st[i - 1]:
[] => nxt
for j in [0:len(st) - 1]:
if j == i:
if st[j] + 1 < need:
nxt + [st[j] + 1] => nxt
else:
nxt + [st[j]] => nxt
sort(nxt) => nxt
if not (str(nxt) in seen):
1 => seen[str(nxt)]
todo + [nxt] => todo
return [False, []]
def sort(xs):
[] => out
for x in xs:
[] => nxt
False => placed
for y in out:
if not placed and x < y:
nxt + [x] => nxt
True => placed
nxt + [y] => nxt
if not placed:
nxt + [x] => nxt
nxt => out
return out
def first_deadlock(size, need, most):
# the fewest users, up to most, for which a deadlock is possible; 0 if none
for c in [1:most]:
if deadlock_possible(size, need, c)[0]:
return c
return 0
Python projection (pool.py)
class Pool:
def __init__(self, size):
self.size = size
self.out = 0
self.leaked = 0
def take(self):
if self.out >= self.size:
return False
self.out = self.out + 1
return True
def give(self):
self.out = self.out - 1
def lease(self):
return Lease(self)
class Lease:
def __init__(self, pool):
self.pool = pool
def __enter__(self):
return self.pool
def __exit__(self, exc_type, exc_value, tb):
self.pool.give()
return False
def body_by_hand(pool, how):
for attempt in range(1, 3):
if how == "break":
break
if how == "return":
return "returned"
if how == "raise":
raise ValueError("failed")
pool.give()
return "done"
return "broke out"
def by_hand(pool, how):
if not pool.take():
return ["no connection free: it would wait forever", False]
try:
r = body_by_hand(pool, how)
except ValueError:
r = "raised"
return [r, True]
def body_with(pool, how):
for attempt in range(1, 3):
with pool.lease():
if how == "break":
break
if how == "return":
return "returned"
if how == "raise":
raise ValueError("failed")
return "done"
return "broke out"
def with_block(pool, how):
if not pool.take():
return ["no connection free: it would wait forever", False]
try:
r = body_with(pool, how)
except ValueError:
r = "raised"
return [r, True]
def run_jobs(size, jobs, style):
p = Pool(size)
out = []
for how in jobs:
if style == "by hand":
r = by_hand(p, how)
else:
r = with_block(p, how)
out = out + [[r[0], p.out, r[1]]]
return out
def deadlock_possible(size, need, users):
start = [0] * users
seen = {}
seen[str(start)] = 1
todo = [start]
while len(todo) > 0:
st = todo[len(todo) - 1]
todo = todo[0:len(todo) - 1]
held = 0
for h in st:
held = held + h
free = size - held
if free == 0 and len(st) > 0:
return [True, st]
if free > 0:
for i in range(0, len(st)):
if i == 0 or st[i] != st[i - 1]:
nxt = []
for j in range(0, len(st)):
if j == i:
if st[j] + 1 < need:
nxt = nxt + [st[j] + 1]
else:
nxt = nxt + [st[j]]
nxt = sort(nxt)
if not str(nxt) in seen:
seen[str(nxt)] = 1
todo = todo + [nxt]
return [False, []]
def sort(xs):
out = []
for x in xs:
nxt = []
placed = False
for y in out:
if not placed and x < y:
nxt = nxt + [x]
placed = True
nxt = nxt + [y]
if not placed:
nxt = nxt + [x]
out = nxt
return out
def first_deadlock(size, need, most):
for c in range(1, most+1):
if deadlock_possible(size, need, c)[0]:
return c
return 0