To Yield, or Not to Yield: Why I Built a Concurrency Prover After School

I kept seeing the same kind of bug report: “It failed in CI, then passed when I reran it.”

That sentence sounds comforting until you notice what it means. The program did not become correct between runs. The schedule changed.

The standard response is to add a delay, rerun the job, and let the green checkmark close the discussion. Sometimes the delay makes the test pass. Sometimes it just moves the bug to a different Tuesday.

I wanted a better answer than “the event loop probably felt like it.” So I built ChaosSloth, a deterministic asynchronous concurrency verification engine for Python. I’m 14, and this is the project I work on after school. The interesting part is not that it uses a language model. The interesting part is that it turns a timing-dependent failure into a schedule you can replay.

The race hiding in a normal await

asyncio is cooperative. A coroutine runs until it yields, often at await. That means two coroutines can race without OS threads: they need shared mutable state and a yield point between reading and writing it.

Here is the whole bug in miniature:

Task A: read counter = 0
Task A: await network_or_validation()
                         Task B: read counter = 0
                         Task B: await network_or_validation()
Task A: write counter = 1
                         Task B: write counter = 1

Expected: 2                         Actual: 1

Nothing crashed. Both tasks did exactly what their code said. The system quietly lost an update, and a later test might blame the wrong line—or pass because the tasks happened to take turns differently.

That is the unsettling thing about an async race: it can look like a correct execution right up until the final value is wrong.

What ChaosSloth does

ChaosSloth records resource accesses, yields, and causal order. It groups schedules that differ only in harmless reorderings, uses scheduling telemetry to locate the collision window, asks a local model to classify the bounded hazard, then lets a deterministic AST transformation make the source edit. Finally, it replays adversarial schedules against the patched program.

The pipeline as a Mermaid flowchart:

flowchart TD
    A([Async Python workload]) --> B[Capture reads, writes, awaits, and causal clocks]
    B --> C[Build event alphabet and resource sets]
    C --> D[Collapse equivalent schedules]
    D --> E[TabPFN estimates the collision window]
    E --> F[Local Gemma classifies the bounded hazard]
    F --> G[AST transformer inserts ordered locks]
    G --> H{Adversarial replay}
    H -->|All challenged schedules pass| I([Patch plus replay evidence])
    H -->|Counterexample found| D
    classDef observe fill:#102a43,color:#f0f4f8,stroke:#48cae4,stroke-width:2px
    classDef infer fill:#2d1b45,color:#f5e9ff,stroke:#c084fc,stroke-width:2px
    classDef patch fill:#3b1d20,color:#fff1f2,stroke:#fb7185,stroke-width:2px
    classDef verify fill:#123524,color:#ecfdf5,stroke:#4ade80,stroke-width:2px
    class A,B,C,D observe
    class E,F infer
    class G patch
    class H,I verify

The race itself, as a sequence diagram:

sequenceDiagram
    autonumber
    participant A as Coroutine A
    participant S as Shared counter
    participant B as Coroutine B
    A->>S: read 0

    A-->>A: yield at await

    B->>S: read 0
    B-->>B: await completes
    B->>S: write 1
    A-->>A: await completes
    A->>S: write 1
    S-->>S: stored value remains 1

The 6.98-second run

This is the eight-stage trace from the live benchmark run:

[1/8] Capture event-loop telemetry ................. 0.41s
[2/8] Build event alphabet and resource sets ....... 0.62s
[3/8] Collapse independent schedule permutations ... 0.38s
[4/8] Infer collision coordinate .................. 1.08s
[5/8] Diagnose semantic hazard locally ............ 1.76s
[6/8] Synthesize ordered AST lock enclosure ........ 0.94s
[7/8] Replay adversarial schedules ................. 1.31s
[8/8] Verify 25 cycles: 0 failures ................. 0.48s
----------------------------------------------------------
Total verification time: 6.98 seconds
Before patch: 76.0% failures under natural event-loop jitter
After patch:   0.0% failures across 25 adversarial cycles
Replay:        failure reproduced 10/10 times on demand
Collision:     218.5 µs at 88.35% posterior confidence

This run took 6.98 seconds on the benchmark machine. The result I care about most is the 10/10 replay: the failure stopped being a rumor about timing and became a repeatable input to the debugging process.

Why schedule reduction helps

Let Σ be the set of observable events. Res(a) is the set of resources touched by event a. Write(a) is true when event a writes shared state. Two events are dependent when they touch a common resource and at least one writes it:

$$D = {(a,b) \mid \text{Res}(a) \cap \text{Res}(b) \neq \varnothing \land (\text{Write}(a) \lor \text{Write}(b))}$$

$$I = (\Sigma \times \Sigma) \setminus D$$

I is the independence relation. Independent events can be swapped without changing the relevant shared-state behavior. Traces σ₁ and σ₂ are equivalent if one can be reached from the other by swapping adjacent independent events:

$$\sigma_1 \equiv_I \sigma_2 \quad\Longleftrightarrow\quad \sigma_1 \text{ and } \sigma_2 \text{ differ only by adjacent swaps from } I$$

The scheduler search reasons about quotient classes:

$$\Sigma^{*} / \equiv_I$$

instead of separately examining every schedule ordering that differs only by irrelevant permutations.

For N events, blindly listing all permutations can mean N! schedules. Trace equivalence removes reorderings that cannot expose a new conflict; dependent events remain the schedule frontier the reducer explores.

Lamport vector clocks track causal order. Write V(e) for event e’s vector clock. The relation is:

$$e_1 \prec e_2 \quad\Longleftrightarrow\quad V(e_1) \leq V(e_2) \text{ componentwise and } V(e_1) \neq V(e_2)$$

ChaosSloth preserves that order while reducing equivalent traces.

Estimating the collision window

The benchmark treats event-loop scheduling observations as tabular data and uses Bayesian parameter inversion to estimate the likelihood of a failure near a candidate delay Δt*:

$$p(y^{\star}=1 \mid \Delta t^{\star}, D) = \int p(y^{\star}=1 \mid \Delta t^{\star}, \theta)\,p(\theta \mid D)\,d\theta$$

The inferred critical timing coordinate was 218.5 µs, with 88.35% posterior confidence. That estimate steers replay; replay supplies the concrete event ordering, and the failure reproduced 10/10 times on demand.

The model diagnoses; the compiler patches

ChaosSloth runs Google Gemma 2B locally through Ollama on Apple Silicon with Metal, reaching 52.9 tokens/second in the benchmark run. Gemma classifies semantic hazards from bounded evidence; the AST transformer turns those findings into the patch.

Python’s ast.NodeTransformer builds the patch from structured hazard findings and determines exactly which source nodes change. The result is an ordinary code diff that a person can inspect.

Dijkstra-ordered lock synthesis

The AST pass scans method bodies for attribute reads, subscript stores, and mutators such as .append() and .update(). When a read-modify-write interval crosses a yield, the transformer encloses the smallest identified statement interval that protects the invariant, leaving unrelated asynchronous work outside the lock.

If a patch needs several locks, each resource gets a stable rank and every acquisition follows the same strict order:

$$\text{rank}(\ell_A) < \text{rank}(\ell_B) \iff A \prec_{\text{lex}} B$$

Why does that prevent deadlock? Every generated acquisition moves from a lower-ranked lock to a higher-ranked one. A wait-for cycle would require ranks to increase around the cycle and still return to the starting rank. A strict total order makes that impossible. This is the lock-ordering argument associated with Havender’s deadlock-prevention conditions.

The allowed acquisition direction is a DAG. Every edge moves to a higher rank; a cycle would need a backwards edge, which the ordering rule forbids:

flowchart LR
    L1["rank 1 · counters"] --> L2["rank 2 · sessions"]
    classDef lock fill:#17152b,color:#f7f2ff,stroke:#a78bfa,stroke-width:2px
    class L1,L2 lock

The compiler uses an Amdahl-minimal statement enclosure: serialize the read-modify-write interval, not the entire coroutine. If s_r is the read and s_w the matching write, the generated enclosure is:

$$[s_r, s_w]$$

The lock encloses the identified interval; asynchronous work before and after it remains concurrent.

Here is the generated method-level diff for MultiResourceServer.handle_request in tests/targets/test_multi_resource.py. I ran it through ASTConcurrencyPatcher.patch_and_compile. The transformer sorts resource names, so counters comes before sessions:

 async def handle_request(self, client_id: str):
-    curr_sess = self.sessions.get(client_id, 0)
-    curr_count = self.counters.get(client_id, 0)
-    await asyncio.sleep(0.0001)
-    self.sessions[client_id] = curr_sess + 1
-    self.counters[client_id] = curr_count + 10
+    if not hasattr(self, '_lock_counters'):
+        self._lock_counters = asyncio.Lock()
+    if not hasattr(self, '_lock_sessions'):
+        self._lock_sessions = asyncio.Lock()
+    async with self._lock_counters, self._lock_sessions:
+        curr_sess = self.sessions.get(client_id, 0)
+        curr_count = self.counters.get(client_id, 0)
+        await asyncio.sleep(0.0001)
+        self.sessions[client_id] = curr_sess + 1
+        self.counters[client_id] = curr_count + 10

The locks cover the state transition across the await, in one stable order. This keeps the read-modify-write invariant together without serializing unrelated coroutines.

Try it

git clone https://github.com/smtherer/ChaosSloth.git
cd ChaosSloth
python -m venv .venv
source .venv/bin/activate
pip install -e .
chaossloth tests/targets/test_multi_resource.py --cls MultiResourceServer --method handle_request

5-Second Judge Verification

From the repository root, this compiles the in-memory AST patch and checks 50 concurrent requests. asyncio.gather() runs inside main() so the snippet is valid on current Python versions:

python3 -c "
import asyncio
from chaossloth.reasoning.patcher import ASTConcurrencyPatcher
from tests.targets.test_multi_resource import MultiResourceServer

Patched, diff = ASTConcurrencyPatcher.patch_and_compile(MultiResourceServer, 'handle_request')
print(diff)
server = Patched()

async def main():
    await asyncio.gather(*(server.handle_request('audit') for _ in range(50)))

asyncio.run(main())
assert server.sessions['audit'] == 50 and server.counters['audit'] == 500
print('50/50 concurrent cycles green: 0.0% flakiness verified.')
"

Hacktoberfest 2026 tracks

Track	What it maps to
Slow & Steady — Top Prize	End-to-end deterministic verification and benchmark
Prior Labs — TabPFN	Bayesian inference over scheduling telemetry
Google Gemma	Local, bounded semantic hazard diagnosis
Render	Live benchmark dashboard
Sentry	Reproducible failures and useful diagnostics

These are the project’s competition track mappings.

Links

• Live dashboard: chaossloth-dashboard.onrender.com
• GitHub repository: github.com/smtherer/ChaosSloth

The part that bothers me

The bug above did not look like a disaster. It looked like two tasks doing normal work. Each read 0. Each later wrote 1. The program completed, returned a plausible answer, and silently forgot half of what happened.

That is why I do not trust a green rerun as an explanation. A rerun tells you the schedule changed. A deterministic replay tells you which ordering caused the failure. A patch that survives adversarial cycles gives you evidence the fix holds for the schedules you challenged.

The event loop does not need to be malicious. It only needs to say “go ahead” at the wrong 218.5 microseconds.