Prove It By Construction, Not By Testing: Partitioning Away A Failure Class

Mostafa Dhouib·10 min read

Prove It By Construction, Not By Testing: Partitioning Away A Failure Class

The short answer. On a tightly coupled memory architecture, two real-time paths that use the same memory bank contend for it, and the contention shows up somewhere else entirely as a buffer underrun. The instinct is to chase the underrun: raise a priority, enlarge a buffer, run a longer soak. All of that makes the failure rarer without making it impossible, and rarer is the worst outcome, because it moves the failure from your bench to the field. Partition the memory and the direct-memory-access ownership so each real-time path has its own bank and its own channel, and the collision stops being improbable and becomes impossible. There is nothing left to stress test, because there is nothing left to collide.

A neuro wearable has at least two paths that cannot be late. One acquires samples from a front end at a fixed rate. One feeds an output peripheral that consumes data at a fixed rate and will not wait.

The firmware worked. Then, occasionally, under no pattern anyone could name, the output path glitched.

A buffer underrun is a symptom with a long causal distance

An underrun is simple to describe. A peripheral consumes data at a fixed rate out of a small hardware queue. Something was supposed to refill that queue before it emptied. It did not arrive in time. The peripheral runs out, and what you observe is a click, a dropped frame, a discontinuity in the output waveform, or an error flag you only see if you were already looking for it.

The description is simple and the cause is not, because the thing that was late is almost never the thing that reports the lateness. The queue emptied because a transfer was delayed. The transfer was delayed because something else held the resource it needed. That something else is usually on an unrelated path, owned by a different part of the codebase, written by a different person, and entirely healthy by its own measurements.

So you get a defect report that points at the output path and a root cause that lives in the acquisition path. The debugging session that follows is long, and the fix that comes out of it is usually a tuning change rather than a structural one.

What tightly coupled memory gives you, and what it quietly takes away

Tightly coupled memory sits close to the core and is deterministic to access. No cache, no wait states, no variance. That determinism is exactly why you put a real-time path there. You want the cost of a load to be the same every time, so that your worst-case timing argument is an argument rather than a hope.

The part that gets missed is that the determinism is per access, not per system. The memory is divided into banks. The core is one master on the internal bus. Each direct-memory-access controller is another. When two masters target the same bank in the same cycle, something has to arbitrate, and arbitration means one of them waits.

A single waited cycle is nothing. The problem is that contention is not a single cycle. A streaming transfer touches a bank repeatedly, and a core running a tight loop against the same bank touches it repeatedly too, so the two interleave and both run slower than either one modelled in isolation. Your timing budget was computed for the isolated case. The real system runs the overlapped case, and only sometimes, because whether the two paths overlap depends on the phase relationship between two independent rates, on which branch the code took, and on how much data happened to be queued.

That is the recipe for a bug that does not reproduce. It is load dependent, phase dependent and data dependent, and none of those three are things your test harness controls.

Partitioning is a statement about what cannot happen

The structural fix is to stop the two paths from ever being candidates for the same arbitration.

Give each real-time path its own memory bank. Put the buffers for the acquisition path in one bank and the buffers for the output path in another. Keep the hot code and hot data of whichever path runs on the core out of the bank a controller is streaming through. Assign each buffer a single owning channel, so no two transfers can be pointed at the same region by a configuration error.

Once that is done, the statement you can make about the system changes category. Before partitioning, the statement was "contention is rare and we have not seen an underrun in a long test". After partitioning, the statement is "the two paths do not address the same bank, therefore they cannot arbitrate against each other, therefore this cause of underrun does not exist here".

The second statement is checkable by reading. A linker script, a memory map and a channel assignment table are three artefacts a reviewer can inspect in an afternoon. The first statement is only ever checkable by running for longer, and running for longer never terminates in a proof.

Why chasing the symptom is the wrong move even when it works

The tuning fixes are not useless. A bigger buffer genuinely buys more slack. A higher priority genuinely gets a transfer serviced sooner. The objection is not that they do nothing, it is what they do to the shape of the risk.

They move the failure rate below your observation threshold, not to zero. A failure you cannot reproduce on the bench still occurs at a rate. Multiply that rate by a fleet and by a duty cycle and you get a support queue.

They are sensitive to every later change. Slack created by a buffer size is consumed by the next feature that adds work to the path. Nothing in the build tells you that you have spent it.

They make the system harder to reason about. A priority assignment chosen to fix one observed glitch encodes a conclusion nobody wrote down. Two years later it looks arbitrary, someone changes it, and the glitch returns with no visible connection to the commit that caused it.

They produce test suites that assert the absence of a symptom. A soak test that watches for underruns is a test whose passing means nothing happened during the window. That is the weakest form of evidence a test can produce.

The general rule: when a failure class follows from shared ownership, remove the sharing

The memory bank case is one instance of a pattern that shows up throughout embedded work and in systems generally. If the mechanism of a failure is "two things used the same thing", then the failure is a property of the sharing and not of either participant, and no amount of improving either participant removes it.

Two writers to one buffer produce torn reads. The fix is single-writer ownership with an explicit handoff, not a lock somebody has to remember to take.

An interrupt handler and a task touching the same mutable state produce a race. The fix is to transfer ownership through a queue, so the state is only ever reachable from one context at a time.

A shared heap in a real-time path produces non-deterministic allocation and fragmentation. The fix is static allocation sized to the worst case, which converts a runtime failure into a build-time one.

A serial bus shared between a time-critical transfer and a bulk transfer produces missed deadlines. The fix is a dedicated bus or an enforced time division, not a retry.

In each case there is a tempting alternative that reduces frequency: a lock, a careful calling convention, a retry, a bigger buffer. The structural version costs more up front in memory, parts or layout, and it returns a property you can state and a reviewer can verify.

What you still have to test

Partitioning removes one cause of underrun. It does not remove the others, and the others are real.

You still have to establish that each path meets its deadline in isolation, because partitioning protects a path from the other path and not from itself. You still have to establish that whatever sits at the root of the bus, the flash, the power rail or the single output peripheral, is adequate, because those are the resources you cannot split.

The difference is that the remaining tests are about things you can characterise. Worst-case execution time on a single path is measurable and bounded. Interaction between two asynchronous paths through a shared resource is neither.

The honest limit

Not everything can be partitioned. There is one power rail, one flash array, one root of the bus matrix, and often one peripheral both paths must eventually reach. Where you cannot separate in space, the only remaining option is to separate in time, and a time-division argument does depend on measurement, because it depends on durations rather than on addresses. So the construction proof covers part of the problem and hands the rest back to instrumentation.

Partitioning also costs you. Static allocation to the worst case means memory sitting unused for most of the duty cycle, and on a part chosen for a wearable there is not much to spare.

The sharpest limit is that a by-construction argument is only as strong as the assumptions under it, and those assumptions are easy to invalidate silently. A toolchain upgrade that changes default section placement, a linker script edit made to fix an unrelated overflow, or a library that allocates its own buffer in the wrong region. Each of those can quietly return the sharing you removed while every test still passes. So the proof needs a guard: a build-time assertion that each buffer lands in the bank you claimed, failing the build rather than the device. Without that guard you have a diagram and not a property.

FAQ

What actually causes a buffer underrun on a tightly coupled memory architecture? Two real-time paths addressing the same memory bank. The core and each direct-memory-access controller are separate masters on the internal bus, so when both target one bank the arbitration makes one of them wait. The delayed transfer fails to refill the output peripheral's hardware queue before it empties, and the underrun gets reported by the output path rather than by whatever caused it.

Why not just increase the buffer size or the priority? Because both reduce the failure rate without removing the failure. The collision can still occur, so you have moved it below the threshold where your bench reproduces it and into the field, where a fleet multiplied by a duty cycle finds it for you. The slack is also silently spent by the next feature that adds work to the path.

What does partitioning memory and channel ownership mean in practice? Each real-time path gets its own memory bank for its buffers, each buffer has exactly one owning transfer channel, and the hot code and data of the path running on the core stay out of any bank a controller is streaming through. The evidence is a linker script, a memory map and a channel assignment table rather than a test run.

How do I prove a failure class is gone rather than rare? State the mechanism, then show that one of its necessary conditions is absent by construction. Two paths that do not address the same bank cannot arbitrate against each other, and that is readable in the memory map. A long test that saw no symptom proves only that nothing happened during the window.

Does this mean I can skip testing the real-time paths? No. Partitioning protects each path from the other path, not from itself. Worst-case execution time, deadline margin within a single path, and the behaviour of resources you cannot split, such as the flash, the power rail and the shared output peripheral, all still need measurement. The gain is that what remains is characterisable rather than phase dependent.

What makes a by-construction argument go stale? Anything that moves a section without telling you. A toolchain upgrade that changes default placement, a linker script edit made for an unrelated overflow, or a library that allocates its own buffer in the wrong region. The defence is a build-time assertion on placement, so the build fails when the layout stops matching the claim, instead of the device failing later.