core/timers.rad core/notifications.rad core/devices.rad core/interrupts.rad core/mmio.rad

CORE_ASM := arch/atomic.ras arch/context.ras arch/clock.ras arch/mmio.ras

	check/budgets.rad check/budget_caps.rad check/timers.rad check/notifications.rad check/devices.rad

interrupt.rv64: interrupt.rad check/interrupt.ras arch/entry.ras core.rad $(MODULES) $(CORE_ASM) $(COMPILER)

	$(COMPILE) $(CORE) -pkg interrupt -start arch/entry.ras -mod interrupt.rad -mod check/interrupt.ras -entry interrupt -o $@

check: all check.rv64 context.rv64 interrupt.rv64

	$(EMU) -machine -harts=2 -no-guard-stack -irq=3 -irq-at=4000000 -uart-rx=52 -uart-rx-at=8000000 -max-steps=100000000 -count-instructions -run interrupt.rv64

	rm -f kernel.rv64 check.rv64 context.rv64 interrupt.rv64

record the contracts established through step 14 of the 22-step plan.

## Devices and external interrupts

- Device access validates live authority, rights, complete byte range, overflow,

  and physical alignment. Its admitted address is consumed by one MMIO operation;

  it cannot become a user pointer.

- One FDT-selected PLIC machine context services external interrupts; other

  contexts remain masked. Access only implemented source words and fence memory

  and device I/O.

- A claimed source stays masked and active until notification consumption. The

  driver drains the device first. Completion briefly enables the route because

  the PLIC may require its enable bit. Claims survive queue backpressure and

  exclusive receiver transfer.

- Missing, dead, or stale receiver authority leaves the source masked. Invalid

  consumer progress cannot release a claim or rearm a source. The two-hart

  IRQ/UART check exercises the primary PLIC route, not multicore dispatch.

Run the two-hart IRQ/UART scenario with IRQ 3 at tick 4,000,000 and UART byte R at tick 8,000,000. Check retained-claim transfer through a full queue, one delivery, draining, dropped authority, and the next timer wake.

// Full I/O and memory fences surround each native 32-bit controller access.

.text;

.export @"core::mmio::read32";

@"core::mmio::read32"

	fence;

	lwu    %a0    0(%a0);

	fence;

	ret;

.export @"core::mmio::write32";

@"core::mmio::write32"

	fence;

	sw     %a1    0(%a0);

	fence;

	ret;

mod devices;

    devices::run();

//! Device materialization authority and byte-range boundary checks; no hardware I/O.

use core::abi;

use core::capabilities;

use core::contexts;

use core::devices;

use core::domains;

use core::fdt;

use core::frames;

use core::handles;

use core::memory;

use core::platform;

use core::resources;

use core::state;

/// One caller and its device authority.

static DOMAINS: [domains::Domain; 1] = undefined;

/// Device windows, including deliberately invalid physical bounds.

static OBJECTS: [resources::Slot; 4] = undefined;

/// Context storage required by shared kernel state.

static CONTEXTS: [contexts::Context; 1] = undefined;

/// Empty RAM pool; materialization must not access physical device bytes.

static POOL: frames::Pool = undefined;

/// Unused frame metadata backing.

static PINS: [u16; 1] = undefined;

/// Unused Page claim backing.

static ASSIGNED: [bool; 1] = undefined;

/// Domain grant backing.

static GRANTS: [u64; 1] = undefined;

/// Shared state for the checked materialization entry point.

static KERNEL: state::State = undefined;

/// Install a real device resource and read-only capability without touching MMIO.

fn device(base: u64, size: u64) -> abi::Handle {

    let object = try! resources::create(&mut OBJECTS[..], resources::Value::Device(fdt::Range { base, size }));

    resources::retain(&mut OBJECTS[..], object);

    let slot = try! handles::vacant(&DOMAINS[0].handles);

    return handles::install(&mut DOMAINS[0].handles, slot, object, abi::READ);

}

/// Observe the public error result rather than private validation steps.

fn error(handle: abi::Handle, offset: u64, width: u64, rights: u16) -> abi::Error {

    let _address = try devices::access(&KERNEL, 0, handle, offset, width, rights) catch result {

        return result;

    };

    return abi::Error::Ok;

}

/// Check exact-end bounds, physical alignment, arithmetic overflow, and authority.

export fn run() {

    domains::init(&mut DOMAINS[..]);

    resources::init(&mut OBJECTS[..]);

    contexts::init(&mut CONTEXTS[0], 0);

    let mut machine: platform::Platform = undefined;

    set machine.memoryCount = 0;

    set machine.reservedCount = 0;

    try! frames::init(&mut POOL, &machine);

    let mut ram: memory::Memory = undefined;

    memory::init(&mut ram, &mut POOL, &mut PINS[..], &mut ASSIGNED[..], &mut GRANTS[..], 1);

    set KERNEL = state::State { domains: &mut DOMAINS[..], resources: &mut OBJECTS[..], contexts: &mut CONTEXTS[..], memory: ram };

    let root = domains::root(&mut DOMAINS[..], 0);

    let registers = device(0x1000, 16);

    assert try! devices::access(&KERNEL, 0, registers, 8, 8, abi::READ) == 0x1008;

    assert error(registers, 16, 1, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 12, 8, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 0xffffffffffffffff, 2, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 0, 0, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 0, 3, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 1, 2, abi::READ) == abi::Error::InvalidArg;

    assert error(registers, 0, 1, 0) == abi::Error::InvalidArg;

    assert error(registers, 0, 1, abi::READ | abi::EXECUTE) == abi::Error::InvalidArg;

    assert error(registers, 0, 1, abi::READ | abi::WRITE) == abi::Error::Denied;

    assert error(root, 0, 1, abi::READ) == abi::Error::BadHandle;

    // Alignment belongs to the physical address, not just the region offset.

    let unaligned = device(0x2001, 8);

    assert try! devices::access(&KERNEL, 0, unaligned, 3, 4, abi::READ) == 0x2004;

    assert error(unaligned, 0, 4, abi::READ) == abi::Error::InvalidArg;

    let overflowing = device(0xfffffffffffffffc, 16);

    assert error(overflowing, 4, 1, abi::READ) == abi::Error::InvalidArg;

    // A still-packed handle cannot name another incarnation of its resource slot.

    let entry = try! capabilities::lookup(&KERNEL, 0, registers);

    set OBJECTS[entry.object.index].epoch += 1;

    assert error(registers, 0, 1, abi::READ) == abi::Error::BadHandle;

    try! capabilities::drop(&mut KERNEL, 0, unaligned);

    assert error(unaligned, 0, 1, abi::READ) == abi::Error::BadHandle;

}

// Byte MMIO for the trusted physical-device regression only.

.text;

.export @"interrupt::read8";

@"interrupt::read8"

	fence;

	lbu    %a0    0(%a0);

	fence;

	ret;

.export @"interrupt::write8";

@"interrupt::write8"

	fence;

	sb     %a1    0(%a0);

	fence;

	ret;

export mod devices;

export mod interrupts;

export mod mmio;

//! Capability-checked MMIO address materialization; never device I/O.

use core::abi;

use core::capabilities;

use core::resources;

use core::state;

/// Materialize one loader-verified MMIO instruction's complete byte range.

/// The returned address is not Page authority and is consumed by that instruction.

export fn access(kernel: *state::State, caller: u32, handle: abi::Handle, offset: u64, width: u64, rights: u16) -> u64 throws (abi::Error) {

    let entry = try capabilities::lookup(kernel, caller, handle);

    if entry.object.kind <> abi::Kind::Device { throw abi::Error::BadHandle; }

    if rights == 0 or rights & ~(abi::READ | abi::WRITE) <> 0 {

        throw abi::Error::InvalidArg;

    }

    if entry.rights & rights <> rights { throw abi::Error::Denied; }

    if width <> 1 and width <> 2 and width <> 4 and width <> 8 {

        throw abi::Error::InvalidArg;

    }

    let case resources::Value::Device(region) = kernel.resources[entry.object.index].value else {

        panic "access: device kind mismatch";

    };

    if offset > region.size or width > region.size - offset

        or region.base > 0xffffffffffffffff - offset {

        throw abi::Error::InvalidArg;

    }

    let address = region.base + offset;

    if address > 0xffffffffffffffff - (width - 1) or address % width <> 0 {

        throw abi::Error::InvalidArg;

    }

    return address;

}

//! Exclusive PLIC routing with retained claims and bounded queue backpressure.

use core::abi;

use core::domains;

use core::events;

use core::mmio;

use core::platform;

use core::resources;

use core::state;

/// Private state for one source; source zero is never enabled or published.

export record Source: Copy {

    /// Installed Interrupt resource identity, not its mutable receiver.

    object: abi::Object,

    /// A real hardware claim still awaiting publication or consumer progress.

    claimed: bool,

    /// Domain incarnation whose queue contains this claim, or the empty identity.

    published: abi::Object,

}

/// One machine-context PLIC service route, serialized by the kernel lock.

/// All online harts may call poll; only the selected hart handles external traps.

/// Domain execution routing and remote wakeups are separate from this controller.

export record Controller: Copy {

    /// Validated physical PLIC register base.

    base: u64,

    /// Actual FDT machine-context index, never derived from the hardware hart ID.

    context: u32,

    /// Largest usable source identifier; strictly less than MAX_IRQS.

    limit: u32,

    /// Shadow of the selected context's enable words; sole writer is this module.

    enabled: [u32; platform::MAX_IRQS / 32],

    /// Constant-space resource mapping and notification state, indexed by source.

    sources: [Source; platform::MAX_IRQS],

}

/// Initialize once before external interrupts or secondary kernel entry are enabled.

/// machine must be a validated platform and hartIndex an online-hart array index.

/// Sources stay disabled until register followed by poll observes a live receiver.

export unsafe fn init(controller: *mut Controller, machine: *platform::Platform, hartIndex: u32) {

    assert machine.hartCount > 0 and machine.hartCount <= platform::MAX_HARTS;

    assert hartIndex < machine.hartCount;

    assert machine.irqCount > 0 and machine.irqCount < platform::MAX_IRQS;

    set controller.base = machine.plic.base;

    set controller.context = machine.harts[hartIndex].plicContext;

    set controller.limit = machine.irqCount;

    set controller.enabled = [0; platform::MAX_IRQS / 32];

    for source in 0..platform::MAX_IRQS {

        set controller.sources[source] = Source {

            object: domains::none(), claimed: false, published: domains::none(),

        };

    }

    for hart in 0..machine.hartCount {

        let context = machine.harts[hart].plicContext as u64;

        // Touch only implemented source words; reserved PLIC words may fault.

        for word in 0..controller.limit / 32 + 1 {

            mmio::write32(controller.base + 0x2000 + context * 0x80 + word as u64 * 4, 0);

        }

        // Priority one is eligible only on the selected service context.

        let mut threshold: u32 = 1;

        if hart == hartIndex { set threshold = 0; }

        mmio::write32(controller.base + 0x200000 + context * 0x1000, threshold);

    }

    for source in 1..controller.limit + 1 {

        mmio::write32(controller.base + source as u64 * 4, 1);

    }

}

/// Bind an installed exclusive IRQ resource before its first poll; no MMIO occurs.

/// The mapping cannot be replaced, so resource-slot reuse never inherits a claim.

export fn register(controller: *mut Controller, source: u32, object: abi::Object) {

    assert source > 0 and source <= controller.limit;

    assert object.kind == abi::Kind::Interrupt and object.epoch <> 0;

    assert controller.sources[source].object.kind == abi::Kind::Empty;

    set controller.sources[source].object = object;

}

/// Change one selected-context enable bit without disturbing other source masks.

unsafe fn enable(controller: *mut Controller, source: u32, active: bool) {

    let word = source / 32;

    let bit: u32 = 1 << (source % 32);

    let previous = controller.enabled[word];

    let mut next = previous & ~bit;

    if active { set next = previous | bit; }

    if next == previous { return; }

    set controller.enabled[word] = next;

    mmio::write32(controller.base + 0x2000 + controller.context as u64 * 0x80 + word as u64 * 4, next);

}

/// Complete a retained hardware claim after user service, while its route is enabled.

/// A PLIC can ignore completion through a disabled route.

unsafe fn complete(controller: *mut Controller, source: u32) {

    enable(controller, source, true);

    mmio::write32(controller.base + 0x200004 + controller.context as u64 * 0x1000, source);

}

/// Resolve the current exclusive holder, checking both resource and domain epochs.

fn target(controller: *Controller, kernel: *state::State, source: u32) -> abi::Object {

    let object = controller.sources[source].object;

    if object.kind <> abi::Kind::Interrupt

        or not resources::live(kernel.resources, kernel.domains, object) {

        return domains::none();

    }

    let slot = &kernel.resources[object.index];

    let case resources::Value::Interrupt(irq) = slot.value else { return domains::none(); };

    if slot.references <> 1 or irq.number <> source or not domains::live(kernel.domains, irq.target) {

        return domains::none();

    }

    return irq.target;

}

/// Test the authoritative coalescing bit only after refresh accepted consumer head.

fn outstanding(queue: *events::Queue, source: u32) -> bool {

    return queue.pending[source / 64] & (1 << (source as u64 % 64)) <> 0;

}

/// Reconcile retained claims with current ownership and validated consumer progress.

/// Never claims hardware or fabricates a notification merely because a source exists.

/// A transfer republishes retained work to the new incarnation, coalescing if needed.

/// Drop or domain death discards work and leaves the source masked. Invalid consumer

/// progress also leaves it masked, but preserves the claim for a later valid head.

export unsafe fn poll(controller: *mut Controller, kernel: *mut state::State) {

    for source in 1..controller.limit + 1 {

        let receiver = target(controller, kernel, source);

        let pending = &mut controller.sources[source];

        if receiver.kind == abi::Kind::Empty {

            if pending.claimed { complete(controller, source); }

            set pending.claimed = false;

            set pending.published = domains::none();

            enable(controller, source, false);

            continue;

        }

        let queue = &mut kernel.domains[receiver.index].events;

        try events::refresh(queue) catch {

            enable(controller, source, false);

            continue;

        };

        if pending.claimed {

            let previous = pending.published;

            if previous.kind == abi::Kind::Domain and previous.index == receiver.index

                and previous.epoch == receiver.epoch {

                if not outstanding(queue, source) {

                    complete(controller, source);

                    set pending.claimed = false;

                    set pending.published = domains::none();

                }

            } else {

                // Keep the real claim across Busy and transfers until push succeeds.

                try events::push(queue, events::Event { kind: 1, reserved: 0, code: source, value: 0 }, events::Class::Interrupt(source)) catch {

                    enable(controller, source, false);

                    continue;

                };

                set pending.published = receiver;

            }

        }

        enable(controller, source, not pending.claimed and not outstanding(queue, source)

            and queue.ordinary < events::CAPACITY - events::CRITICAL);

    }

}

/// Claim at most limit sources, masking each until its notification is consumed.

/// The gateway stays active while the driver services the device. Consumer

/// progress permits completion and rearming without a held-level interrupt loop.

/// Call under the kernel lock; poll also runs before every subsequent user dispatch.

export unsafe fn handle(controller: *mut Controller, kernel: *mut state::State) {

    let claim = controller.base + 0x200004 + controller.context as u64 * 0x1000;

    for count in 0..controller.limit {

        let source = mmio::read32(claim);

        if source == 0 { break; }

        // Initialization disables every out-of-range source; never index by bad MMIO.

        if source > controller.limit {

            mmio::write32(claim, source);

            break;

        }

        enable(controller, source, false);

        set controller.sources[source].claimed = true;

        set controller.sources[source].published = domains::none();

    }

    poll(controller, kernel);

}

//! Machine-only access to validated, naturally aligned controller registers.

/// Read one mapped 32-bit register, ordered before and after all memory and I/O.

export unsafe fn read32(address: u64) -> u32;

/// Write one mapped 32-bit register, ordered before and after all memory and I/O.

export unsafe fn write32(address: u64, value: u32);

//! PLIC claims, level-triggered UART service, and exclusive receiver transfer.

use core::abi;

use core::atomic;

use core::capabilities;

use core::clock;

use core::contexts;

use core::cpu;

use core::devices;

use core::domains;

use core::events;

use core::fdt;

use core::frames;

use core::handles;

use core::interrupts;

use core::memory;

use core::mmio;

use core::platform;

use core::resources;

use core::state;

/// One ordered byte access to an already checked device address.

unsafe fn read8(address: u64) -> u8;

/// One ordered byte write to an already checked device address.

unsafe fn write8(address: u64, value: u8);

/// Independent interrupt receivers.

static DOMAINS: [domains::Domain; 2] = undefined;

/// One UART device and two exclusive interrupt sources.

static OBJECTS: [resources::Slot; 3] = undefined;

/// No user context is needed for this physical notification check.

static CONTEXTS: [contexts::Context; 1] = undefined;

/// Empty RAM accounting; this check does not allocate user Pages.

static POOL: frames::Pool = undefined;

/// Empty-pool pins.

static PINS: [u16; 1] = undefined;

/// Empty-pool claims.

static ASSIGNED: [bool; 1] = undefined;

/// Empty-pool grants.

static GRANTS: [u64; 2] = undefined;

/// Private PLIC ownership and coalescing state.

static PLIC: interrupts::Controller = undefined;

/// Serialized control-plane state.

static KERNEL: state::State = undefined;

/// Install exclusive authority for one real PLIC source.

fn interrupt(source: u32, root: abi::Object) -> abi::Handle {

    let object = try! resources::create(&mut OBJECTS[..], resources::Value::Interrupt(resources::Interrupt { number: source, target: root }));

    resources::retain(&mut OBJECTS[..], object);

    interrupts::register(&mut PLIC, source, object);

    return handles::install(&mut DOMAINS[0].handles, try! handles::vacant(&DOMAINS[0].handles), object, abi::RIGHTS);

}

/// Observe exactly one IRQ event, then release it to the producer.

fn consume(receiver: u32, source: u32) {

    let ring = &mut DOMAINS[receiver].events.ring;

    let head = atomic::load(&ring.head);

    assert atomic::load(&ring.tail) - head == 1;

    let event = ring.data[head & (events::CAPACITY - 1)];

    assert event.kind == 1 and event.code == source and event.value == 0;

    atomic::store(&mut ring.head, head + 1);

}

/// Read the physical enable register, not the controller's private shadow.

unsafe fn enabled(source: u32) -> bool {

    let address = PLIC.base + 0x2000 + PLIC.context as u64 * 0x80 + (source / 32) as u64 * 4;

    return mmio::read32(address) & (1 << (source % 32)) <> 0;

}

/// Wake from the next external interrupt and run the actual PLIC service path.

unsafe fn receive(frame: *mut cpu::Frame) {

    clock::interrupts(2048);

    cpu::idle(frame);

    clock::interrupts(0);

    assert frame.cause == 0x800000000000000b;

    interrupts::handle(&mut PLIC, &mut KERNEL);

}

/// Exercise an injected edge at tick 4,000,000 and UART byte R at tick 8,000,000.

@default unsafe fn main(hart: u64, description: *u8) -> u32 {

    assert hart == 0;

    let size = try! fdt::word(@sliceOf(description, 40), 4);

    assert size >= 40 and size <= fdt::MAX_BYTES;

    let mut tree: fdt::Tree = undefined;

    try! fdt::decode(@sliceOf(description, size), &mut tree);

    let mut machine: platform::Platform = undefined;

    try! platform::discover(&tree, &mut machine);

    assert machine.harts[0].id == 0 and machine.devices[0].irq == 10;

    interrupts::init(&mut PLIC, &machine, 0);

    domains::init(&mut DOMAINS[..]);

    resources::init(&mut OBJECTS[..]);

    contexts::init(&mut CONTEXTS[0], 0);

    let mut empty: platform::Platform = undefined;

    set empty.memoryCount = 0;

    set empty.reservedCount = 0;

    try! frames::init(&mut POOL, &empty);

    let mut ram: memory::Memory = undefined;

    memory::init(&mut ram, &mut POOL, &mut PINS[..], &mut ASSIGNED[..], &mut GRANTS[..], 2);

    set KERNEL = state::State { domains: &mut DOMAINS[..], resources: &mut OBJECTS[..], contexts: &mut CONTEXTS[..], memory: ram };

    let own = domains::root(&mut DOMAINS[..], 0);

    let root = try! domains::resolve(&DOMAINS[..], 0, own, abi::CREATE);

    let child = try! domains::create(&mut DOMAINS[..], root, 0);

    let target = handles::install(&mut DOMAINS[0].handles, 2, child, abi::DOMAIN_RIGHTS);

    let device = try! resources::create(&mut OBJECTS[..], resources::Value::Device(machine.devices[0].region));

    resources::retain(&mut OBJECTS[..], device);

    let uart = handles::install(&mut DOMAINS[0].handles, 3, device, abi::READ | abi::WRITE);

    let edge = interrupt(3, root);

    let _uartIrq = interrupt(10, root);

    write8(try! devices::access(&KERNEL, 0, uart, 1, 1, abi::WRITE), 1);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    assert enabled(3) and enabled(10);

    let mut frame: cpu::Frame = undefined;

    cpu::init(&mut frame, 0, 0, 0, 0);

    receive(&mut frame);

    assert not enabled(3);

    for i in 0..events::CAPACITY - events::CRITICAL {

        try! events::push(&mut DOMAINS[1].events, events::Event { kind: 5, reserved: 0, code: i, value: 0 }, events::Class::Ordinary);

    }

    let moved = try! capabilities::transfer(&mut KERNEL, 0, edge, target, abi::RIGHTS as u64);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    assert not enabled(3);

    consume(0, 3);

    atomic::store(&mut DOMAINS[1].events.ring.head, events::CAPACITY - events::CRITICAL);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    consume(1, 3);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    assert enabled(3);

    try! capabilities::drop(&mut KERNEL, 1, moved);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    assert not enabled(3);

    receive(&mut frame);

    assert not enabled(10);

    for i in 0..4 { interrupts::poll(&mut PLIC, &mut KERNEL); }

    let byte = read8(try! devices::access(&KERNEL, 0, uart, 0, 1, abi::READ));

    assert byte == 82;

    write8(try! devices::access(&KERNEL, 0, uart, 0, 1, abi::WRITE), byte);

    consume(0, 10);

    interrupts::poll(&mut PLIC, &mut KERNEL);

    assert enabled(10);

    clock::arm(machine.clint.base, machine.harts[0].clintIndex, clock::read(machine.clint.base) + 1000);

    clock::interrupts(2176);

    cpu::idle(&mut frame);

    clock::interrupts(0);

    clock::arm(machine.clint.base, machine.harts[0].clintIndex, 0xffffffffffffffff);

    assert frame.cause == 0x8000000000000007;

    return 0;

}