Region Ownership: Unifying the Priority-Ceiling Protocol and DMA Handshakes in a Bare-Metal Language

A compiler for a microcontroller normally models a single bus master: the CPU. But memory correctness on a modern MCU is a property of the whole system — CPU cores, DMA engines, caches, and the bus matrix that connects them. The resulting bugs are silent: a buffer placed in memory the DMA engine cannot reach, a cache line the DMA never sees, a descriptor armed before the CPU has finished writing it. We describe BML, a language and compiler (beemel) for ARM Cortex-M firmware, built around two ideas. First, every bus master is a first-class agent with its own reach, cache view, and permissions, and CPU/DMA memory sharing is checked at compile time. Second — our central claim — the CPU priority-ceiling protocol (mutual exclusion between interrupt and thread contexts) and the asynchronous DMA release/reclaim handshake are one concept, region ownership, with the synchronization mechanism derived from the set of sharers — the programmer declares the sharing and the ownership window, not which exclusion protocol to emit. The model was built failure-first: every check traces to a specific hardware bug we provoked on a development board, and the result was validated back on silicon across three DMA architectures (ST crossbar, RP2350 per-channel, nRF51 fixed-block). We position the work against the priority-ceiling literature (which covers the CPU half only) and the formal DMA-isolation and OS memory-model literature (which treats DMA but never unifies it with CPU-side mutual exclusion). These are compile-time analyses plus a test suite, not formal proofs; we are explicit about the resulting trust boundary.