Interrupt-driven pulse sequencer 2026-10-25
View more
A pulse sequencer can separate event capture from output timing. A short interrupt handler acknowledges the event latch and increments a pending count. An independent finite-state machine consumes one count on entering ON, changes to GAP after the pulse width, and enters IDLE only after the mandatory off interval. Even an empty queue must not bypass GAP: an arrival immediately after light-off would otherwise start too soon.
The pending count equals recorded events minus started pulses. A critical section protects its read-modify-write operations; declaring shared state as in volatile-qualified objects in C does not alone make each update an atomic operation. Separate sequencers for different channels allow simultaneous pulses while one hardware timer schedules their earliest deadline. Finite queue capacity, detector rearming and dispatch resolution remain explicit assumptions.
Read the full article
Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof / 2 / a / Solution 2026-10-25
View more
A short interrupt handler should acknowledge the detector and count work; a timed finite-state machine should generate the flashes. A Boolean “someone arrived” variable cannot preserve several queued detections. This is an interrupt-driven pulse sequencer. Initialise the light off, the pending-event counter to zero and the sequencer to IDLE before enabling interrupts.
In the following pseudocode, interrupt acknowledgement uses the source-specified operation of writing zero. The atomic operation and timer calls name abstract services, not undocumented device registers of a particular microcontroller.
eye_handler():
    if EYE_DETECTED != 0:
        EYE_DETECTED = 0
        pending = pending + 1

try_take_event():
    briefly mask the detector interrupt
    if pending == 0: taken = false
    else: pending = pending - 1; taken = true
    restore the previous interrupt mask
    return taken

service(now):
    if state == ON and elapsed(now, started) >= one_second:
        LIGHT = 0
        state = GAP
        started = now
    if state == GAP and elapsed(now, started) >= one_second:
        state = IDLE
    if state == IDLE and try_take_event():
        LIGHT = 1
        state = ON
        started = now
The main program repeatedly handles a new event or the next timer deadline and calls service. The ON state lasts one second; every completed flash enters GAP, even if the queue is empty at that instant. An arrival during that gap must wait for it to expire. Otherwise turning the light off and immediately treating the device as idle could allow a new flash too soon. Once a gap has expired, a queued event starts a new flash; if no work is pending the device remains idle. Removing a pending event only when a flash starts gives one completed flash per consumed event.
An interrupt can arrive during the main program's decrement. Without a critical section, its increment can be overwritten by a race condition. Merely declaring the counter volatile, as in volatile-qualified objects in C, does not make the decrement an atomic operation. Short interrupt masking, or an appropriate atomic operation, protects it; interrupts must remain enabled during the one-second intervals so that detections continue to be recorded.
A calibrated busy-wait loop is simple, but occupies the CPU and its duration depends on instruction timing, compiler transformations and time spent in interrupts. Polling a hardware timer avoids calibration dependence but still consumes CPU while polling. A timer interrupt or timer comparison deadline permits useful work or safe sleeping between transitions and is preferable for precise timing. If sleeping, the test for queued work and entry into sleep must avoid a lost wake-up. By the modulo-counter elapsed-time identity, a wrapping digital counter is usable if elapsed-time subtraction is unsigned and the real observation interval is less than its modulus; a wide enough counter or suitable bounded intervals make this explicit. Software dispatch adds bounded latency, so the specification is achieved to timer/interrupt-service resolution; stricter physical pulse-width requirements call for hardware output comparison or a suitably prioritised timer handler.
Finally, the device register is only a single-bit event latch. Two physical detections before acknowledgement may coalesce, so no software can recover their multiplicity from that bit alone. The event counter must also have enough capacity for the allowed backlog; indefinitely many arrivals faster than one flash every two seconds cannot be guaranteed with finite storage. These are explicit hardware/rate assumptions, not missing input files. Keeping the handler short minimises the rearming interval but cannot abolish those limitations.
Read the full article
Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Digital systems, linear algebra, introduction to formal proof resit / 2 / a / Solution 2026-10-25
View more
Give the hardware to a single device driver process. Other processes request a conversion through message passing and never touch its memory-mapped input-output registers. The following is protocol pseudocode for Phōs: its operation names specify their required semantics, rather than asserting an unverified spelling of a particular 2019 C interface. The hardware actions and the request/reply design are fully specified.
Use a FIFO queue of accepted requests, each containing its sender and a per-call token. Bind the device's interrupt to a persistent notification addressed to the driver before any conversion is started. A notification must remain pending if it arrives before the driver next waits; this is the lost-wakeup avoidance requirement. The driver receives both client requests and interrupt notifications in its event loop.
configure sensor and connect its interrupt notification to this process
TEMP_DATARDY := 0
clear stale pending interrupt notification
enable sensor interrupt and interrupt-controller delivery
pending := empty FIFO
active := none

forever:
    if active is none and pending is not empty:
        active := remove oldest request from pending
        TEMP_DATARDY := 0
        clear stale pending interrupt notification
        TEMP_START := 1

    event := wait for a request or persistent interrupt notification

    if event is REQUEST(sender, token):
        append (sender, token) to pending

    if event is sensor interrupt and active is not none:
        if TEMP_DATARDY != 0:
            value := TEMP_TEMP
            TEMP_DATARDY := 0
            acknowledge the interrupt through the OS interrupt mechanism
            send RESULT(active.token, value) to active.sender
            active := none
After receiving an idle-time request, the next loop iteration starts its conversion before waiting again. While a conversion is in progress, additional requests join the queue without starting another conversion. A completed reading is copied before its ready flag is cleared, and the next request cannot start until the current result has been delivered. Spurious or stale notifications do not complete a request unless the device's ready register confirms completion.
Clearing old status and notification precedes TEMP_START; doing so afterwards could erase a very fast completion. The operating system interrupt binding and persistent notification cover completion in the interval between starting the device and entering the wait. Register accesses must use the platform's device-access semantics, including required volatile-qualified objects in C or ordering primitives. Exact initialization and interrupt-connection call names remain an implementation binding, not invented Phōs API calls. The later teaching site's named system is documented separately; it is not used as proof of an identical historical API.[ref]
Read the full article
Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 2 / b / Solution 2026-10-25
View more
The interrupt handler is the only writer of interval_ms, valid and next_slot. The foreground function takes an interrupt-safe ring-buffer snapshot inside a short critical section, copying the count and exactly that many valid entries before restoring the previous mask. It performs the comparatively expensive summation and division after interrupts are restored. A new pulse then affects the next query, while the current query consistently describes the earlier snapshot.
Without exclusion, the foreground could read an old entry, be interrupted while the buffer is updated, then read new entries or an inconsistent count. Even indivisible 32-bit loads would not make that multi-element snapshot atomic. The volatile-qualified objects in C ensure that the compiler performs required shared or device accesses; volatile does not provide mutual exclusion or a coherent multiword snapshot.[ref]
This design assumes a single-core foreground/interrupt execution model: no other interrupt, DMA engine or core modifies the protected buffer. The mask hooks must prevent compiler reordering across their boundaries and really mask the GPIO interrupt. Restoring the saved mask also makes the function safe to call when interrupts were already disabled. Keep the critical section short enough that the event register does not coalesce multiple heartbeats while interrupts are masked; otherwise the hardware interface cannot reconstruct events it never recorded.
Read the full article
Volatile-qualified objects in C 2026-10-24
View more
Volatile-qualified objects in C are objects whose accesses must follow the implementation's observable-access rules even when the optimizer cannot see an ordinary program dependency. They are commonly used for device registers and state changed by an interrupt handler, under the target compiler's embedded execution model. volatile does not by itself provide atomic multiword access, mutual exclusion or inter-thread synchronization. Protecting a shared snapshot still requires a suitable critical section or another synchronization protocol.[ref]
Read the full article