Firmware field guide · concurrency and synchronization

Name every actor. Protect the invariant. Prove bounded progress.

Concurrency becomes manageable when every shared object has an owner, every handoff has a publication rule, and every wait has a bound. Use one single-core Cortex-M4 system to compare mutexes, queues, notifications, atomics, priority inheritance, and explicit buffer ownership.

  • Name the owner Separate atomic access, memory ordering, ownership, and lifetime before choosing a synchronization primitive.
  • Publish deliberately Choose an RTOS primitive by meaning, not by habit, and verify how it transfers visibility and ownership.
  • Bound progress Calculate blocking and buffer capacity under worst-case timing, then define recovery for every wait and overload path.

Example system. A fictional 80 MHz single-core Cortex-M4 runs FreeRTOS with three fixed-priority tasks, a 20 ksample/s ADC stream, 128-sample DMA blocks, no data cache, and DMA buffers in coherent SRAM.

Verify on the real target. Priorities, queue depths, atomic lock freedom, port restrictions, and visibility rules are teaching values. Check the compiler, RTOS port, selected target manual, and DMA documentation.

Scope. This guide begins with named task, ISR, DMA, and peripheral actors. NVIC priority, masking, handler design, and DMA-completion service remain in the interrupts and DMA guide. Here the focus is task/task synchronization, C memory ordering, priority inversion, deadlock, and buffer lifetime after handoff.

Interactive ownership scheduler

Follow ownership and visibility on one shared time axis.

Select a case to see which actor can run, who owns the data, where a happens-before edge is required, and whether the system has a bounded path back to progress.

CPU1 core · 80 MHz
ActorsISR + H/M/L + DMA
DMA block128 samples
Period6.4 ms
ISR / DMA
block done
queue handle
return
High task
blocked
ready
take handle
read payload
release slot
sleep
Medium task
preempted
preempted
runs
Low / owner
FREE → DMA
DMA → QUEUED
CONSUMER → FREE
Follow t0–t5 for each actor. Solid highlighted cells own or consume the object; amber cells are blocked; red cells expose a safety or liveness failure. Empty cells mean the actor does not affect this case.
SafetyNo actor observes a mixed revision, reused buffer, or object outside its lifetime.
VisibilityThe publication mechanism creates the required release/acquire relationship.
LivenessEvery wait, critical section, queue, and ownership cycle has a measured bound or recovery.

01Actors

Context · owner · invariant · lifetime

Start with the shared state, not the lock.

A task, ISR, DMA engine, and peripheral can all influence one result even on a single-core MCU. List who can read, who can write, when ownership changes, and what must remain true before choosing any synchronization mechanism.

Execution model

Interleaving is enough to create a race

Two tasks do not need to execute simultaneously. Preemption between a multi-step write and a read can expose a mixed configuration. DMA can operate in parallel with the core, and a peripheral can change status independently.

Draw the legal preemption points and hardware ownership intervals before calling a sequence “atomic.”

Design model

Give each object one publication contract

Name the writer, readers, lifetime, reuse signal, and invalid state. Prefer single-writer or single-owner designs. A queue copy or command message often removes shared writable state entirely.

The invariant belongs in code structure and tests, not only in a comment beside a mutex.

Failure policy

Define overload before it happens

Every bounded queue or buffer pool eventually fills under a long enough consumer blackout. Decide whether to block, drop newest, drop oldest, overwrite with a sequence gap, shed optional work, or enter a fault state.

“Should never happen” is not a backpressure policy.

Interactive lab 1 · interleaving explorer

Can a reader observe half of a configuration update?

Task A changes gain and sample rate. Task B reads both fields to program hardware. Compare an unsafe shared struct with a mutex, queue copy, and single-owner command design.

  1. 1Old config
  2. 2Write gain
  3. 3Reader runs
  4. 4Write rate
  5. 5Commit
Step 1 of 5 · old configuration Published pair is { gain=2, rate=10 kHz }

Both tasks agree on one complete old configuration.

Invariant Hardware must consume gain and rate from the same configuration revision
Current result SAFE SO FAR · no update has begun

Checkpoint · 2 easy, 2 medium, 1 hard

Can you name the owner before the primitive?

Easy What is an invariant?

An invariant is a property that must remain true at every externally visible point, such as “gain and rate belong to the same revision” or “a DMA buffer has exactly one owner.” It tells you what synchronization must protect.

What this tests: reasoning from correctness rather than APIs.

Easy Can a race occur on a single-core processor?

Yes. Preemption can interleave two multi-step operations, and DMA or peripherals can act independently of the core. Simultaneous instruction execution is not required for one actor to observe another actor’s partial state.

What this tests: interleaving versus physical parallelism.

Medium Two tasks read a configuration, but only one task ever writes it. Is synchronization unnecessary?

No. Single writer removes write/write conflict but not read/write publication. Readers still need a complete revision and a lifetime rule. Use a mutex, immutable copy with synchronized pointer/index publication, queue copy, or single-owner command path.

What this tests: single-writer benefits and remaining reader contract.

Medium Why can a pointer queue be less safe than a value-copy queue?

The pointer transfers an address, not necessarily ownership or lifetime. The producer may reuse stack storage or mutate the object while the consumer reads it. A value-copy queue gives the queue its own snapshot; a pointer queue needs explicit immutable lifetime and return/reuse rules.

What this tests: aliasing, lifetime, and ownership transfer.

Hard Design the ownership of a control configuration used by acquisition and telemetry tasks.

Give one control task exclusive mutable ownership. Other tasks send bounded commands to it. After validation, the owner publishes an immutable revision by queue copy or release/acquire index into a stable double buffer. Acquisition applies revisions only at a documented boundary; telemetry reports the committed revision number.

Define queue-full behavior, timeout rollback, object lifetime, and boot defaults. Prove no actor observes a partially validated configuration.

What this tests: complete actor map, ownership transfer, overload, and proof.

02Publication

Atomicity · ordering · visibility · reuse

An atomic flag does not automatically publish its payload.

Atomicity prevents one object access from tearing. Publication additionally requires an ordering relationship so a consumer that observes “ready” also observes the payload writes that happened before it. The payload must remain stable until reuse is acknowledged.

Not synchronization

volatile is not a thread contract

volatile is used for observable accesses such as MMIO and some implementation-defined environments. It does not make a compound operation atomic, remove a C data race, or create release/acquire ordering between tasks.

Atomic object

Choose order for the actual guarantee

Relaxed atomics provide atomic modification order for the atomic object but no payload ordering. A release store can publish prior writes to an acquire load that reads from the matching release sequence.

Do not assume an atomic type is lock-free. Verify atomic_is_lock_free, compiler documentation, and the target port where latency or ISR legality depends on it.

Lifetime

Publication needs a reuse protocol

Even correct release/acquire code fails if the producer overwrites the payload while the consumer still uses it. Add acknowledgment, generation counters, immutable allocation, double buffering, or a queue whose ownership rules cover reuse.

Interactive lab 2 · publication litmus

When does “ready” make the payload visible?

Compare plain, volatile, relaxed atomic, and release/acquire flag code. The readout states only the guarantee provided by the C abstract machine.

/* Producer */
payload.value = 42;
atomic_store_explicit(&ready, true, memory_order_release);

/* Consumer */
if (atomic_load_explicit(&ready, memory_order_acquire)) {
    use(payload.value);
}
Language guarantee If the acquire reads the released value, the prior payload write happens before the consumer reads it

This publishes one stable payload revision. It does not by itself prevent the producer from reusing the payload too early.

Allowed conclusion ORDERED PUBLICATION · add an explicit acknowledgment or immutable lifetime before reuse
Target check Verify the chosen atomic type is implemented with acceptable bounded behavior on the compiler and Cortex-M4 target

Explore the mechanism

Publishing and returning are two different edges.

Inspect one stable payload revision while the consumer owns it, then compare an early overwrite with an acknowledged return.

  1. 01 · OwnerConsumer holds revision 7
  2. 02 · Publication edgeAcquire reads the release-published ready value
  3. 03 · Payload accessRead the stable value: 42
  4. 04 · Return / reuse gateWAIT · no return acknowledgment
Visibility is established; reuse is still closed.

The matching release/acquire publishes the earlier write. The producer must leave this ordinary payload unchanged while the consumer reads it.

Check nextCheck both edges: publication before read, then a synchronized return acknowledgment before the next write.

Single producer, single consumer, ordinary payload in the guide’s no-cache SRAM model. The acquire must read from the release publication. Compare the publication code above.

Checkpoint · 2 easy, 2 medium, 1 hard

Can you distinguish atomic access from publication?

Easy What does atomicity guarantee for one object?

An atomic access participates in the atomic object’s modification order and is not observed as a torn mixture of two writes. It does not automatically group adjacent objects into one transaction or publish unrelated payload writes.

What this tests: scope of an atomic operation.

Easy Does a volatile ready flag publish an ordinary payload?

No. volatile makes specified accesses observable to the C implementation, but it does not create an inter-thread happens-before relationship for the payload. Use a publication design whose release/acquire operation covers a stable payload, or transfer ownership through an RTOS primitive with a documented memory contract.

What this tests: volatile limits and payload publication.

Medium When does a release store synchronize with an acquire load?

When the acquire load observes the value written by the release store or an applicable release sequence. Then writes sequenced before the release happen before reads sequenced after the acquire. Merely using acquire somewhere does not synchronize unrelated values.

What this tests: the reads-from relationship, not keyword matching.

Medium When is memory_order_relaxed useful?

It is useful when you need atomicity and per-object modification order but no cross-object publication, such as an independent diagnostic count. It is not sufficient for a ready flag that must make ordinary payload writes visible.

What this tests: matching memory order to the invariant.

Hard Publish a multi-field snapshot without holding a mutex while readers process it.

Use two stable buffers. The single writer fills the inactive buffer, validates it, then release-stores its index or generation. A reader acquire-loads the index and uses only that immutable revision. Add a reader acknowledgment, reference count, epoch, or bounded copy so the writer cannot reuse the buffer while a reader still holds it.

If multiple writers exist, serialize them first. Verify atomic lock freedom only if the design’s latency depends on it, and add DMA/cache maintenance if the selected target requires it.

What this tests: coherent publication plus lifetime and reuse.

03Primitives

Ownership · signaling · transfer · exclusion

Choose the primitive whose meaning matches the contract.

Mutexes express task-owned exclusion. Semaphores and notifications signal availability. Queues transfer bounded messages. Event bits summarize conditions. Critical sections suppress scheduling or interrupts for a tightly bounded operation. Similar APIs do not make these mechanisms interchangeable.

Owned exclusion

Mutex

The task that takes a mutex owns it and must release it. FreeRTOS mutexes add priority inheritance, making them appropriate for short task/task resource protection. They are not an ISR signaling primitive.

Signal or count

Semaphore or notification

A binary semaphore represents an event; a counting semaphore represents available units or accumulated events. A direct task notification is compact and fast when the signal has one receiving task and its value semantics fit.

Transfer

Queue

A queue copies fixed-size messages into bounded storage and makes overload visible. It is often the cleanest way to move a command or immutable snapshot to a single owner.

Decision matrix · FreeRTOS semantics

Ask what crosses the boundary.

Port APIs and ISR-safe variants are target-specific. The table captures intent, not a substitute for the official API contract.

NeedDefault choiceOwnership ruleBlocking ruleCommon mistake
Protect task-owned bus transactionMutexTaker releasesBound wait and hold timeGiving from a different task or ISR
Wake one worker for an eventTask notification or binary semaphoreNo resource ownershipReceiver may blockTreating repeated events as an unbounded count
Track N identical resourcesCounting semaphoreCount represents available unitsTake blocks only by policyCount drifting from real resources
Transfer a command snapshotQueue by valueQueue owns copied bytesDefine full/empty timeoutsBlocking forever while holding another lock
Wait for several level conditionsEvent groupBits represent documented conditionsDefine clear-on-exit behaviorUsing one bit as a lossless event counter
Protect a few instructions from preemptionCritical sectionCurrent context owns a bounded regionNever block insideWrapping slow I/O or unknown library code

Explore the mechanism

What crosses a queue: the record or its address?

Compare the same two-field configuration transferred by value and by pointer.

  1. 01 · Producer storageOriginal record: { gain: 2, rate: 10 kHz }
  2. 02 · Send → queue storageCopies the complete fixed-size record
  3. 03 · Receive → consumerReceives its own copied record
The queue transfers bytes with their own storage.

For this record of scalar fields, later changes to the producer’s original do not change the queued copy. The send and receive still need a full/empty policy.

Check nextThe item size covers the whole record. A copied struct containing pointers would still need a pointee-lifetime contract.

This is a task-to-task message comparison. Item size, lifetime, timeout and full-queue behavior remain part of the design. Use the primitive decision matrix.

Checkpoint · 2 easy, 2 medium, 1 hard

Can you select by semantics?

Easy What key property distinguishes a mutex from a binary semaphore?

A mutex has ownership: the task that locks it must unlock it, and the RTOS can associate priority inheritance with that owner. A binary semaphore represents a signal and may be given by a different permitted context.

What this tests: exclusion ownership versus signaling.

Easy When is a queue preferable to a shared global plus a notification?

When the consumer needs a stable command or snapshot and bounded backlog matters. A value-copy queue combines transfer, lifetime, ordering, and full/empty policy instead of leaving those contracts around a mutable global.

What this tests: message transfer and explicit capacity.

Medium Can an event bit count five identical arrivals?

No. A bit represents a level such as “work exists”; setting it repeatedly while already set does not preserve multiplicity. Use a counting semaphore, queue entries, notification count, or explicit bounded counter when every arrival matters.

What this tests: level state versus event count.

Medium Why is blocking on a queue while holding an unrelated mutex dangerous?

The task can retain the mutex for the entire queue wait, inflating blocking and possibly forming a wait-for cycle if the queue consumer needs that mutex. Release unrelated ownership before a blocking call or redesign the transaction.

What this tests: compositional blocking and deadlock risk.

Hard Select primitives for a UART command service with many clients and one hardware owner.

Give one service task exclusive hardware ownership. Clients send bounded command records through a queue and include a completion token or response queue when needed. The service serializes transactions and signals completion without clients taking a hardware mutex. Define queue-full, client timeout, cancellation, and late-response disposal.

The ISR-to-service wakeup remains in the interrupts guide; task/task command ownership belongs here. Avoid holding client locks while waiting for a response.

What this tests: single-owner architecture, bounded messaging, and cross-guide boundaries.

04Blocking

H · M · L · critical section · inheritance

A high-priority task can wait behind medium-priority work.

Priority inversion begins when a low-priority task owns a resource needed by a high-priority task. An unrelated medium-priority task can then delay the owner. Priority inheritance reduces this specific interference, but it does not make long critical sections, nested locks, or deadlock safe.

Blocking term

Bound the owner’s remaining work

When H requests the mutex, its direct blocking depends on the lower-priority owner’s remaining critical section plus protocol and scheduling effects. Average hold time is not the deadline argument.

Protocol

Inheritance boosts the owner temporarily

When H blocks, L inherits H’s priority so M cannot preempt L. Once L releases the relevant mutex, the RTOS restores priority according to its implementation rules.

Study the actual FreeRTOS version and nested-mutex limitations.

Limit

Inheritance does not solve cycles

If tasks acquire A then B and B then A, no priority boost can create progress. Enforce one global lock order, avoid blocking calls while holding unrelated locks, and design rollback for timeouts.

Interactive lab 3 · priority inversion simulator

Follow L, H, and M on one exact timeline.

L enters a 3 ms mutex-protected section at t=0. H wakes and blocks at 1 ms. M wakes at 1.2 ms with 8 ms of work. Assume zero scheduler overhead and no other releases.

  1. t=0L locks
  2. t=1.0H blocks
  3. t=1.2M wakes
  4. releaseL unlocks
  5. nextH runs
Step 1 of 5 · t=0 L starts its 3 ms critical section at base priority L

No higher-priority task is runnable yet.

High-task blocking Not started; H has not requested the mutex
Protocol conclusion Without inheritance, later medium work can delay the low-priority owner

Checkpoint · 2 easy, 2 medium, 1 hard

Can you calculate blocking instead of naming the pattern?

Easy What is priority inversion?

A higher-priority task is prevented from progressing because a lower-priority task owns a required resource. Unrelated intermediate-priority work can extend the delay if the owner is preempted.

What this tests: resource-induced blocking versus ordinary scheduling.

Easy What does priority inheritance change?

It temporarily raises the priority of the resource owner when a higher-priority task blocks on its mutex. This lets the owner finish and release without interference from tasks below the inherited priority.

What this tests: owner boosting, not waiter boosting.

Medium In the lab, how long does H wait without inheritance?

H blocks at 1 ms. L executes until 1.2 ms, leaving 1.8 ms of its section. M then runs for 8 ms until 9.2 ms; L finishes at 11.0 ms. H waits 11.0 - 1.0 = 10.0 ms under the stated zero-overhead assumptions.

What this tests: an exact preemptive timeline.

Medium How long does H wait with inheritance in the same lab?

At 1 ms, L inherits H’s priority and continues. M cannot preempt at 1.2 ms. L completes its 3 ms section at t=3 ms, so H waits 3 - 1 = 2 ms, excluding stated-zero protocol overhead.

What this tests: the bound inheritance improves and the work it cannot remove.

Hard A task holds two mutexes while calling a slow driver. Why is “FreeRTOS has inheritance” not a schedulability proof?

The driver duration may be unbounded, and nested mutex behavior can delay priority disinheritance depending on the kernel version. Other tasks may form lock-order cycles. Measure worst-case hold time, split slow I/O from protected state, establish a global lock order, and analyze each blocking chain against deadlines.

Use the official FreeRTOS implementation contract for the exact version. Inheritance reduces one class of interference; it does not replace whole-system blocking analysis.

What this tests: protocol limits, nesting, and schedulability evidence.

05Buffers

Ownership state · capacity · backpressure · reuse

A completed buffer is not automatically free.

After hardware completes a transfer, software must publish a stable buffer, process it, and explicitly return it before reuse. Capacity converts a maximum consumer blackout into a concrete number of simultaneously owned buffers.

Lifecycle

Make ownership a checked state machine

Use FREE → DMA_OWNED → READY → PROCESSING → FREE. Only the owner may mutate payload or metadata. Illegal transitions indicate double return, overwrite, or stale handles.

Capacity

Budget blackout, not average throughput

ControlNode completes 128 samples at 20 ksample/s every 128 / 20,000 = 6.4 ms. With no backlog at blackout start, total buffers needed are one active DMA buffer plus the number that can complete while the consumer is unavailable.

Policy

State what happens when full

A control loop might stop acquisition and fault; telemetry might drop oldest with a sequence gap; a logger might shed lower-value records. The decision depends on product semantics, not the queue API.

Interactive lab 4 · buffer ownership and capacity

Will this pool survive the consumer blackout?

Choose the worst-case processing blackout and total buffer count. The lab calculates completed capacity and identifies overwrite or margin.

Consumer blackout

Total pool size

FREE DMA_OWNED READY PROCESSING FREE
Capacity calculation ceil(18 / 6.4) = 3 completed buffers; plus 1 active DMA buffer = 4 total
Pool verdict PASS WITH NO MARGIN · 4 available, 4 required

The pool survives exactly the assumed blackout. Add margin for scheduling jitter, handoff overhead, and a blackout that begins just before completion.

Overflow policy If no FREE buffer exists, stop acquisition and record a capacity fault; never overwrite DMA_OWNED or PROCESSING storage

Lab assumption: the blackout begins with no READY backlog, each block completes exactly every 6.4 ms, and one buffer is always active in DMA. A conservative product analysis must include phase, jitter, handoff time, and cache/coherency rules.

Cross-guide boundary: how the DMA-complete event is configured, acknowledged, prioritized, and handed out of interrupt context belongs to the interrupts guide. This chapter begins once ownership of a completed buffer is being published to software.

Checkpoint · 2 easy, 2 medium, 1 hard

Can you prove ownership and capacity?

Easy Who may write a DMA_OWNED buffer?

Only the DMA engine according to the programmed transfer contract. Software may inspect control state required by the driver but must not reuse or mutate the payload until completion and visibility requirements transfer ownership.

What this tests: exclusive ownership during hardware production.

Easy Why include a generation number in a buffer handle?

It distinguishes the current ownership cycle from a stale reference to the same physical slot. Returning a handle with an old generation can be rejected instead of freeing a buffer that has already been reassigned.

What this tests: stale references and ABA-like reuse.

Medium How many total buffers does an 18 ms blackout require in this lab?

Each block takes 6.4 ms. ceil(18 / 6.4) = 3 buffers can complete while the consumer is unavailable. Add one active DMA buffer, giving four total before margin under the stated phase assumption.

What this tests: rates, ceiling, and simultaneous ownership.

Medium Is four buffers a robust production choice for that 18 ms blackout?

It is only the exact lab minimum. Scheduling jitter, completion-to-queue delay, blackout phase, processing release time, and measurement uncertainty can consume it. Add justified margin or tighten the blackout bound and prove it.

What this tests: mathematical minimum versus engineered capacity.

Hard Define a loss policy for acquisition data that controls a safety function and also feeds optional telemetry.

Separate the safety consumer from optional telemetry ownership. Reserve capacity or priority for the safety path, and never let telemetry retain the only processing buffer. If the safety path cannot obtain a complete sequence within its bound, stop or degrade the controlled function and record a fault. Telemetry may drop oldest or decimate with explicit sequence gaps.

Measure high-water marks, blackout duration, drops, and illegal transitions. Do not overwrite a buffer still owned by DMA or safety processing.

What this tests: product semantics, partitioned capacity, and observable overload.

06Liveness

Lock order · wait graph · timeout rollback · proof

Correct data is not enough if the system cannot progress.

Safety properties say bad states never occur. Liveness says required work eventually completes. A complete firmware design proves bounded queues, finite critical sections, acyclic lock acquisition, timeout rollback, and recovery when a dependency stops responding.

Deadlock

Make the wait-for graph acyclic

Enforce one global lock order, such as configuration before storage before transport. Detect violations in review and debug builds. Prefer message ownership when two subsystems would otherwise call each other while locked.

Timeout

Rollback every partial acquisition

A timeout is not complete until the task releases already-held resources, cancels or marks late work, restores state, and returns an unambiguous error. Otherwise retries leak tokens or corrupt ownership.

Proof

Measure the longest path

Instrument queue high-water marks, mutex hold times, blocking time, missed deadlines, buffer generations, timeout reasons, and recovery count. Verify worst-case combinations, not only one primitive in isolation.

Explore the mechanism

Draw the wait edges before changing priorities.

Compare opposite acquisition orders with a shared A-before-B order.

Task 1Holds A

Waits for B, held by Task 2

Task 2Holds B

Waits for A, held by Task 1

Task 1 waits for Task 2; Task 2 waits for Task 1.

Both tasks wait for an owner that cannot run past its wait.

This fixture assumes blocking acquisition, neither task releases its held lock while waiting, and no recovery action intervenes. The two edges form a cycle.

Check nextRecord held and requested locks together. Priority inheritance cannot release either resource.

Two tasks and two exclusive locks; no other dependencies are modeled. The wait edges describe “waits for,” not execution order. Revisit the limits of priority inheritance.

Synthesis capstone · complete runtime contract

ControlNode concurrency proof sheet

Every row identifies the state owner, transfer primitive, capacity or blocking bound, overload action, and evidence. Replace lab values with measured product limits.

FlowOwnerTransferBoundFailure actionProof
Configuration commandsControl taskQueue by value8 commandsReject newest with explicit busy responseQueue high-water and revision trace
Published configurationImmutable revisionRelease/acquire index2 buffersDelay reuse until acknowledgmentGeneration and reader-ack assertions
ADC blocksDMA → acquisition taskOwnership state plus queue5 buffersStop acquisition on no FREE bufferIllegal-transition and high-water counters
Shared storage serviceStorage taskRequest/response queues25 ms request deadlineCancel token and discard late responseEnd-to-end latency histogram
Short I²C register sequenceCalling task with mutexOwned exclusion350 µs holdRelease, reset bus owner state, report timeoutMaximum hold and waiter-block time
Fault notificationSafety taskDedicated notificationOne pending level plus cause recordEnter safe state on missed service boundCause sequence and response timestamp
Global lock order Configuration → storage metadata → transport; no reverse acquisition is permitted
Blocking rule No task blocks on a queue, notification, or slow peripheral while holding an unrelated mutex
Whole-system invariant Each resource has one owner, every transfer has bounded storage and lifetime, and each timeout either completes or rolls state back

Checkpoint · 2 easy, 2 medium, 1 hard

Can you prove the runtime eventually moves?

Easy What is deadlock?

Deadlock is a state in which actors wait on a cycle of resources or conditions that none can satisfy. With mutual exclusion, hold-and-wait, no forced release, and circular wait, progress stops even if CPU time remains available.

What this tests: liveness failure versus CPU overload.

Easy How does a global lock order prevent a common deadlock?

If every task acquires locks only in one increasing order, a circular wait among those locks cannot form. The order must include every acquisition path, callbacks, error paths, and helper functions.

What this tests: a structural deadlock-prevention argument.

Medium A queue send times out after a task has reserved a buffer. What must happen?

The task must return or otherwise resolve the reserved buffer exactly once, update generation/state consistently, and report that the message was not transferred. A retry cannot reuse the same ownership token ambiguously.

What this tests: timeout rollback and resource conservation.

Medium Why is a timeout alone not proof of liveness?

A timeout bounds one wait, but the caller may immediately retry forever, leak a resource, or leave the callee processing a request whose response becomes stale. Prove the complete state transition after timeout, including cancellation, cleanup, retry budget, and recovery.

What this tests: local bounds versus system progress.

Hard Review the capstone for a failure where storage stalls, telemetry backs up, and acquisition continues.

Storage requests must time out with cancellation and no held unrelated mutex. Telemetry must apply its bounded drop or shedding policy instead of retaining acquisition buffers. Acquisition capacity remains reserved for the safety path; if its no-FREE bound is reached, it stops or faults according to policy. The control task remains responsive because it owns configuration through a separate bounded queue.

Test the combined fault with instrumentation for queue high-water, ownership transitions, hold times, late responses, drops, and final recovery. The system passes only if no buffer is overwritten, the safety bound holds, and normal service resumes or enters a defined degraded state.

What this tests: interacting bounds, partitioned ownership, and recovery proof.

Primary references

Verify the language, architecture, RTOS, compiler, and target together.

  1. WG14 N1570, C11 Committee Draft, especially the multithreaded execution and <stdatomic.h> clauses.
  2. WG14 N1479, Memory Model Rationale for release/acquire publication examples and memory-order intent.
  3. Armv7-M Architecture Reference Manual for exclusive accesses, memory attributes, and barrier architecture.
  4. CMSIS-Core CPU intrinsics for the selected Cortex-M barrier and exclusive-access interfaces.
  5. Official FreeRTOS mutex and priority-inheritance documentation plus the exact kernel version’s semaphore, queue, notification, event-group, scheduling, and Cortex-M port API references.
  6. The selected compiler’s atomic implementation documentation, link map, and generated code when bounded or lock-free behavior matters.
  7. The selected SoC and DMA reference manual for buffer ownership, bus visibility, cache maintenance where present, and peripheral-specific constraints.