BTM Model

Bio Task Manager (BTM) Model

English | 中文 | Русский | Español | Português | 繁體中文 | Deutsch

Formal model of concurrency in BioLang: cooperative threads and the task manager. Builds on the Bio Running (BR) Model.

1. Tasks and threads

Definition 1.1 (Thread). A thread is an execution context:

t = (ctx, area, boothₜ, state)

• ctx — the saved machine context (ucontext on POSIX, fiber on Windows).
• area — the thread's private area layer (an Areastream).
• boothₜ — the thread's phone-booth region (for @call methods).
• state ∈ {Ready, Running, Blocked, Done}.

Definition 1.2 (Task). A task is a scheduled unit of work:

task = (m, a⃗, t)

a method m with argument vector a⃗ bound to a thread t. The task manager (Taskm) is a dispatcher over the task set.

2. Cooperative scheduling

Axiom 2.1 (Cooperation). Scheduling is cooperative: a thread runs until it yields (Threads::yield()), blocks (Threads::join), or finishes. There is no preemption — the run queue changes only at explicit suspension points.

Definition 2.2 (Run queue). The scheduler maintains a FIFO queue Q = [t₁, t₂, ..., tₙ] of Ready threads. The transition:

Q = [t, ...]  ⟹  run t until t yields/blocks/done

After t suspends: if t is Done, it leaves the queue; otherwise it is appended: Q = [... , t].

Axiom 2.3 (Fairness). The FIFO discipline guarantees eventual progress for every non-blocked thread: each thread is scheduled within finitely many suspension points. (No starvation by construction.)

3. Task manager semantics

Definition 3.1 (Task set). Taskm maintains a multiset of tasks T = {τ₁, ..., τₖ} plus a rotation interval δ (ms).

Definition 3.2 (Rotation). With Taskm::interval(δ), the dispatcher rotates the ready task set every δ milliseconds: each task receives a time slice bounded by δ, then yields back to the dispatcher. Taskm::run() executes until T = ∅.

Axiom 3.3 (Completeness). Taskm::run() terminates iff every task in T terminates.

4. Synchronization primitives

Definition 4.1 (Join). Threads::join(t) blocks the caller until t is Done, then returns t's result:

join(t) = Res(v)   if t.state = Done ∧ res(t) = v

While a thread is Blocked on a join, it is not in the run queue.

Definition 4.2 (Self and active). Threads::self() returns the calling thread's identifier; Threads::active() returns the number of non-Done threads.

5. Concurrency properties

Theorem 5.1 (Atomicity of non-suspending steps). Between suspension points, a thread's execution is atomic with respect to other threads: no other thread can observe intermediate states.

Proof sketch. There is no preemption (2.1); the interpreter runs one thread's code at a time; context switches happen only at yields/blocks/joins. ∎

Corollary 5.2 (No data races). In the BR model, shared state (the arena, globals) is accessed only by the currently running thread at any instant. Without preemption there are no interleavings, hence no data races in the classical sense.

Remark. This is the standard trade-off of cooperative models: races are impossible, but a thread that never yields can starve others (2.3 requires explicit yielding for progress).

Theorem 5.3 (Booth isolation under threads). Two threads invoking the same @call method never share memory:

boothₜ₁ ≠ boothₜ₂   for t₁ ≠ t₂

Proof. Booth regions are per-thread by construction (Def. 1.1), and booth discipline (BR 5.2) confines a @call method's allocations to its thread's booth. ∎

Theorem 5.4 (Global booth mutual exclusion). For a @ucall method u, at most one thread executes u at any instant; concurrent entry is refused (returning Ref), not queued:

⟦u(a⃗)⟧ = Ref("phone-booth method u does not support recursion")
         when booth_global.in_use

Proof. The global booth has a single in_use flag (BR 5.2.2); a second thread entering while it is set is refused. ∎

Definition 5.5 (Join graph). The join relation forms a directed graph G = (Threads, {(a, b) : a joined b}). Cycles in G are a deadlock:

deadlock ⇔ ∃ cycle t₁ → t₂ → ... → t₁

Theorem 5.6 (Deadlock detection). A cyclic join graph implies a configuration with no Ready thread; the scheduler reaches a quiescent state and Taskm::run() cannot complete. BioLang detects this at the language level as a stuck state (the cooperative model makes cycles observable and reproducible).

6. The task manager as a game

Metaphor. A kitchen with several chefs (threads) and a single stove (processor): the head chef (Taskm) gives each chef a slice of time at the stove (interval), and a chef must step back (yield) when the timer rings. join is waiting for a chef to finish plating a dish before serving. Phone booths are the recipe cards: each chef has their own copy (@call), or the single communal recipe (that only one chef may read at a time) (@ucall).

7. BR × BTM summary

Aspect	BR model	BTM model
Unit	request / stream	thread / task
State	arena + layers + booths	run queue + join graph
Failure	Ref value, total semantics	stuck states (cyclic join), refused booth entry
Memory	stable arena, zero-move	per-thread booths, global booth mutex
Concurrency	— (single flow)	cooperative, no preemption, no races

Together they give a complete account: BR explains how one request changes the world; BTM explains how many requests share the world.