<!-- canonical: https://efficientnewlanguage.org/eml-p/projects/P128-connection-pool/ | updated: 2026-10-17 -->

# 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.

EML-P project `projects/connection-pool` in the EML language repo: 2 module(s), entry `main.eml`, terminal UI. There, `eml project run projects/connection-pool` runs it and `eml project verify projects/connection-pool` 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: connection-pool-release (https://efficientnewlanguage.org/cases/186-connection-pool-release/), pool-reentrancy-deadlock (https://efficientnewlanguage.org/cases/285-pool-reentrancy-deadlock/).

## Sessions

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

Input:

```text
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
```

Screen:

```text
== 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.
```

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

Input:

```text
1
3
end break return raise end end
2
3
4
2
4
3
4
2
3
4
```

Screen:

```text
== 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.
```

## Modules

### main.eml

```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 of main.eml:

```python
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 of pool.eml:

```python
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
```

## README

# P128 - Connection pool

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 case
- `pool.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).