L3/07 — Traps and interrupts

Node: this file is the object — the trap/interrupt mechanism (the imported machine-mode machinery, the interrupt sources, the synchronous surface). The proof that it refines the machine-mode ISA is the edge, 12.

Background

An interrupt is the mechanism by which the outside world interrupts a running program: a device raises a wire, and the processor — at a suitable boundary — suspends the program, saves enough state to resume it, and jumps to a handler. RISC-V specifies this machinery in its privileged architecture: on a trap (an interrupt, or a synchronous exception like an illegal instruction), the machine saves the interrupted pc to mepc, records the reason in mcause, stacks the interrupt-enable bit inside mstatus, and jumps to the handler address in mtvec; the handler returns with mret, which unstacks and resumes. Interrupt delivery is governed by two CSRs — mip (which interrupts are pending) and mie (which are enabled) — gated by the global enable bit mstatus.MIE. The core implements exactly this machine-mode machinery, so the specification is imported — the Sail privileged subset, ratified standard — not authored.

The system side is the standard shape as well, which is worth appreciating as a cost that didn't materialise: all three standard interrupt lines are live. The CLINT drives the software-interrupt and timer-interrupt pending bits (msip from its software-interrupt register, mtip from the mtime/mtimecmp compare), and the PLIC drives the external-interrupt bit, funnelling its device sources (the UART) through gateways, priorities, and a claim/complete protocol. Both devices sit behind the memory map, so their register semantics are device models — L5/03's business — while the core-side delivery machinery is entirely the imported spec. What remains authored at the core is only the custom control CSRs (L4/01), and their spec must say they never alter delivery semantics.

The synchronous side is the standard's full surface: illegal instruction, misaligned load/store, access faults (a denied TileLink response does arrive as a precise access-fault trap — the error device makes even unmapped addresses well-behaved, L5/03), breakpoint, and the environment calls. The exact per-cause behaviour is the choice register's to record (L4/02); this chapter's lemmas consume it.

The proof that this machinery refines the machine-mode spec — the six proof obligations, the anchors against spec-side error, and the delivery split — is the edge this mechanism carries, 12.

Effort

Short; the mechanism is imported standard machinery — the Sail privileged subset plus standard interrupt sources. The refinement proof and its cost (mostly standard months, with the S3 residue) are the edge, 12.