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

parallel.rv64: parallel.rad parallel/mailboxes.rad arch/start.ras core.rad $(MODULES) $(CORE_ASM) build/baseline/images.rad user/sys.ras $(COMPILER)

	$(COMPILE) $(BASE_CATALOG) $(CORE) -pkg parallel -start arch/start.ras -mod parallel.rad -mod parallel/mailboxes.rad -entry parallel -o $@

check: all check.rv64 context.rv64 interrupt.rv64 native.rv64 parallel.rv64

	$(MACHINE) -harts=1 -run parallel.rv64

	$(MACHINE) -harts=2 -run parallel.rv64

	$(MACHINE) -harts=8 -run parallel.rv64

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

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

## Hart startup and remote transport

- Each online hart enters M-mode on a private 64 KiB stack in reserved image

  memory. Hart zero release-publishes shared state; secondary harts acquire it

  before use. Each hart synchronizes local instruction fetch.

- One FIFO ticket lock serializes shared kernel mechanisms. Its Once guard must

  be released exactly once. Machine interrupts remain disabled while it is held.

  Wrapping u32 tickets stay distinct with at most eight callers.

- Each hart has eight ordinary FIFO request slots. Exact kind, domain incarnation,

  and context identity form the coalescing key. A full queue of distinct requests

  returns Busy without disturbing order. Transport itself grants no authority.

- CLINT publication uses firmware-selected banks and full memory/I/O fences.

  Queue drain and software-interrupt acknowledgement share the publication lock.

- Machine probes cover ticket wraparound, mailbox capacity, coherent increments,

  and software-interrupt wakeup after payload publication on 1, 2, and 8 harts.

  RV64A checks run in machine mode, not the hosted emulator.

Run machine mailbox/startup probes on 1, 2, and 8 harts, including wraparound, full queues, coherent shared increments, and CLINT wakeup after payload publication.

// RV64A FIFO tickets and machine-mode CLINT software interrupts.

.text;

.export @"core::smp::ticket";

@"core::smp::ticket"

	li     %t0    1;

	amoadd.w.aqrl %a0 %t0 0(%a0);

	// AMO word results are sign-extended by RV64; the Radiance u32 ABI is not.

	slli   %a0    %a0    32;

	srli   %a0    %a0    32;

	ret;

.export @"core::smp::hart";

@"core::smp::hart"

	csrr   %a0    mhartid;

	slli   %a0    %a0    32;

	srli   %a0    %a0    32;

	ret;

.export @"core::smp::kick";

@"core::smp::kick"

	slli   %a1    %a1    2;

	add    %a0    %a0    %a1;

	li     %t0    1;

	// Full iorw,iorw ordering publishes RAM before asserting MSIP.

	fence;

	sw     %t0    0(%a0);

	fence;

	ret;

.export @"core::smp::acknowledge";

@"core::smp::acknowledge"

	slli   %a1    %a1    2;

	add    %a0    %a0    %a1;

	// Full iorw,iorw ordering completes the MSIP clear before queue handling.

	fence;

	sw     %zero  0(%a0);

	fence;

	ret;

.export @"core::smp::syncInstructions";

@"core::smp::syncInstructions"

	fence.i;

	ret;

// M-mode entry on each hart with private 64 KiB stacks in reserved image RAM.

.text;

    csrw mie %zero;

    csrr %t0 mstatus;

    li %t1 -9;

    and %t0 %t0 %t1;

    csrw mstatus %t0;

    la %t0 @bootFault;

    csrw mtvec %t0;

    csrr %a0 mhartid;

    li %t0 8;

    bgeu %a0 %t0 @bootFault;

    la %sp @hartStacks;

    addi %t0 %a0 1;

    slli %t0 %t0 16;

    add %sp %sp %t0;

    call @"::default";

    csrr %t0 mhartid;

    bnez %t0 @bootIdle;

    li %t1 0x5555;

    j @bootFinish;

@bootFault

    csrr %t1 mcause;

    slli %t1 %t1 16;

    li %t0 0x3333;

    or %t1 %t1 %t0;

@bootFinish

    li %t0 0x10001000;

    sw %t1 0(%t0);

@bootIdle

    wfi;

    j @bootIdle;

.data;

.align 16;

@hartStacks

.space 524288;

export mod smp;

//! FIFO kernel serialization and bounded, identity-bearing remote messages.

//! One global Lock protects all kernel state and all Mailbox operations. User

//! architectural frames remain owned by their Running hart outside that lock.

use core::abi;

use core::atomic;

/// Maximum distinct requests retained by one hart's mailbox.

export constant CAPACITY: u32 = 8;

/// Naturally aligned FIFO ticket counters; never move or copy a published lock.

/// At most platform::MAX_HARTS callers may be outstanding, one per online hart.

export record Lock {

    /// Next ticket to allocate, modulo 2^32; accessed atomically after publication.

    next: u32,

    /// Ticket currently admitted, modulo 2^32; accessed atomically after publication.

    serving: u32,

}

/// Exact-use ownership of a held lock; consume only through release.

export union Guard: Once {

    /// Lock address and acquired ticket; the lock must outlive this obligation.

    Held {

        /// Stable address of the acquired kernel lock.

        lock: *mut Lock,

        /// Ticket whose turn was observed with acquire ordering.

        ticket: u32,

    },

}

/// Atomically allocate one wrapping ticket with acquire/release ordering.

/// The native RV64A implementation zero-extends the old word to the u32 ABI.

fn ticket(pointer: *mut u32) -> u32;

/// Initialize unshared storage once, before publishing its stable address.

/// Reinitializing a published lock or one with outstanding callers is forbidden.

export fn init(lock: *mut Lock) {

    set lock.next = 0;

    set lock.serving = 0;

}

/// Wait in ticket order and return the obligation to release this lock once.

/// The caller must keep machine interrupts disabled until release, must not

/// acquire recursively, and must keep the lock at a stable address. There may

/// be at most platform::MAX_HARTS outstanding callers, so u32 wrap is unambiguous.

export fn acquire(lock: *mut Lock) -> Guard {

    let acquired = ticket(&mut lock.next);

    while atomic::load(&lock.serving) <> acquired {}

    return Guard::Held { lock, ticket: acquired };

}

/// Consume a held lock and release-publish all kernel writes to the next ticket.

export fn release(guard: Guard) {

    match guard {

        case Guard::Held { lock, ticket: acquired } => {

            atomic::store(&mut lock.serving, ((acquired as u64 + 1) & 0xffffffff) as u32);

        },

    }

}

/// Remote mechanisms only; a request does not convey capability authority.

export union RequestKind: Copy {

    /// Reconsider a waiting context after authorized event publication.

    Wake,

    /// Dispatch an explicitly authorized context with its assigned budget.

    Run,

    /// Stop the named context before lifecycle reclamation can proceed.

    Stop,

}

/// A remote message, not authority: the receiver must recheck current domain

/// incarnation and context identity under the global lock before any mutation.

export record Request: Copy {

    /// Mechanism requested of the receiving hart.

    kind: RequestKind,

    /// Complete target domain identity, including its incarnation.

    domain: abi::Object,

    /// Complete target context identity, including its incarnation.

    context: u64,

}

/// Caller-owned FIFO storage; every access after initialization requires the

/// global kernel lock, including canPost. Keep admission and posting in the

/// same critical section when another state change depends on admission.

export record Mailbox {

    /// Circular request storage; only count entries starting at head are live.

    entries: [Request; CAPACITY],

    /// Index of the oldest live request, always less than CAPACITY.

    head: u32,

    /// Number of live distinct requests, never greater than CAPACITY.

    count: u32,

}

/// Initialize private mailbox storage before publication to any receiving hart.

export fn initMailbox(mailbox: *mut Mailbox) {

    let empty = Request {

        kind: RequestKind::Wake,

        domain: abi::Object { kind: abi::Kind::Empty, index: 0, epoch: 0 },

        context: 0,

    };

    set mailbox.entries = [empty; CAPACITY];

    set mailbox.head = 0;

    set mailbox.count = 0;

}

/// Compare the entire message key, including both object and context incarnations.

fn identical(left: Request, right: Request) -> bool {

    return left.kind == right.kind and left.domain.kind == right.domain.kind

        and left.domain.index == right.domain.index and left.domain.epoch == right.domain.epoch

        and left.context == right.context;

}

/// Search only live entries; the caller holds the global kernel lock.

fn contains(mailbox: *Mailbox, request: Request) -> bool {

    for offset in 0..mailbox.count {

        if identical(mailbox.entries[(mailbox.head + offset) % CAPACITY], request) { return true; }

    }

    return false;

}

/// Check admission without mutation while holding the global kernel lock.

/// An identical outstanding request is admissible even when the mailbox is full.

export fn canPost(mailbox: *Mailbox, request: Request) -> bool {

    return mailbox.count < CAPACITY or contains(mailbox, request);

}

/// Append or coalesce under the global kernel lock. Identical requests retain

/// their original FIFO position. Busy means a full distinct request, and leaves

/// all mailbox state unchanged. The sender authorizes the operation separately.

export fn post(mailbox: *mut Mailbox, request: Request) throws (abi::Error) {

    if contains(mailbox, request) { return; }

    if mailbox.count == CAPACITY { throw abi::Error::Busy; }

    set mailbox.entries[(mailbox.head + mailbox.count) % CAPACITY] = request;

    set mailbox.count = mailbox.count + 1;

}

/// Remove the oldest request under the global kernel lock, or return nil.

/// Revalidate the message's current identities before performing its operation.

export fn take(mailbox: *mut Mailbox) -> ?Request {

    if mailbox.count == 0 { return nil; }

    let request = mailbox.entries[mailbox.head];

    set mailbox.head = (mailbox.head + 1) % CAPACITY;

    set mailbox.count = mailbox.count - 1;

    return request;

}

/// Read mhartid in machine mode; boot must validate it fits platform::MAX_HARTS.

export unsafe fn hart() -> u32;

/// Set a validated CLINT MSIP bank with full memory and I/O ordering.

/// clint is the physical controller base; bank is its FDT-selected bank index,

/// not necessarily a hardware hart ID. Publish the request before calling.

export unsafe fn kick(clint: u64, bank: u32);

/// Clear a validated CLINT MSIP bank with full memory and I/O ordering.

/// Use the same lock as posting to serialize acknowledgement with queue drain;

/// clearing after an unlocked empty observation can lose a concurrent kick.

export unsafe fn acknowledge(clint: u64, bank: u32);

/// Synchronize this hart's instruction fetch after observing published code.

/// Each executing hart must call this before entering newly published code.

export unsafe fn syncInstructions();

//! Machine proof of per-hart stacks, coherent ticket locking, and CLINT requests.

use core::abi;

use core::atomic;

use core::clock;

use core::cpu;

use core::fdt;

use core::platform;

use core::smp;

mod mailboxes;

/// Release-published platform initialization.

static READY: u32 = 0;

/// Single FIFO lock for all protected counters and request mailboxes.

static LOCK: smp::Lock = undefined;

/// Firmware-selected hardware routes, immutable after publication.

static PLATFORM: platform::Platform = undefined;

/// Protected counter incremented by every actual hardware hart.

static COUNTER: u32 = 0;

/// Per-hart completion publication for each phase.

static DONE: [u32; platform::MAX_HARTS] = undefined;

/// Ordinary coherent data published before each software interrupt.

static PAYLOAD: [u32; platform::MAX_HARTS] = undefined;

/// Values observed by the receiving harts.

static OBSERVED: [u32; platform::MAX_HARTS] = undefined;

/// Bounded remote queues with the same lock as acknowledgement.

static MAILBOXES: [smp::Mailbox; platform::MAX_HARTS] = undefined;

/// Resolve a hardware ID to its validated firmware routing record.

fn route(hart: u32) -> platform::Hart {

    for i in 0..PLATFORM.hartCount {

        if PLATFORM.harts[i].id == hart { return PLATFORM.harts[i]; }

    }

    panic "route: executing hart absent from firmware";

}

/// Wait for all discovered harts, not absent array slots.

fn barrier(phase: u32) {

    for i in 0..PLATFORM.hartCount {

        let hart = PLATFORM.harts[i].id;

        while atomic::load(&DONE[hart]) < phase {}

    }

}

/// Execute the same kernel function independently on each online hart.

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

    assert hardware < platform::MAX_HARTS as u64;

    let hart = hardware as u32;

    if 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);

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

        smp::init(&mut LOCK);

        set LOCK.next = 0xfffffffc;

        set LOCK.serving = 0xfffffffc;

        for i in 0..platform::MAX_HARTS {

            atomic::store(&mut DONE[i], 0);

            set PAYLOAD[i] = 0;

            set OBSERVED[i] = 0;

            smp::initMailbox(&mut MAILBOXES[i]);

        }

        mailboxes::run();

        atomic::store(&mut READY, 1);

    } else {

        while atomic::load(&READY) == 0 {}

    }

    let routing = route(hart);

    assert smp::hart() == hart;

    smp::syncInstructions();

    clock::arm(PLATFORM.clint.base, routing.clintIndex, 0xffffffffffffffff);

    smp::acknowledge(PLATFORM.clint.base, routing.clintIndex);

    for i in 0..256 {

        let guard = smp::acquire(&mut LOCK);

        set COUNTER += 1;

        smp::release(guard);

    }

    atomic::store(&mut DONE[hart], 1);

    if hart == 0 {

        barrier(1);

        assert COUNTER == PLATFORM.hartCount * 256;

        for i in 0..PLATFORM.hartCount {

            let recipient = PLATFORM.harts[i];

            if recipient.id == 0 { continue; }

            let guard = smp::acquire(&mut LOCK);

            set PAYLOAD[recipient.id] = 100 + recipient.id;

            try! smp::post(&mut MAILBOXES[recipient.id], smp::Request {

                kind: smp::RequestKind::Wake,

                domain: abi::Object { kind: abi::Kind::Domain, index: 7, epoch: 11 },

                context: 0x100000000 | recipient.id as u64,

            });

            smp::kick(PLATFORM.clint.base, recipient.clintIndex);

            smp::release(guard);

        }

        atomic::store(&mut DONE[hart], 2);

        barrier(2);

        for i in 0..PLATFORM.hartCount {

            let recipient = PLATFORM.harts[i].id;

            if recipient <> 0 { assert OBSERVED[recipient] == 100 + recipient; }

        }

    } else {

        let mut frame: cpu::Frame = undefined;

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

        clock::interrupts(8);

        cpu::idle(&mut frame);

        clock::interrupts(0);

        assert frame.cause == 0x8000000000000003;

        let guard = smp::acquire(&mut LOCK);

        let request = smp::take(&mut MAILBOXES[hart]) else { panic "main: missing published request"; };

        assert request.kind == smp::RequestKind::Wake;

        assert request.domain.index == 7 and request.domain.epoch == 11;

        assert request.context == (0x100000000 | hart as u64);

        set OBSERVED[hart] = PAYLOAD[hart];

        smp::acknowledge(PLATFORM.clint.base, routing.clintIndex);

        smp::release(guard);

        atomic::store(&mut DONE[hart], 2);

    }

    return 0;

}

//! Real RV64A ticket wraparound and bounded remote-request queue contracts.

//! Machine checks use the kernel's atomic object code on a real emulated hart.

//! Queue checks hold a ticket guard for admission, publication, and consumption.

use core::abi;

use core::atomic;

use core::smp;

/// Make one valid domain message with an explicit full context identity.

fn request(kind: smp::RequestKind, epoch: u32, context: u64) -> smp::Request {

    return smp::Request {

        kind, domain: abi::Object { kind: abi::Kind::Domain, index: 7, epoch }, context,

    };

}

/// Reject a full distinct request without disturbing subsequent FIFO delivery.

fn busy(mailbox: *mut smp::Mailbox, message: smp::Request) {

    assert not smp::canPost(mailbox, message);

    try smp::post(mailbox, message) catch error {

        assert error == abi::Error::Busy;

        return;

    };

    panic "busy: full mailbox accepted a distinct request";

}

/// Consume and compare one whole message, including both incarnation fields.

fn expect(mailbox: *mut smp::Mailbox, expected: smp::Request) {

    let actual = smp::take(mailbox) else { panic "expect: mailbox lost a request"; };

    assert actual.kind == expected.kind;

    assert actual.domain.kind == expected.domain.kind;

    assert actual.domain.index == expected.domain.index;

    assert actual.domain.epoch == expected.domain.epoch;

    assert actual.context == expected.context;

}

/// Exercise full-ring coalescing, failed admission, FIFO order, and slot reuse.

/// The caller holds the same kernel lock for admission, publication, and drain.

fn capacity(mailbox: *mut smp::Mailbox) {

    for round in 0..2 {

        let base = 0x100000000 + round as u64 * 32;

        for i in 0..smp::CAPACITY {

            let message = request(smp::RequestKind::Wake, 3, base + i as u64);

            assert smp::canPost(mailbox, message);

            try! smp::post(mailbox, message);

        }

        let duplicate = request(smp::RequestKind::Wake, 3, base + 3);

        assert smp::canPost(mailbox, duplicate);

        try! smp::post(mailbox, duplicate);

        busy(mailbox, request(smp::RequestKind::Wake, 3, base + 99));

        for i in 0..4 {

            expect(mailbox, request(smp::RequestKind::Wake, 3, base + i as u64));

        }

        for i in smp::CAPACITY..smp::CAPACITY + 4 {

            let message = request(smp::RequestKind::Wake, 3, base + i as u64);

            assert smp::canPost(mailbox, message);

            try! smp::post(mailbox, message);

        }

        let retained = request(smp::RequestKind::Wake, 3, base + 6);

        assert smp::canPost(mailbox, retained);

        try! smp::post(mailbox, retained);

        busy(mailbox, request(smp::RequestKind::Stop, 3, base + 6));

        for i in 4..smp::CAPACITY + 4 {

            expect(mailbox, request(smp::RequestKind::Wake, 3, base + i as u64));

        }

        assert smp::take(mailbox) == nil;

    }

}

/// Distinct mechanism, domain slot, domain epoch, and context epoch all survive.

/// Reposting each exact key must neither add entries nor reorder the first post.

fn identities(mailbox: *mut smp::Mailbox) {

    let wake = request(smp::RequestKind::Wake, 3, 0x100000007);

    let run = request(smp::RequestKind::Run, 3, 0x100000007);

    let stop = request(smp::RequestKind::Stop, 3, 0x100000007);

    let domainEpoch = request(smp::RequestKind::Wake, 4, 0x100000007);

    let contextEpoch = request(smp::RequestKind::Wake, 3, 0x200000007);

    let mut domainSlot = wake;

    set domainSlot.domain.index = 8;

    let mut objectKind = wake;

    set objectKind.domain.kind = abi::Kind::Empty;

    // Mailbox keys are transport data, not authorization or a live-identity test.

    let messages = [wake, run, stop, domainEpoch, contextEpoch, domainSlot, objectKind];

    for i in 0..messages.len { try! smp::post(mailbox, messages[i]); }

    for i in 0..messages.len {

        assert smp::canPost(mailbox, messages[i]);

        try! smp::post(mailbox, messages[i]);

    }

    for i in 0..messages.len { expect(mailbox, messages[i]); }

    assert smp::take(mailbox) == nil;

    // A consumed key is a new request, not a permanently retained coalescing bit.

    try! smp::post(mailbox, wake);

    expect(mailbox, wake);

    assert smp::take(mailbox) == nil;

}

/// Acquire and release real tickets across 0xffffffff, including sign-bit values.

/// A missing AMO zero-extension would leave acquire spinning at the first ticket.

fn wraparound(lock: *mut smp::Lock) {

    // The lock is unshared and has no callers when its starting counters are seeded.

    atomic::store(&mut lock.next, 0xfffffffe);

    atomic::store(&mut lock.serving, 0xfffffffe);

    for i in 0..4 {

        let current = ((0xfffffffe + i as u64) & 0xffffffff) as u32;

        let next = ((current as u64 + 1) & 0xffffffff) as u32;

        let guard = smp::acquire(lock);

        assert atomic::load(&lock.serving) == current;

        assert atomic::load(&lock.next) == next;

        smp::release(guard);

        assert atomic::load(&lock.serving) == next;

    }

}

/// Exercise queue behavior under a real ticket guard and wrapping exact-use release.

export fn run() {

    let mut lock: smp::Lock = undefined;

    let mut mailbox: smp::Mailbox = undefined;

    smp::init(&mut lock);

    smp::initMailbox(&mut mailbox);

    wraparound(&mut lock);

    let guard = smp::acquire(&mut lock);

    assert smp::take(&mut mailbox) == nil;

    capacity(&mut mailbox);

    identities(&mut mailbox);

    smp::release(guard);

}