Q076FreeFirmware
Verify a DMA flood-fill transaction
Question
Write the oracle and transaction checks for firmware driving a direct memory access (DMA) engine that recolors the seed's four-connected region in bounded static RAM (SRAM). Implement the complete C oracle, checker and wrapper with the supplied platform hooks. The address is a byte-addressed bus address, not a host pointer: base zero is valid, alignment is four bytes, and mapped SRAM covers the complete validated image. One exclusive owner holds its cache-line-rounded storage so maintenance cannot affect unrelated dirty bytes. Flush completes the CPU-to-device ownership transfer before START; invalidate restores CPU visibility only after DMA is quiescent. prepare_if_current atomically validates reset generation, clears stale completion and programs the descriptor; start_if_current accepts only in that generation. Reset cancels the old producer and changes the 64-bit generation, which cannot wrap during a call. Abort is idempotent and returns only after old accesses/status are quiescent. The completion lock validates generation and excludes reset until unlock. Error has priority over DONE; an observed successful DONE takes priority over a timeout first noticed in that poll. Timer subtraction is modulo 2^32 and each call lasts less than one full wrap. On failure the image may contain successful partial writes; abort before invalidating so CPU ownership is still returned safely. The DV checker is initialized with checker_cancel. Call checker_begin at accepted START with a private immutable image snapshot and the two guard values. Every byte access is observed in order; a failed access changes no byte, and all later accesses before termination are forbidden. Successful writes update the observed image, and reads must match it. checker_complete receives the complete final image and guards; successful completion must match the flood-fill oracle, while hardware error must match the observed partial image. Abort/reset/timeout calls checker_cancel; subsequent accesses/completions without a new owner are rejected. Another job starts only after the canceled engine is quiescent. Checker objects and all host snapshots are live, correctly sized and mutually disjoint. Successful DONE means all DMA accesses for that job have completed and no further accesses remain, so invalidation under the completion lock is safe without abort.
Implementation scaffold
#include <stdbool.h>
#include <stddef.h>
#include <stdint.h>
#include <limits.h>
typedef enum { FILL_OK, FILL_BAD_ARG, FILL_HW_ERROR,
FILL_TIMEOUT } fill_status_t;
enum { FILL_BUSY = 1u << 0, FILL_DONE = 1u << 1, FILL_ERR = 1u << 2 };
extern uint32_t fill_status(void);
extern uint64_t fill_reset_generation(void);
extern bool fill_prepare_if_current(uint64_t generation, uint32_t base,
uint8_t w, uint8_t h, uint8_t x,
uint8_t y, uint8_t color);
extern bool fill_start_if_current(uint64_t generation);
extern bool fill_lock_completion(uint64_t generation);
extern void fill_unlock_completion(void);
extern void fill_abort(void);
extern void fill_flush_for_device(uint32_t base, size_t bytes);
extern void fill_invalidate_for_cpu(uint32_t base, size_t bytes);
extern uint32_t platform_ticks(void);
#include <string.h>
typedef struct {
bool active, faulted;
uint32_t base;
uint16_t pixels;
uint8_t expected[256], observed[256];
uint8_t guard_before, guard_after;
} fill_checker_t;
// Supplied reset/abort hook: discard all transaction ownership.
void fill_checker_cancel(fill_checker_t *checker) {
*checker = (fill_checker_t){0};
}
bool fill_descriptor_valid(uint32_t base, uint8_t w, uint8_t h,
uint8_t x, uint8_t y) {
// TODO: validate alignment, dimensions, seed and final byte address.
}
// Called only with valid dimensions/seed and a private writable 256-byte buffer.
void flood_fill_reference(uint8_t image[256], uint8_t width, uint8_t height,
uint8_t seed_x, uint8_t seed_y, uint8_t replacement) {
// TODO: recolor the bounded four-connected region without recursion.
}
bool fill_checker_begin(fill_checker_t *checker, uint32_t base,
uint8_t w, uint8_t h, uint8_t x, uint8_t y,
uint8_t replacement, const uint8_t image[256],
uint8_t guard_before, uint8_t guard_after) {
// TODO: snapshot one accepted image and retain its complete prediction.
}
bool fill_checker_access(fill_checker_t *checker, bool write,
uint32_t address, uint8_t data, bool fault) {
// TODO: enforce ownership/bounds/stop-after-fault and mirror successful accesses.
}
bool fill_checker_complete(fill_checker_t *checker, bool hw_error,
const uint8_t image[256],
uint8_t guard_before, uint8_t guard_after) {
// TODO: compare observed/final memory and guards, then retire ownership.
}
fill_status_t flood_fill(uint32_t base, uint8_t w, uint8_t h,
uint8_t x, uint8_t y, uint8_t color, uint32_t timeout) {
// TODO: validate, transfer cache ownership, start, poll and quiesce on failure.
}
Trace one case
3x3 image=[[1,1,0],[1,0,0],[0,1,1]], seed=(0,0), new_color=7[[7,7,0],[7,0,0],[0,1,1]]Only the three four-connected old-color pixels touching the seed are recolored; the separate bottom-right region remains unchanged.
Requirements
- Validate four-byte base alignment, dimensions 1 through 16, seed coordinates, and final-address arithmetic before MMIO.
- Snapshot the image at accepted START and recolor only pixels connected to the seed through up, down, left, or right moves.
- Treat equal old and new colors as a successful no-op and keep every bus access within the image.
- Stop on the first fault, distinguish hardware error and timeout, and forbid late status or writes after abort or reset.