Cortex-M execution profile

Selected lanes and pins

tools.lock.json pins URLs and SHA-256 for every downloaded package, including shared-library dependencies and GDB's Python support. The portable Renode archive SHA-256 is 4ba7c68b59e2447f188ef4b4b112fcccd2802582c460beedceb63b84e5605a5f. The installer verifies archives before extraction. Each probe verifies the installation inventory and versions before execution, checks it again afterward, and retains that inventory. Debian 13 supplies the base libc and Python; this is a supported host profile, not a hermetic operating-system image.

These C probe flags select base AAPCS soft-float transport and ELF32 EABI. R6.20 separately selects the internal Landin transport described in the target guide. The compiler describes Cortex-M0 layout but has no Cortex-M emitter.

Memory and device map

The prototype is a sketch combining M0 CPU pressure with vendor-like registers; it does not identify a real part matching that whole map. The Renode platform is deliberately named prototype, not micro:bit or STM32. GPIO B, unused streams and unspecified UART registers are absent. Unknown modeled-register accesses and invalid access directions throw; unsupported bus widths generate warnings which fail the runner. Explicit halfword support covers the 16-bit count and GPIO data, without automatic read/modify/write translation. The linker refuses initialized data (this probe startup only clears BSS), a wrong vector extent, flash overflow and BSS entering the reserved stack area.

Why QEMU plus Renode

Current official QEMU documentation identifies the micro:bit's M0 and Nordic devices. Selection also inspects the pinned SoC implementation and runs the controls below. Device presence does not prove the prototype's behavior: Nordic GPIO/UART addresses differ, clock registers include stubs, and this is not a prototype DMA model. QEMU retains the mandatory CPU/startup role and R6.90's QEMU obligation is unchanged.

Renode's official documentation and peripheral modeling guide provide composable devices, bus access, IRQ wiring and C# models loaded from source. Those are useful here because the same firmware can execute against an explicit, small contract model. An independent host-only register simulator would not exercise CPU loads/stores and the NVIC together. Extending QEMU's native device tree would require a separately maintained emulator build. For this bounded lane, Renode's runtime model loading is the selected route.

Stock STM32 models were evaluated, not assumed faithful from a board list. The shipped binary identifies source f1dd1b4af; its Infrastructure submodule is cd4b002aac2398994c4a61a34a8b31b5700facf2, distinct from the release tag's submodule. The inspected DMA implementation implements request-driven copies and completion IRQs but tags CIRC, HTIE and TEIE. It does not supply the required circular reload or half/error behavior. The UART implementation can signal DMA reception; stock platform wiring alone does not establish that route. stock.repl explicitly connects it. stock.py demonstrates two received bytes reaching RAM, completion status/clear, GPIO set/reset and zero remaining count despite CIRC. Its expected warnings identify tagged CIRC and unclocked UART reception: this control proves no baud or idle-line behavior.

Executable routes and limits

Feeds happen while virtual execution is paused, followed by a fixed 1 ms virtual run and a checked firmware stage. No host sleep decides firmware success. Only the debugger socket startup uses a bounded readiness poll. The Renode time framework is execution scheduling, not physical bus timing. The model's transfer order is an explicit harness assumption. The ordinary C buffer is reloaded across opaque memory-clobber barriers; that is no definition of Landin DMA visibility. R6.30 must define races, tearing, atomics, compiler/hardware barriers and cache maintenance, with models for behaviors this cacheless M0 profile cannot expose. Supplemental hardware can test actual bus/interrupt timing, electrical behavior and a real device's DMA visibility; it cannot replace the emulator gates or by itself establish language concurrency semantics.

Reproduction and evidence

On the documented native Linux host, with Python 3 and dpkg-deb:

python3 environments/cortex-m/setup.py
python3 environments/cortex-m/test.py
python3 environments/cortex-m/run.py --output /absolute/new/evidence-directory

The default private tool root is ~/work/.cortex-m; --tools selects another installation. Setup refuses an existing root; install deliberately into a new root to change tools. No sudo, host package replacement, Linux container on the Mac, Nix job or compiler dependency is introduced. Missing tools, wrong pins/host, subprocess failures, deadline expiration, model errors, unexpected warnings and absent assertions all fail. Renode returning zero after a script error is insufficient: the runner requires the unique final marker and scans its log for failures. The stock control allows only its two known warnings.

After Renode exits, the runner removes only its verified empty renode.config.lock coordination file before inventorying evidence. Native export omits lock files, so recording that transient file would correctly fail export verification. Nonempty or linked replacements fail instead.

Each subprocess has a 30-second deadline, GDB 20 seconds, and QEMU startup three seconds; timeout cleanup terminates the owned process group, escalating after two seconds. Each run needs a new output directory and retains failure logs as well as successes. Evidence includes exact commands, version replies, installed file hashes, input hashes, linker maps, ELF headers/attributes, sizes, ELFs, generated GDB/Monitor scripts, logs, UART bytes and result.json.

The Linux acceptance documents job executes both the failure controls and these live probes from the same committed archive as every native job. job.py copies its cortex-m evidence into the exported, hash-verified bundle. Thus the annotated dual-native approval binds the environment's actual run, not only this document or a development transcript. Darwin retains native compiler/workload/LLDB evidence and does not impersonate this probe host. R6.10 selects routine scope with debugger coverage because it adds debugger control checks and changes acceptance commands/evidence retention. This is not the full R6.100 milestone matrix. Nix CI and scheduler/cache/resume work retain R5.51's dispositions.

The retained development result is indexed by validation.json. Its successful probe images contain 643 and 836 text bytes respectively, no initialized data and 24 BSS bytes each. These are environment-control sizes, not measurements of the future Landin driver or a stack-usage guarantee.

R6.20 layout and ABI evidence

The same mandatory run.py now also builds probes/abi.c and abi.S with the original pinned flags, startup and memory limits, then executes them in QEMU. Renode remains a separate peripheral lane; its result is never counted as ABI evidence. No library or tool pin changes. The additional ELF, disassembly, macro dump, GDB script/log, measured JSON and both layout contract inputs are retained in the existing exported cortex-m directory. The original Renode lock-file cleanup and its regression controls remain required.

Three independent comparisons meet:

1. The Ada cortex ABI suite computes scalar, aggregate, variant, evidence, any and multiple-result layouts and physical call plans from compiler packages, comparing with compiler/tests/cortex-m.contract. It also checks eight existing source fixtures through lowering and entry/direct/indirect planning under Cortex-M0 and synthetic-32, comparing detailed neutral IR. These are compiler-host tests, not target execution.
2. abi.py compares the contract with every original synthetic-32 row in layout.targets, without regenerating that golden. GCC independently lays out C control structures, unions and tables. QEMU/GDB reads their emitted measurements and compares them with the contract. Static assertions also cover data/code pointers, slices, ILP32, plain-char policy and 64-bit alignment. The C union is a representation control, not C semantics for a Landin variant.
3. Independently written assembly captures actual GCC-produced r0–r3, incoming sp and stack argument words. Assertions compare meaningful words with the compiler plan for double-word gaps, split 12-byte records, narrow stack arguments, soft floats, float-only records, promoted varargs and result-pointer displacement. Separate hand callers check GCC callees, and C callers check hand returns/callbacks, including 3/4/5-byte records and integer/double 64-bit results. Padding and skipped registers are unspecified and are not asserted as values.

The Landin convention has a separate handwritten witness: hidden aggregate result and direct/parent evidence addresses, an address-passed value, a stacked u64, successful and failing r12 outcomes, r0/r1 scalar results, multiple-result storage, and erased data/table dispatch through Thumb code pointers. GDB checks the nested r11 frame records, saved lr, chain termination and aligned sp; firmware checks callee-save registers and restoration. These execute the selected contract with real M0 instructions; they are not compiler-generated Landin calls or Landin source-debugging acceptance.

Compiler refusal/boundary controls cover wrong targets, unavailable C and emission capabilities, narrow extension, the four-byte C result threshold, empty C carriers, unpromoted varargs, declared C errors, stack-budget rounding and a target-overflowing argument without materializing it. Source checks cover pointer-sized integer/address overflow and the array byte-extent boundary. The Python controls refuse duplicate/missing/invalid contract rows, synthetic mismatches, missing markers, subprocess errors and timeouts. They preserve the R6.10 lock cleanup refusal for linked or nonempty replacements.

Every subprocess retains the original deadlines (GDB 20 seconds, build/tools 30, debugger readiness three) and owned process-group cleanup. The final exact-archive Linux documents job repeats all lanes and retains tool/input hashes alongside the new ABI artifacts. Its ordinary dual-native approval binds these results to the same revision as the hosted checks. Development results are indexed separately in abi-validation.json; validation.json keeps its historical R6.10 meaning.

These bounded probes establish neither floating arithmetic helpers, general unwind support, a complete C language ABI surface, firmware stack bounds, physical hardware behavior nor a Cortex-M compiler backend. R6.50 must consume the plans with native selection and frame code; R6.60 must implement image placement/startup; R6.100 must establish Landin debugging and stack evidence. R6.30/R6.40 retain concurrency and invalid packed encodings. Existing resource, evidence, scheduling, Nix and general-generator dispositions are unchanged.