rv64: Add kernel synchronization primitives
fc84a1d3aaaa56718952e42350f8adeb883ce2bfea31f09c4cbf90544e1e29e8
Assisted-by: Codex:gpt-6
1 parent
10626288
kernel/kernel.rad
+1 -0
| 1 | 1 | //! Kernel resource management and machine execution. |
|
| 2 | 2 | ||
| 3 | 3 | use std::testing; |
|
| 4 | 4 | ||
| 5 | 5 | export mod range; |
|
| 6 | + | export mod sync; |
|
| 6 | 7 | @test export mod tests; |
kernel/kernel/sync.rad
added
+22 -0
| 1 | + | //! RV64 synchronization and ordered device access. |
|
| 2 | + | ||
| 3 | + | /// Allocate one wrapping ticket from a naturally aligned u32 counter. |
|
| 4 | + | export fn nextTicket(counter: &mut u32) -> u32; |
|
| 5 | + | /// Read a naturally aligned shared word with acquire ordering. |
|
| 6 | + | export fn loadAcquire(value: &u64) -> u64; |
|
| 7 | + | /// Publish a naturally aligned shared word with release ordering. |
|
| 8 | + | export fn storeRelease(value: &mut u64, next: u64); |
|
| 9 | + | /// Read a naturally aligned shared 32-bit word with acquire ordering. |
|
| 10 | + | export fn loadAcquire32(value: &u32) -> u32; |
|
| 11 | + | /// Publish a naturally aligned shared 32-bit word with release ordering. |
|
| 12 | + | export fn storeRelease32(value: &mut u32, next: u32); |
|
| 13 | + | /// Add to a naturally aligned shared word and return its previous value. |
|
| 14 | + | export fn fetchAdd(value: &mut u64, amount: u64) -> u64; |
|
| 15 | + | /// Synchronize local instruction fetch after executable bytes become visible. |
|
| 16 | + | export fn syncInstructions(); |
|
| 17 | + | /// Order memory and device accesses in both directions. |
|
| 18 | + | export fn deviceFence(); |
|
| 19 | + | /// Read a 32-bit device register with memory and I/O ordering. |
|
| 20 | + | export unsafe fn read32(address: &u32) -> u32; |
|
| 21 | + | /// Write a 32-bit device register with memory and I/O ordering. |
|
| 22 | + | export unsafe fn write32(address: &mut u32, value: u32); |
kernel/kernel/sync.ras
added
+73 -0
| 1 | + | //! RV64 synchronization boundary. Shared words must be naturally aligned. |
|
| 2 | + | .text; |
|
| 3 | + | .export @kernel::sync::nextTicket; |
|
| 4 | + | .export @kernel::sync::loadAcquire; |
|
| 5 | + | .export @kernel::sync::storeRelease; |
|
| 6 | + | .export @kernel::sync::loadAcquire32; |
|
| 7 | + | .export @kernel::sync::storeRelease32; |
|
| 8 | + | .export @kernel::sync::fetchAdd; |
|
| 9 | + | .export @kernel::sync::syncInstructions; |
|
| 10 | + | .export @kernel::sync::deviceFence; |
|
| 11 | + | .export @kernel::sync::read32; |
|
| 12 | + | .export @kernel::sync::write32; |
|
| 13 | + | ||
| 14 | + | // Allocate a wrapping ticket and return its zero-extended u32 value. |
|
| 15 | + | @kernel::sync::nextTicket |
|
| 16 | + | li %t0 1; |
|
| 17 | + | amoadd.w.aqrl %a0 %t0 (%a0); |
|
| 18 | + | slli %a0 %a0 32; |
|
| 19 | + | srli %a0 %a0 32; |
|
| 20 | + | ret; |
|
| 21 | + | ||
| 22 | + | // Order subsequent memory accesses after this load. |
|
| 23 | + | @kernel::sync::loadAcquire |
|
| 24 | + | ld %a0 0(%a0); |
|
| 25 | + | fence r rw; |
|
| 26 | + | ret; |
|
| 27 | + | ||
| 28 | + | // Order preceding memory accesses before this store. |
|
| 29 | + | @kernel::sync::storeRelease |
|
| 30 | + | fence rw w; |
|
| 31 | + | sd %a1 0(%a0); |
|
| 32 | + | ret; |
|
| 33 | + | ||
| 34 | + | // Order subsequent memory accesses after a zero-extended word load. |
|
| 35 | + | @kernel::sync::loadAcquire32 |
|
| 36 | + | lwu %a0 0(%a0); |
|
| 37 | + | fence r rw; |
|
| 38 | + | ret; |
|
| 39 | + | ||
| 40 | + | // Order preceding memory accesses before a word store. |
|
| 41 | + | @kernel::sync::storeRelease32 |
|
| 42 | + | fence rw w; |
|
| 43 | + | sw %a1 0(%a0); |
|
| 44 | + | ret; |
|
| 45 | + | ||
| 46 | + | // Atomically add with acquire and release ordering. |
|
| 47 | + | @kernel::sync::fetchAdd |
|
| 48 | + | amoadd.d.aqrl %a0 %a1 (%a0); |
|
| 49 | + | ret; |
|
| 50 | + | ||
| 51 | + | // Refresh the local instruction stream after code publication. |
|
| 52 | + | @kernel::sync::syncInstructions |
|
| 53 | + | fence.i; |
|
| 54 | + | ret; |
|
| 55 | + | ||
| 56 | + | // Order both memory and device accesses. |
|
| 57 | + | @kernel::sync::deviceFence |
|
| 58 | + | fence iorw iorw; |
|
| 59 | + | ret; |
|
| 60 | + | ||
| 61 | + | // Read a device word between full I/O barriers. |
|
| 62 | + | @kernel::sync::read32 |
|
| 63 | + | fence iorw iorw; |
|
| 64 | + | lwu %a0 0(%a0); |
|
| 65 | + | fence iorw iorw; |
|
| 66 | + | ret; |
|
| 67 | + | ||
| 68 | + | // Write a device word between full I/O barriers. |
|
| 69 | + | @kernel::sync::write32 |
|
| 70 | + | fence iorw iorw; |
|
| 71 | + | sw %a1 0(%a0); |
|
| 72 | + | fence iorw iorw; |
|
| 73 | + | ret; |
test/sync/build.rad
added
+50 -0
| 1 | + | //! Build a native image from the synchronization machine fixture. |
|
| 2 | + | ||
| 3 | + | use std::sys; |
|
| 4 | + | use std::io; |
|
| 5 | + | use std::sys::unix; |
|
| 6 | + | use std::lang::alloc; |
|
| 7 | + | use std::lang::strings; |
|
| 8 | + | use std::arch::rv64::asm; |
|
| 9 | + | use std::arch::rv64::image; |
|
| 10 | + | ||
| 11 | + | /// Assembly input storage. |
|
| 12 | + | static SOURCE: [u8; 65536] = [0; 65536]; |
|
| 13 | + | /// Encoded text words. |
|
| 14 | + | static TEXT: [u32; 4096] = [0; 4096]; |
|
| 15 | + | /// Assembly name and fixup storage. |
|
| 16 | + | static MEMORY: [u8; 4194304] = [0; 4194304]; |
|
| 17 | + | /// Interned assembly identifiers. |
|
| 18 | + | unsafe static STRINGS: strings::Pool = strings::Pool { table: undefined, count: 0 }; |
|
| 19 | + | ||
| 20 | + | /// Assemble startup and synchronization routines into one native code segment. |
|
| 21 | + | @default unsafe fn main(env: *sys::Env) -> i32 { |
|
| 22 | + | assert env.args.len == 3; |
|
| 23 | + | let length = unix::readFile(env.args[1], &mut SOURCE[..]) else panic "missing assembly"; |
|
| 24 | + | let mut arena = alloc::new(&mut MEMORY[..]); |
|
| 25 | + | let data: *mut [u8] = &mut []; |
|
| 26 | + | let program = try asm::assemble(asm::scanner::SourceKind::String, &SOURCE[..length], |
|
| 27 | + | &mut TEXT[..], &mut data[..], &mut arena, &mut STRINGS, 0) catch err { |
|
| 28 | + | match err { |
|
| 29 | + | case asm::Error::Invalid { offset, message } => { |
|
| 30 | + | io::printU32(offset); io::print(": "); io::printLn(message); |
|
| 31 | + | }, |
|
| 32 | + | else => io::printLn("assembly output full"), |
|
| 33 | + | } |
|
| 34 | + | return 1; |
|
| 35 | + | }; |
|
| 36 | + | assert program.externalFixups.len == 0; |
|
| 37 | + | let size = program.text.len * 4; |
|
| 38 | + | let header = try! image::header(image::Layout { |
|
| 39 | + | entry: 0x80010000, |
|
| 40 | + | code: image::Segment { address: 0x80010000, initialized: size, memory: size }, |
|
| 41 | + | roData: image::Segment { address: 0, initialized: 0, memory: 0 }, |
|
| 42 | + | rwData: image::Segment { address: 0x80020000, initialized: 0, memory: 4096 }, |
|
| 43 | + | }); |
|
| 44 | + | let fd = unix::openOpts(env.args[2], unix::OpenFlags(*unix::O_WRONLY | *unix::O_CREAT | *unix::O_TRUNC), 420); |
|
| 45 | + | assert fd >= 0; |
|
| 46 | + | let written = unix::writeAll(fd, &header[..]) and unix::writeAll(fd, @sliceOf(program.text.ptr as *u8, size)); |
|
| 47 | + | let closed = unix::close(fd) == 0; |
|
| 48 | + | assert written and closed; |
|
| 49 | + | return 0; |
|
| 50 | + | } |
test/sync/machine.ras
added
+118 -0
| 1 | + | //! Exercise code publication and contended metadata updates on each hart. |
|
| 2 | + | .constant EXPECTED HARTS * 100; |
|
| 3 | + | .text; |
|
| 4 | + | @entry |
|
| 5 | + | csrr %s6 mhartid; |
|
| 6 | + | li %s0 0x40010000; |
|
| 7 | + | slli %s0 %s0 1; |
|
| 8 | + | bnez %s6 @waitCode; |
|
| 9 | + | li %t0 1; |
|
| 10 | + | slli %t0 %t0 32; |
|
| 11 | + | addi %t0 %t0 -4; |
|
| 12 | + | sw %t0 0(%s0); |
|
| 13 | + | sw %t0 4(%s0); |
|
| 14 | + | li %t0 0x02a00513; |
|
| 15 | + | sw %t0 64(%s0); |
|
| 16 | + | li %t0 0x00008067; |
|
| 17 | + | sw %t0 68(%s0); |
|
| 18 | + | li %t0 37; |
|
| 19 | + | sw %t0 44(%s0); |
|
| 20 | + | addi %a0 %s0 40; |
|
| 21 | + | li %a1 -1; |
|
| 22 | + | call @kernel::sync::storeRelease32; |
|
| 23 | + | addi %a0 %s0 24; |
|
| 24 | + | li %a1 1; |
|
| 25 | + | call @kernel::sync::storeRelease; |
|
| 26 | + | @waitCode |
|
| 27 | + | addi %a0 %s0 24; |
|
| 28 | + | call @kernel::sync::loadAcquire; |
|
| 29 | + | beqz %a0 @waitCode; |
|
| 30 | + | addi %a0 %s0 40; |
|
| 31 | + | call @kernel::sync::loadAcquire32; |
|
| 32 | + | li %t0 1; |
|
| 33 | + | slli %t0 %t0 32; |
|
| 34 | + | addi %t0 %t0 -1; |
|
| 35 | + | bne %a0 %t0 @fail; |
|
| 36 | + | lwu %t0 44(%s0); |
|
| 37 | + | li %t1 37; |
|
| 38 | + | bne %t0 %t1 @fail; |
|
| 39 | + | call @kernel::sync::syncInstructions; |
|
| 40 | + | addi %t0 %s0 64; |
|
| 41 | + | jalr %ra %t0 0; |
|
| 42 | + | li %t0 42; |
|
| 43 | + | bne %a0 %t0 @fail; |
|
| 44 | + | li %s1 100; |
|
| 45 | + | @ticket |
|
| 46 | + | mv %a0 %s0; |
|
| 47 | + | call @kernel::sync::nextTicket; |
|
| 48 | + | mv %s2 %a0; |
|
| 49 | + | li %t0 100; |
|
| 50 | + | bne %s1 %t0 @acquire; |
|
| 51 | + | // Every hart holds its first ticket before any hart can enter the lock. |
|
| 52 | + | addi %a0 %s0 72; |
|
| 53 | + | li %a1 1; |
|
| 54 | + | call @kernel::sync::fetchAdd; |
|
| 55 | + | @queued |
|
| 56 | + | addi %a0 %s0 72; |
|
| 57 | + | call @kernel::sync::loadAcquire; |
|
| 58 | + | li %t0 HARTS; |
|
| 59 | + | bne %a0 %t0 @queued; |
|
| 60 | + | @acquire |
|
| 61 | + | addi %a0 %s0 4; |
|
| 62 | + | call @kernel::sync::loadAcquire32; |
|
| 63 | + | bne %a0 %s2 @acquire; |
|
| 64 | + | // The protected count must follow ticket order across the u32 wrap. |
|
| 65 | + | addi %t1 %s2 4; |
|
| 66 | + | slli %t1 %t1 32; |
|
| 67 | + | srli %t1 %t1 32; |
|
| 68 | + | ld %t0 8(%s0); |
|
| 69 | + | bne %t0 %t1 @fail; |
|
| 70 | + | addi %t0 %t0 1; |
|
| 71 | + | sd %t0 8(%s0); |
|
| 72 | + | addi %a0 %s0 4; |
|
| 73 | + | addi %a1 %s2 1; |
|
| 74 | + | call @kernel::sync::storeRelease32; |
|
| 75 | + | addi %s1 %s1 -1; |
|
| 76 | + | bnez %s1 @ticket; |
|
| 77 | + | addi %a0 %s0 16; |
|
| 78 | + | li %a1 1; |
|
| 79 | + | call @kernel::sync::fetchAdd; |
|
| 80 | + | addi %a0 %a0 1; |
|
| 81 | + | li %t0 HARTS; |
|
| 82 | + | beq %a0 %t0 @check; |
|
| 83 | + | @park |
|
| 84 | + | wfi; |
|
| 85 | + | j @park; |
|
| 86 | + | @check |
|
| 87 | + | ld %t0 8(%s0); |
|
| 88 | + | li %t1 EXPECTED; |
|
| 89 | + | bne %t0 %t1 @fail; |
|
| 90 | + | lwu %t0 0(%s0); |
|
| 91 | + | lwu %t2 4(%s0); |
|
| 92 | + | bne %t0 %t2 @fail; |
|
| 93 | + | addi %t1 %t1 -4; |
|
| 94 | + | bne %t0 %t1 @fail; |
|
| 95 | + | addi %t2 %s0 32; |
|
| 96 | + | lr.w.aq %t0 (%t2); |
|
| 97 | + | bnez %t0 @fail; |
|
| 98 | + | li %t1 13; |
|
| 99 | + | sc.w.rl %t0 %t1 (%t2); |
|
| 100 | + | bnez %t0 @fail; |
|
| 101 | + | lr.d.aq %t0 (%t2); |
|
| 102 | + | bne %t0 %t1 @fail; |
|
| 103 | + | sc.d.rl %t0 %zero (%t2); |
|
| 104 | + | bnez %t0 @fail; |
|
| 105 | + | li %a0 0x02000000; |
|
| 106 | + | call @kernel::sync::read32; |
|
| 107 | + | bnez %a0 @fail; |
|
| 108 | + | j @success; |
|
| 109 | + | @fail |
|
| 110 | + | li %a0 0x10001000; |
|
| 111 | + | li %a1 0x13333; |
|
| 112 | + | call @kernel::sync::write32; |
|
| 113 | + | ebreak; |
|
| 114 | + | @success |
|
| 115 | + | li %a0 0x10001000; |
|
| 116 | + | li %a1 0x5555; |
|
| 117 | + | call @kernel::sync::write32; |
|
| 118 | + | ebreak; |
test/sync/run
added
+13 -0
| 1 | + | #!/bin/sh |
|
| 2 | + | # Execute the synchronization boundary under deterministic hart interleaving. |
|
| 3 | + | set -eu |
|
| 4 | + | emulator=${RAD_EMULATOR:-emulator} |
|
| 5 | + | work=$(mktemp -d) |
|
| 6 | + | trap 'rm -rf "$work"' EXIT HUP INT TERM |
|
| 7 | + | for harts in 1 2 8; do |
|
| 8 | + | printf '.constant HARTS %s;\n' "$harts" > "$work/sync.ras" |
|
| 9 | + | cat test/sync/machine.ras kernel/kernel/sync.ras >> "$work/sync.ras" |
|
| 10 | + | "$emulator" -run bin/sync.build.rv64 -- "$work/sync.ras" "$work/sync.rv64" |
|
| 11 | + | "$emulator" -machine -harts="$harts" -run "$work/sync.rv64" |
|
| 12 | + | done |
|
| 13 | + | printf 'synchronization: code publication, locks, atomics, and MMIO passed on 1/2/8 harts\n' |