Concurrency disposition: data-race foreclosure + deadlock/weak-memory gaps

Goal

Concurrency disposition: data-race foreclosure + deadlock/weak-memory gaps. Facet of the UB-disposition model: every miri-enumerated UB class in this section’s scope is dispositioned and (where claimed foreclosed) pinned.

Implementation Sketch

Populate the coverage matrix rows owned by this section; ground every disposition in actual Ori spec/source (cite file:line or spec clause); add the pin / verification surface the disposition claims.

Spec References

• spec Clause 4.5 (04-conformance.md:32) — no silent UB
• missions.md §AIMS, §Compiler

Work Items

• Pin data-race foreclosure: a spec/AOT pin demonstrating Sendable + capture-by-value forbids the shared-mutable access miri’s data-race detector targets.
• Record deadlocks + weak-memory ordering + intentional leaks as GAP rows, each with a concrete tracked hardening anchor (plan checkbox / filed bug), never an untracked note.

Fresh intel (regenerated)

{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-05431ad0” }, “generated_at”: “2026-06-25T19:50:50.064953+00:00”, “graph_state”: { “head_sha”: “adb80a77”, “last_code_import_at”: “2026-06-25T19:50:47.717Z”, “embedding_stale”: true, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-05431ad0] agent-authored dossier”, “degraded”: false, “dossier”: { “objective_symbols”: [], “tiers”: {}, “agent_authored”: true, “difficulty”: { “class”: “routine”, “research_online”: false, “research_mode”: “auto”, “signals”: [], “plan_dir”: “/home/eric/projects/ori_lang/plans/ub-safety-threat-model” } } }

(full dossier: concurrency-disposition—s-05431ad0.intel.json)