Executors and shutdown

ThreadPoolExecutor(max_workers: Positive[i64], queue_capacity: Positive[i64]) returns Result[ThreadPoolExecutor, PoolError]. Both counts are Positive[i64]; positive literals convert at compile time, and computed counts use Positive.try_from(count)?. Construction starts all fixed native workers before success and provides a bounded FIFO queue. Partial startup failure stops and joins workers already started. PoolError has Allocation(AllocError) and Thread(ThreadError).

cancel_pending() does not wait for running jobs. It removes the queued jobs, so their queue slots are free for later submissions; their futures report FutureError.Cancelled, and each job’s captures are dropped with its future. To stop without running queued work, call pool.cancel_pending() and then pool.shutdown(). shutdown() takes no argument; shutdown(True) is rejected with a diagnostic naming cancel_pending().

Methods observe the pool; mut is unnecessary. Executors are affine and do not support copying or equality. Jobs may differ in concrete argument/result types on one pool. Reusable closures run once then release their environment; one-shot closures transfer captures into their body. Named submissions infer ordinary argument types and return a callable bound job on failure.

Inputs and results must be wholly owned and satisfy the worker checks. Jobs share state through Shared[T] handles: pass each job its own handle.share(). Borrowed captures/arguments, generator frames, and uncertified indirect effects are rejected. Executors and futures cannot enter workers.

User jobs must own their inputs because a future can outlive the borrow that would feed it. Parallel pipelines are the one internal exception: .par chunk jobs read a list’s rows in place, which is sound because every .par terminal waits for all submitted jobs before returning, including after a failed submission. User-facing scoped pool jobs, a deferred B22 extension, would build on the same guarantee. Channel protocols can still deadlock.

SubmitError[F] has Full(job), Shutdown(job), OutOfMemory(job), and CapacityOverflow(job). Each owns the complete unstarted job for retry, synchronous invocation, or drop. A named submission’s job is a one-shot closure binding the arguments, so pool.submit(stopped, token)? can propagate as SubmitError[OnceClosure[[], bool]]; a signature names jobs as for owned starts. pool.submit(job).drop_job()? instead drops the job of a rejected submission at the call and gives SubmitError[()] with the same variant, such as Shutdown(()); one such member covers every job, as for job-free start errors. Blocking submit never returns Full. Shutdown is reported before job allocation; waiting for space precedes allocation and transfer. submit_nowait can contend on synchronization.

Construction uses one allocation; each accepted job needs one fallible cell. Status, cancellation, result transfer, waiting, and shutdown allocate nothing.

Lifetime

with ThreadPoolExecutor(workers, capacity)? as pool: owns the executor and lends &ThreadPoolExecutor. Every normal exit drains accepted work and joins workers; ordinary drop does the same. Explicit shutdown is idempotent and always waits. Detachment and wait=False are unsupported; running jobs are not forcibly killed. Tokens permit cooperative stopping; a shutdown that could wait for a job holding a token before the function’s later cancel is rejected, and with ThreadPoolExecutor(...)? as pool, stop.cancel_on_exit(): cancels it on every exit. See cancel on every exit.

Workers must finish their communication before the scope can close. See futures for result ownership and parallel operations for batched work.

Shutdown and live receivers

Shutdown waits for every accepted job, and a job waiting for queue space is released only by a receive or by the drop of the last receiver. The compiler therefore applies the task join rule to pools:

A pool cannot be shut down while a live binding of the function can hold Receiver[T], once the function has submitted a job that can hold Sender[T].

A pool shuts down at pool.shutdown(), including through a &ThreadPoolExecutor, at drop(pool), when its binding is reassigned, and wherever its owner leaves scope: the end of its with block or of the function, return, ?, break, and continue. A call that receives a pool, by value or by reference, counts as a shutdown when a function it reaches, directly or through further calls, calls shutdown() or owns a pool. A call through a Callable, closure, or boxed callable value, or to a function that makes one, is assumed to shut down a pool passed to it. Locals are released last declared first, so a receiver bound after the pool is dropped before the pool shuts down.

Jobs are not matched to pools and are never assumed to have finished. A job submitted with submit or submit_nowait counts at every later shutdown in the function, and at every shutdown in a loop that contains the submission. A submit(...)? or submit(...).drop_job()? that fails has submitted nothing on the path that leaves. map, map_result, and reduce_tree finish their jobs before returning and do not count. What a job and a binding can hold is defined as for tasks.

The recommended patterns for tasks apply. When the function does not wait for the job’s result inside the block, guard the receiver as the last manager of the pool’s with, so every exit drops it before the pool shuts down:

with ThreadPoolExecutor(2, 8)? as pool, receiver as inbox:
    pool.submit(produce, sender).drop_job()?
    ...

That guard is still alive at a future.result() inside the block, which its own check rejects. To wait for the result, end the receiver’s guard first:

with ThreadPoolExecutor(2, 8)? as pool:
    future = pool.submit(produce, sender).drop_job()?
    with receiver as inbox:
        ...
    result = future.result()

A channel created inside the pool’s block, and a drop(receiver) on every path to the shutdown, also satisfy the rule. The holders of a task join apply too: a returned Ok(receiver), an unfinished pair = (receiver, future.result()?), or a match case whose value is receiver holds it through the shutdown. The diagnostic reports the shutdown or the pool’s binding, each binding, returned value, or unfinished expression that holds a matching receiver, where the job is submitted, and the early exit that reaches the shutdown.

The rule has the task rule’s false positives and gaps. It also rejects these safe programs:

• the job has finished, for example after future.result() returned;
• the job was submitted to a different pool than the one shutting down;
• a submit failure handled without ? returned the job to the caller.

It does not cover:

• a job submitted by another function, through a &ThreadPoolExecutor or a pool it returns;
• a pool passed to a call inside a class, tuple, or collection;
• a map, map_result, or reduce_tree callback that waits to send.

Blocking future retrieval has its own check at result(), before any later receiver cleanup.

Shutdown and held locks

A job waiting for a mutex this function holds would keep the shutdown waiting too. Submission therefore also records the guarded types of the Mutex[T] values a job can reach, including through Shared handles:

A pool cannot be shut down while the function holds a lock on a Mutex[T], once it has submitted a job that can reach a Mutex[T] of the same T.

Shutdown points, job counting, and the false positives are those of the receiver rule; mutexes are matched by type, as for joins under a lock. End the lock’s with block before the pool shuts down.