kernel: Add system acceptance and invariant tests
3342aa20da3e20bdbb50fefcd0c8f734ea7da38cb271218cf7536991ae2edbed
1 parent
3cff2b05
Makefile
+15 -1
| 21 | 21 | ||
| 22 | 22 | # Verify the emulator binary exists. |
|
| 23 | 23 | EMU_PATH := $(shell command -v $(EMU) 2>/dev/null) |
|
| 24 | 24 | ||
| 25 | 25 | default: emulator $(RAD_BIN) |
|
| 26 | - | test: emulator seed-test std-test bin-test kernel-test module-test package-test native-test shared-test sync-test kernel-boot-test trap-test page-test loader-test dispatch-test smp-test termination-test runtime-test bootstrap-test mmio-test scheduling-test |
|
| 26 | + | test: emulator seed-test std-test bin-test kernel-test module-test package-test native-test shared-test sync-test kernel-boot-test trap-test page-test loader-test dispatch-test smp-test termination-test runtime-test bootstrap-test mmio-test cycles-test kernel-size-check scheduling-test |
|
| 27 | 27 | ||
| 28 | 28 | seed-test: |
|
| 29 | 29 | @seed/test |
|
| 30 | 30 | ||
| 31 | 31 | module-test: emulator $(RAD_BIN) |
| 251 | 251 | ||
| 252 | 252 | # Checked user-mode register access, including rejection before device effects. |
|
| 253 | 253 | .PHONY: mmio-test |
|
| 254 | 254 | mmio-test: $(RAD_BIN) $(BIN_DIR)/kernel.build.rv64 |
|
| 255 | 255 | @RAD_EMULATOR="$(EMU)" sh test/dispatch/run mmio |
|
| 256 | + | ||
| 257 | + | # Physical source-line limits and fixed native image memory. |
|
| 258 | + | .PHONY: kernel-size-check |
|
| 259 | + | kernel-size-check: $(BIN_DIR)/kernel.rv64 |
|
| 260 | + | @python3 test/acceptance/sizes |
|
| 261 | + | ||
| 262 | + | # Full sibling-emulator and kernel validation with retained acceptance reports. |
|
| 263 | + | .PHONY: kernel-acceptance |
|
| 264 | + | kernel-acceptance: |
|
| 265 | + | @sh test/acceptance/run |
|
| 266 | + | ||
| 267 | + | .PHONY: cycles-test |
|
| 268 | + | cycles-test: $(RAD_BIN) $(BIN_DIR)/kernel.build.rv64 |
|
| 269 | + | @RAD_EMULATOR="$(EMU)" sh test/cycles/run |
kernel/kernel/sync.rad
+14 -0
| 4 | 4 | static NEXT: u32 = 0; |
|
| 5 | 5 | /// Metadata ticket permitted to enter the critical section. |
|
| 6 | 6 | static SERVING: u32 = 0; |
|
| 7 | 7 | /// Largest observed instruction count inside the metadata lock. |
|
| 8 | 8 | static MAXIMUM: u64 = 0; |
|
| 9 | + | /// Largest observed instruction count from ticket request to lock acquisition. |
|
| 10 | + | static MAXIMUM_WAIT: u64 = 0; |
|
| 9 | 11 | ||
| 10 | 12 | /// Interrupt state and start counter retained by one metadata transaction. |
|
| 11 | 13 | export record Section: Copy { |
|
| 12 | 14 | /// Original machine interrupt-enable bit. |
|
| 13 | 15 | interrupts: u64, |
| 32 | 34 | ||
| 33 | 35 | /// Acquire shared metadata in ticket order with local interrupts masked. |
|
| 34 | 36 | /// Calls must not nest. At most one ticket per online hart can be outstanding. |
|
| 35 | 37 | export fn enter() -> Guard { |
|
| 36 | 38 | let interrupts = maskInterrupts(); |
|
| 39 | + | let requested = retired(); |
|
| 37 | 40 | let ticket = nextTicket(&mut NEXT); |
|
| 38 | 41 | while loadAcquire32(&SERVING) <> ticket {} |
|
| 39 | 42 | let start = retired(); |
|
| 43 | + | let wait = start - requested; |
|
| 44 | + | if wait > MAXIMUM_WAIT { set MAXIMUM_WAIT = wait; } |
|
| 40 | 45 | return Guard::Held(Section { interrupts, start, ticket }); |
|
| 41 | 46 | } |
|
| 42 | 47 | ||
| 43 | 48 | /// Publish metadata and restore the acquiring hart's interrupt state. |
|
| 44 | 49 | export fn leave(guard: Guard) { |
| 58 | 63 | let value = MAXIMUM; |
|
| 59 | 64 | leave(guard); |
|
| 60 | 65 | return value; |
|
| 61 | 66 | } |
|
| 62 | 67 | ||
| 68 | + | /// Read the maximum measured ticket acquisition work under serialization. |
|
| 69 | + | /// This includes the acquisition of the reporting call itself. |
|
| 70 | + | export fn maximumWait() -> u64 { |
|
| 71 | + | let guard = enter(); |
|
| 72 | + | let value = MAXIMUM_WAIT; |
|
| 73 | + | leave(guard); |
|
| 74 | + | return value; |
|
| 75 | + | } |
|
| 76 | + | ||
| 63 | 77 | /// Allocate one wrapping ticket from a naturally aligned u32 counter. |
|
| 64 | 78 | export fn nextTicket(counter: &mut u32) -> u32; |
|
| 65 | 79 | /// Read a naturally aligned shared word with acquire ordering. |
|
| 66 | 80 | export fn loadAcquire(value: &u64) -> u64; |
|
| 67 | 81 | /// Publish a naturally aligned shared word with release ordering. |
test/acceptance/metrics
added
+113 -0
| 1 | + | #!/usr/bin/env python3 |
|
| 2 | + | """Require the native acceptance matrix and report observed metadata work.""" |
|
| 3 | + | ||
| 4 | + | import pathlib |
|
| 5 | + | import re |
|
| 6 | + | import sys |
|
| 7 | + | ||
| 8 | + | ||
| 9 | + | def report(path): |
|
| 10 | + | """Read completed fixture records without accepting partial test output.""" |
|
| 11 | + | lines = path.read_text().splitlines() |
|
| 12 | + | completed = set(lines) |
|
| 13 | + | samples = {} |
|
| 14 | + | waits = {} |
|
| 15 | + | pending = None |
|
| 16 | + | pending_wait = None |
|
| 17 | + | invariants = False |
|
| 18 | + | cycles_invariants = False |
|
| 19 | + | cycles_pending = None |
|
| 20 | + | cycles_wait = None |
|
| 21 | + | for line in lines: |
|
| 22 | + | if line == "smp final ownership and interval invariants passed": |
|
| 23 | + | if invariants: |
|
| 24 | + | raise ValueError("duplicate SMP invariant completion") |
|
| 25 | + | invariants = True |
|
| 26 | + | elif match := re.fullmatch(r"smp metadata instructions: 0x([0-9a-f]+)", line): |
|
| 27 | + | pending = int(match[1], 16) |
|
| 28 | + | elif match := re.fullmatch(r"smp acquisition instructions: 0x([0-9a-f]+)", line): |
|
| 29 | + | pending_wait = int(match[1], 16) |
|
| 30 | + | elif match := re.fullmatch(r"smp: ([128])-hart execution passed", line): |
|
| 31 | + | if pending is None or pending <= 0: |
|
| 32 | + | raise ValueError("SMP completion has no positive metadata measurement") |
|
| 33 | + | if not invariants: |
|
| 34 | + | raise ValueError("SMP completion has no final invariant check") |
|
| 35 | + | invariants = False |
|
| 36 | + | name = f"SMP {match[1]} harts" |
|
| 37 | + | if name in samples: |
|
| 38 | + | raise ValueError("duplicate SMP completion") |
|
| 39 | + | samples[name] = pending |
|
| 40 | + | waits[name] = pending_wait |
|
| 41 | + | pending = None |
|
| 42 | + | pending_wait = None |
|
| 43 | + | elif line == "cycles final recovery and invariants passed": |
|
| 44 | + | if cycles_invariants: |
|
| 45 | + | raise ValueError("duplicate cycles invariant completion") |
|
| 46 | + | cycles_invariants = True |
|
| 47 | + | elif match := re.fullmatch(r"cycles metadata instructions: ([0-9a-f]+)", line): |
|
| 48 | + | cycles_pending = int(match[1], 16) |
|
| 49 | + | elif match := re.fullmatch(r"cycles acquisition instructions: ([0-9a-f]+)", line): |
|
| 50 | + | cycles_wait = int(match[1], 16) |
|
| 51 | + | elif match := re.fullmatch(r"cycles: ([128])-hart load, spawn, yield, fault, and recovery passed", line): |
|
| 52 | + | if not cycles_invariants or cycles_pending is None or cycles_pending <= 0: |
|
| 53 | + | raise ValueError("cycles completion has no final invariants or metadata measurement") |
|
| 54 | + | name = f"cycles {match[1]} harts" |
|
| 55 | + | if name in samples: |
|
| 56 | + | raise ValueError("duplicate cycles completion") |
|
| 57 | + | samples[name] = cycles_pending |
|
| 58 | + | waits[name] = cycles_wait |
|
| 59 | + | cycles_invariants = False |
|
| 60 | + | cycles_pending = None |
|
| 61 | + | cycles_wait = None |
|
| 62 | + | elif match := re.fullmatch(r"runtime (admission )?metadata instructions: ([0-9a-f]+)", line): |
|
| 63 | + | name = "runtime admission" if match[1] else "runtime completion" |
|
| 64 | + | if name in samples: |
|
| 65 | + | raise ValueError("duplicate runtime metadata measurement") |
|
| 66 | + | samples[name] = int(match[2], 16) |
|
| 67 | + | elif match := re.fullmatch(r"runtime (admission )?acquisition instructions: ([0-9a-f]+)", line): |
|
| 68 | + | name = "runtime admission" if match[1] else "runtime completion" |
|
| 69 | + | if name in waits: |
|
| 70 | + | raise ValueError("duplicate runtime acquisition measurement") |
|
| 71 | + | waits[name] = int(match[2], 16) |
|
| 72 | + | names = {"SMP 1 harts", "SMP 2 harts", "SMP 8 harts", "runtime admission", "runtime completion"} |
|
| 73 | + | names.update(f"cycles {harts} harts" for harts in (1, 2, 8)) |
|
| 74 | + | if samples.keys() != names or any(value <= 0 for value in samples.values()): |
|
| 75 | + | raise ValueError("metadata measurements are incomplete") |
|
| 76 | + | if waits.keys() != names or any(value is None or value <= 0 for value in waits.values()): |
|
| 77 | + | raise ValueError("acquisition measurements are incomplete") |
|
| 78 | + | required = { |
|
| 79 | + | "dispatch: 1-hart execution passed", |
|
| 80 | + | "termination: 1-hart execution passed", |
|
| 81 | + | "runtime: scheduled cancellation, retry, and publication passed", |
|
| 82 | + | "bootstrap: root exit preserves allocation and creation authority", |
|
| 83 | + | "mmio: 1-hart execution passed", |
|
| 84 | + | } |
|
| 85 | + | for harts in (1, 2, 8): |
|
| 86 | + | required.add(f"scheduling: {harts}-hart root handoff, four user-space yields, and checked shutdown passed") |
|
| 87 | + | for profile, counts in (("dispatch", (1,)), ("smp", (1, 2, 8)), ("termination", (1,)), |
|
| 88 | + | ("runtime", (1,)), ("bootstrap", (1,)), ("mmio", (1,)), |
|
| 89 | + | ("scheduling", (1, 2, 8)), ("cycles", (1, 2, 8))): |
|
| 90 | + | for harts in counts: |
|
| 91 | + | required.add(f"replay: {profile} {harts}-hart output matched") |
|
| 92 | + | if missing := required - completed: |
|
| 93 | + | raise ValueError("native completions are missing: " + "; ".join(sorted(missing))) |
|
| 94 | + | for name, value in sorted(samples.items()): |
|
| 95 | + | print(f"{name}: {value} maximum metadata instructions") |
|
| 96 | + | print(f"{name}: {waits[name]} maximum acquisition instructions") |
|
| 97 | + | print(f"SMP/runtime/cycles maximum observed metadata work: {max(samples.values())} instructions") |
|
| 98 | + | print(f"SMP/runtime/cycles maximum observed acquisition work: {max(waits.values())} instructions") |
|
| 99 | + | ||
| 100 | + | ||
| 101 | + | def main(): |
|
| 102 | + | """Report a log produced by the acceptance runner.""" |
|
| 103 | + | if len(sys.argv) != 2: |
|
| 104 | + | raise ValueError("usage: metrics test-log") |
|
| 105 | + | report(pathlib.Path(sys.argv[1])) |
|
| 106 | + | ||
| 107 | + | ||
| 108 | + | if __name__ == "__main__": |
|
| 109 | + | try: |
|
| 110 | + | main() |
|
| 111 | + | except (OSError, ValueError) as error: |
|
| 112 | + | print(f"kernel acceptance: {error}", file=sys.stderr) |
|
| 113 | + | sys.exit(1) |
test/acceptance/run
added
+16 -0
| 1 | + | #!/bin/sh |
|
| 2 | + | # Build and test the sibling emulator and the full kernel before reporting acceptance. |
|
| 3 | + | set -eu |
|
| 4 | + | mkdir -p bin/acceptance |
|
| 5 | + | if ! make -C ../kernel-emulator test > bin/acceptance/emulator.log 2>&1; then |
|
| 6 | + | cat bin/acceptance/emulator.log |
|
| 7 | + | exit 1 |
|
| 8 | + | fi |
|
| 9 | + | if ! KERNEL_REPLAY=1 make test RAD_EMULATOR=../kernel-emulator/bin/emulator > bin/acceptance/kernel.log 2>&1; then |
|
| 10 | + | cat bin/acceptance/kernel.log |
|
| 11 | + | exit 1 |
|
| 12 | + | fi |
|
| 13 | + | python3 test/acceptance/sizes > bin/acceptance/sizes.log |
|
| 14 | + | python3 test/acceptance/metrics bin/acceptance/kernel.log > bin/acceptance/metrics.log |
|
| 15 | + | cat bin/acceptance/sizes.log bin/acceptance/metrics.log |
|
| 16 | + | printf 'kernel acceptance: emulator and complete kernel matrix passed\n' |
test/acceptance/sizes
added
+87 -0
| 1 | + | #!/usr/bin/env python3 |
|
| 2 | + | """Check kernel source limits and report the built image's fixed memory.""" |
|
| 3 | + | ||
| 4 | + | import pathlib |
|
| 5 | + | import struct |
|
| 6 | + | import sys |
|
| 7 | + | ||
| 8 | + | ||
| 9 | + | def source_sizes(root): |
|
| 10 | + | """Count physical source lines and combine files that form one module.""" |
|
| 11 | + | totals = {"runtime": 0, "tests": 0, "tools": 0} |
|
| 12 | + | modules = {} |
|
| 13 | + | for path in sorted(root.rglob("*")): |
|
| 14 | + | if path.suffix not in (".rad", ".ras"): |
|
| 15 | + | continue |
|
| 16 | + | relative = path.relative_to(root) |
|
| 17 | + | category = "runtime" |
|
| 18 | + | if "tests" in relative.parts or path.stem == "tests": |
|
| 19 | + | category = "tests" |
|
| 20 | + | elif relative.parts[0] == "tools": |
|
| 21 | + | category = "tools" |
|
| 22 | + | lines = len(path.read_bytes().splitlines()) |
|
| 23 | + | totals[category] += lines |
|
| 24 | + | if category != "tests": |
|
| 25 | + | module = str(relative.with_suffix("")) |
|
| 26 | + | modules[module] = modules.get(module, 0) + lines |
|
| 27 | + | if not totals["runtime"]: |
|
| 28 | + | raise ValueError("kernel runtime sources are missing") |
|
| 29 | + | for module, lines in sorted(modules.items()): |
|
| 30 | + | print(f"module {module}: {lines} source lines") |
|
| 31 | + | if lines >= 1000: |
|
| 32 | + | raise ValueError(f"module {module} must have fewer than 1000 lines") |
|
| 33 | + | for category, lines in totals.items(): |
|
| 34 | + | print(f"kernel {category}: {lines} source lines") |
|
| 35 | + | if totals["runtime"] > 12000: |
|
| 36 | + | raise ValueError("kernel runtime exceeds 12000 source lines") |
|
| 37 | + | ||
| 38 | + | ||
| 39 | + | def image_sizes(path): |
|
| 40 | + | """Validate the native image extents and report each fixed memory segment.""" |
|
| 41 | + | with path.open("rb") as stream: |
|
| 42 | + | header = stream.read(64) |
|
| 43 | + | if len(header) != 64: |
|
| 44 | + | raise ValueError("native image header is truncated") |
|
| 45 | + | magic, version, entry = struct.unpack_from("<IIQ", header) |
|
| 46 | + | if magic != 0x30444152 or version != 2: |
|
| 47 | + | raise ValueError("expected a version 2 native image") |
|
| 48 | + | segments = [] |
|
| 49 | + | payload = 64 |
|
| 50 | + | for index, name in enumerate(("code", "read-only", "writable")): |
|
| 51 | + | address, initialized, memory = struct.unpack_from("<QII", header, 16 + index * 16) |
|
| 52 | + | alignment = 4 if index == 0 else 8 |
|
| 53 | + | if initialized > memory or address + memory > 1 << 64: |
|
| 54 | + | raise ValueError(f"invalid {name} segment extent") |
|
| 55 | + | if memory and address % alignment: |
|
| 56 | + | raise ValueError(f"misaligned {name} segment") |
|
| 57 | + | segments.append((address, initialized, memory)) |
|
| 58 | + | payload += initialized |
|
| 59 | + | print(f"image {name}: {memory} fixed bytes, {initialized} initialized bytes") |
|
| 60 | + | code, initialized, _ = segments[0] |
|
| 61 | + | if entry % 4 or initialized % 4 or not code <= entry < code + initialized: |
|
| 62 | + | raise ValueError("entry is outside initialized instructions") |
|
| 63 | + | for index, (start, _, size) in enumerate(segments): |
|
| 64 | + | for other, _, length in segments[index + 1:]: |
|
| 65 | + | if size and length and start < other + length and other < start + size: |
|
| 66 | + | raise ValueError("native image segments overlap") |
|
| 67 | + | if path.stat().st_size != payload: |
|
| 68 | + | raise ValueError("native image payload size does not match its header") |
|
| 69 | + | print(f"image total: {sum(segment[2] for segment in segments)} fixed bytes") |
|
| 70 | + | ||
| 71 | + | ||
| 72 | + | def main(): |
|
| 73 | + | """Check the worktree, or explicit source and image paths for a fixture.""" |
|
| 74 | + | if len(sys.argv) not in (1, 3): |
|
| 75 | + | raise ValueError("usage: sizes [kernel-directory native-image]") |
|
| 76 | + | root = pathlib.Path(sys.argv[1] if len(sys.argv) == 3 else "kernel") |
|
| 77 | + | image = pathlib.Path(sys.argv[2] if len(sys.argv) == 3 else "bin/kernel.rv64") |
|
| 78 | + | source_sizes(root) |
|
| 79 | + | image_sizes(image) |
|
| 80 | + | ||
| 81 | + | ||
| 82 | + | if __name__ == "__main__": |
|
| 83 | + | try: |
|
| 84 | + | main() |
|
| 85 | + | except (OSError, ValueError) as error: |
|
| 86 | + | print(f"kernel size check: {error}", file=sys.stderr) |
|
| 87 | + | sys.exit(1) |
test/cycles/job.rad
added
+23 -0
| 1 | + | //! A private worker instance that exits normally or raises a CPU fault. |
|
| 2 | + | use support; |
|
| 3 | + | export mod abi; |
|
| 4 | + | export mod sys; |
|
| 5 | + | ||
| 6 | + | /// Worker startup values supplied by its controller. |
|
| 7 | + | record Env: Copy { |
|
| 8 | + | /// Readable argument memory. |
|
| 9 | + | argsPointer: *opaque, |
|
| 10 | + | /// Zero selects normal exit; one selects a fault. |
|
| 11 | + | argsSize: u64, |
|
| 12 | + | /// Installed event capability. |
|
| 13 | + | eventsHandle: u64, |
|
| 14 | + | /// Shared event-ring address. |
|
| 15 | + | eventsPointer: u64, |
|
| 16 | + | } |
|
| 17 | + | ||
| 18 | + | /// Check private dependency state before the selected terminal operation. |
|
| 19 | + | @default fn main(env: *Env) { |
|
| 20 | + | assert support::advance() == 1; |
|
| 21 | + | if env.argsSize == 0 { sys::exit(9); } |
|
| 22 | + | assert false; |
|
| 23 | + | } |
test/cycles/kernel/dispatchcheck.rad
added
+237 -0
| 1 | + | //! Concurrent private package graphs and complete worker resource recovery. |
|
| 2 | + | use std::mem; |
|
| 3 | + | use kernel::abi; |
|
| 4 | + | use kernel::frames; |
|
| 5 | + | use kernel::slots; |
|
| 6 | + | use kernel::backing; |
|
| 7 | + | use kernel::pages; |
|
| 8 | + | use kernel::capability; |
|
| 9 | + | use kernel::registry; |
|
| 10 | + | use kernel::loader; |
|
| 11 | + | use kernel::domains; |
|
| 12 | + | use kernel::budgets; |
|
| 13 | + | use kernel::dispatch; |
|
| 14 | + | use kernel::boot; |
|
| 15 | + | use kernel::sync; |
|
| 16 | + | use kernel::remote; |
|
| 17 | + | use kernel::events; |
|
| 18 | + | use kernel::devices; |
|
| 19 | + | use kernel::platform; |
|
| 20 | + | use kernel::invariants; |
|
| 21 | + | use kernel::dispatchinput; |
|
| 22 | + | ||
| 23 | + | /// Bootstrap resource capabilities. |
|
| 24 | + | unsafe static TABLE: capability::Table = undefined; |
|
| 25 | + | /// Fixture publication barrier. |
|
| 26 | + | static READY: u64 = 0; |
|
| 27 | + | /// Surviving event consumer. |
|
| 28 | + | unsafe static PARENT: abi::Ref = undefined; |
|
| 29 | + | /// Controller identities indexed by hart. |
|
| 30 | + | unsafe static CHILDREN: [abi::Ref; 8] = undefined; |
|
| 31 | + | /// Bootstrap-owned argument page addresses indexed by hart. |
|
| 32 | + | static ARGUMENTS: [u64; 8] = [0; 8]; |
|
| 33 | + | /// Free frames before controller creation. |
|
| 34 | + | static FREE: u32 = 0; |
|
| 35 | + | /// Reusable page, backing, domain, and context slots before controller creation. |
|
| 36 | + | static SLOTS: [u32; 4] = [0; 4]; |
|
| 37 | + | /// Validated physical page mapping. |
|
| 38 | + | fn memory(address: u64) -> *mut u8; |
|
| 39 | + | /// Current kernel package-state table. |
|
| 40 | + | fn kernelGp() -> u64; |
|
| 41 | + | /// Native checker entry. |
|
| 42 | + | fn completion() -> u64; |
|
| 43 | + | /// Write one diagnostic byte. |
|
| 44 | + | fn put(byte: u8); |
|
| 45 | + | /// Finish the native fixture. |
|
| 46 | + | fn finish(); |
|
| 47 | + | ||
| 48 | + | /// Count reusable frames in short metadata sections. |
|
| 49 | + | unsafe fn freeFrames() -> u32 { |
|
| 50 | + | let mut count: u32 = 0; |
|
| 51 | + | let mut first: u32 = 0; |
|
| 52 | + | while first < pages::STORE.backings.pool.count { |
|
| 53 | + | let mut end = first + 128; |
|
| 54 | + | if end > pages::STORE.backings.pool.count { set end = pages::STORE.backings.pool.count; } |
|
| 55 | + | let guard = sync::enter(); |
|
| 56 | + | for i in first..end { if frames::available(&pages::STORE.backings.pool, i) { set count += 1; } } |
|
| 57 | + | sync::leave(guard); |
|
| 58 | + | set first = end; |
|
| 59 | + | } |
|
| 60 | + | return count; |
|
| 61 | + | } |
|
| 62 | + | ||
| 63 | + | /// Count reusable object slots after all allocation transactions have stopped. |
|
| 64 | + | fn freeSlots(entries: &[slots::Slot]) -> u32 { |
|
| 65 | + | let mut count: u32 = 0; |
|
| 66 | + | let mut first: u32 = 0; |
|
| 67 | + | while first < entries.len { |
|
| 68 | + | let mut end = first + 128; |
|
| 69 | + | if end > entries.len { set end = entries.len; } |
|
| 70 | + | let guard = sync::enter(); |
|
| 71 | + | for i in first..end { |
|
| 72 | + | assert entries[i].state <> slots::State::Reserved; |
|
| 73 | + | if entries[i].state == slots::State::Free { set count += 1; } |
|
| 74 | + | } |
|
| 75 | + | sync::leave(guard); |
|
| 76 | + | set first = end; |
|
| 77 | + | } |
|
| 78 | + | return count; |
|
| 79 | + | } |
|
| 80 | + | ||
| 81 | + | /// Read object capacity at the quiescent boundaries of the workload. |
|
| 82 | + | unsafe fn capacity() -> [u32; 4] { |
|
| 83 | + | return [freeSlots(&pages::STORE.slots[..]), freeSlots(&pages::STORE.backings.slots[..]), |
|
| 84 | + | freeSlots(&domains::STORE.slots[..]), freeSlots(&domains::STORE.contextSlots[..])]; |
|
| 85 | + | } |
|
| 86 | + | ||
| 87 | + | /// Copy one trusted package into bootstrap-owned memory. |
|
| 88 | + | unsafe fn input(authority: abi::Handle, bytes: &[u8]) -> abi::Handle { |
|
| 89 | + | let handle = try! pages::allocate(&mut pages::STORE, &mut TABLE, authority, (bytes.len as u64 + 4095) / 4096); |
|
| 90 | + | let page = try! pages::get(&pages::STORE, (try! capability::get(&TABLE, handle)).object); |
|
| 91 | + | assert try! mem::copy(@sliceOf(memory(page.base), page.count * 4096), bytes) == bytes.len; |
|
| 92 | + | return handle; |
|
| 93 | + | } |
|
| 94 | + | ||
| 95 | + | /// Publish fixture state before any hart enters dispatch. |
|
| 96 | + | export unsafe fn start(last: bool) { |
|
| 97 | + | if last { setup(); sync::storeRelease(&mut READY, 1); } |
|
| 98 | + | while sync::loadAcquire(&READY) == 0 {} |
|
| 99 | + | } |
|
| 100 | + | ||
| 101 | + | /// Prepare one controller per hart and a later surviving checker. |
|
| 102 | + | unsafe fn setup() { |
|
| 103 | + | let pending = try! slots::reserve(&mut domains::STORE.slots[..]); |
|
| 104 | + | let owner = try! slots::commit(&mut domains::STORE.slots[..], pending); |
|
| 105 | + | capability::initialize(&mut TABLE, owner); |
|
| 106 | + | try! backing::registerDomain(&mut pages::STORE.backings, owner); |
|
| 107 | + | let authority = try! capability::install(&mut TABLE, capability::Entry { |
|
| 108 | + | kind: abi::Kind::Domain, object: owner, rights: abi::Rights(abi::CREATE | abi::ALLOCATE), |
|
| 109 | + | }); |
|
| 110 | + | let mut image = abi::Handle(0); |
|
| 111 | + | for bytes in [&dispatchinput::support[..], &dispatchinput::spin[..]] { |
|
| 112 | + | let source = input(authority, &bytes[..]); |
|
| 113 | + | set image = try! loader::load(&mut loader::STATE, &mut pages::STORE, &mut registry::STORE, &mut TABLE, |
|
| 114 | + | loader::Request { authority, source, offset: 0, length: bytes.len as u64 }); |
|
| 115 | + | } |
|
| 116 | + | let source = input(authority, &dispatchinput::job[..]); |
|
| 117 | + | let parentHandle = try! domains::create(&mut domains::STORE, &mut pages::STORE.backings, ®istry::STORE, &mut TABLE, authority, image); |
|
| 118 | + | set PARENT = (try! capability::get(&TABLE, parentHandle)).object; |
|
| 119 | + | let parent = try! domains::get(&domains::STORE, PARENT); |
|
| 120 | + | set domains::STORE.records[PARENT.index].state = domains::Lifecycle::Active; |
|
| 121 | + | let frame = &mut domains::STORE.contexts[parent.initial.index].frame; |
|
| 122 | + | set frame.pc = completion(); set frame.status = 0x1880; |
|
| 123 | + | set frame.registers[2] = domains::STORE.contexts[parent.initial.index].kernelStack.end; |
|
| 124 | + | set frame.registers[3] = kernelGp(); |
|
| 125 | + | let mut arguments: [abi::Handle; 8] = undefined; |
|
| 126 | + | let mut handles: [abi::Handle; 8] = undefined; |
|
| 127 | + | let mut contexts: [abi::Ref; 8] = undefined; |
|
| 128 | + | let mut count: u64 = 0; |
|
| 129 | + | for hart in 0..8 { |
|
| 130 | + | if (boot::PLATFORM.harts & (1 << hart)) == 0 { continue; } |
|
| 131 | + | set count += 1; |
|
| 132 | + | set arguments[hart] = try! pages::allocate(&mut pages::STORE, &mut TABLE, authority, 1); |
|
| 133 | + | set ARGUMENTS[hart] = (try! pages::get(&pages::STORE, (try! capability::get(&TABLE, arguments[hart])).object)).base; |
|
| 134 | + | } |
|
| 135 | + | set FREE = freeFrames(); |
|
| 136 | + | set SLOTS = capacity(); |
|
| 137 | + | for hart in 0..8 { |
|
| 138 | + | if (boot::PLATFORM.harts & (1 << hart)) == 0 { continue; } |
|
| 139 | + | let handle = try! domains::create(&mut domains::STORE, &mut pages::STORE.backings, ®istry::STORE, &mut TABLE, authority, image); |
|
| 140 | + | let object = (try! capability::get(&TABLE, handle)).object; |
|
| 141 | + | let mut child = try! domains::get(&domains::STORE, object); |
|
| 142 | + | set CHILDREN[hart] = object; set handles[hart] = handle; set contexts[hart] = child.initial; |
|
| 143 | + | try! domains::reparent(&mut domains::STORE, &TABLE, handle, parentHandle); |
|
| 144 | + | let self = try! capability::install(&mut child.memory.table, capability::Entry { |
|
| 145 | + | kind: abi::Kind::Domain, object, rights: abi::Rights(abi::CREATE | abi::ALLOCATE), |
|
| 146 | + | }); |
|
| 147 | + | let stack = try! pages::allocate(&mut pages::STORE, &mut child.memory.table, self, 4); |
|
| 148 | + | let storage = try! pages::get(&pages::STORE, (try! capability::get(&child.memory.table, stack)).object); |
|
| 149 | + | let args = @sliceOf(memory(ARGUMENTS[hart]) as *mut u64, 6); |
|
| 150 | + | set args[0] = *(try! pages::grant(&mut pages::STORE, &TABLE, &mut child.memory.table, source, abi::READ as u64)); |
|
| 151 | + | set args[1] = dispatchinput::job.len as u64; |
|
| 152 | + | for i in 0..devices::STORE.count { |
|
| 153 | + | if devices::STORE.regions[i].kind == platform::Kind::Clint { |
|
| 154 | + | set args[2] = *(try! devices::install(&devices::STORE, &mut child.memory.table, i)); |
|
| 155 | + | } |
|
| 156 | + | } |
|
| 157 | + | assert args[2] <> 0; |
|
| 158 | + | set args[3] = *(try! pages::grant(&mut pages::STORE, &TABLE, &mut child.memory.table, arguments[hart], (abi::READ | abi::WRITE | abi::GRANT) as u64)); |
|
| 159 | + | set args[4] = 10000000 * count; |
|
| 160 | + | try! domains::activate(&mut domains::STORE, &pages::STORE, &TABLE, handle, storage.base + storage.count as u64 * 4096, ARGUMENTS[hart], 56); |
|
| 161 | + | } |
|
| 162 | + | for byte in "cycles controllers ready\n" { put(byte); } |
|
| 163 | + | let now = dispatch::clock(); |
|
| 164 | + | let start = now + 1000000 * count; |
|
| 165 | + | for hart in 0..8 { |
|
| 166 | + | if (boot::PLATFORM.harts & (1 << hart)) == 0 { continue; } |
|
| 167 | + | let window = try! budgets::seed(&mut budgets::STORE, &mut TABLE, hart, start, 0xffffffffffffffff); |
|
| 168 | + | let tail = try! budgets::split(&mut budgets::STORE, &mut TABLE, window, start + 800000000 * count, now); |
|
| 169 | + | let bound = try! budgets::bind(&mut budgets::STORE, &domains::STORE, &mut TABLE, |
|
| 170 | + | budgets::Binding { budget: window, domain: handles[hart], context: contexts[hart] }, now); |
|
| 171 | + | if hart == 0 { |
|
| 172 | + | let final = try! budgets::bind(&mut budgets::STORE, &domains::STORE, &mut TABLE, |
|
| 173 | + | budgets::Binding { budget: tail, domain: parentHandle, context: parent.initial }, now); |
|
| 174 | + | } |
|
| 175 | + | } |
|
| 176 | + | } |
|
| 177 | + | ||
| 178 | + | /// Check all terminal records, shared code identity, and complete transient recovery. |
|
| 179 | + | export unsafe fn verify() { |
|
| 180 | + | for byte in "cycles checking completion\n" { put(byte); } |
|
| 181 | + | let guard = sync::enter(); |
|
| 182 | + | let mut parent = try! domains::get(&domains::STORE, PARENT); |
|
| 183 | + | let job = registry::find(®istry::STORE, &"job"[..]) else panic "worker package required"; |
|
| 184 | + | let package = try! registry::get(®istry::STORE, job); |
|
| 185 | + | let mut seen: u64 = 0; |
|
| 186 | + | while let event = try! events::pop(&mut parent.memory.ring) { |
|
| 187 | + | assert event.kind == events::CHILD_EXIT and event.code == 68; |
|
| 188 | + | let mut found = false; |
|
| 189 | + | for hart in 0..8 { |
|
| 190 | + | if (boot::PLATFORM.harts & (1 << hart)) == 0 { continue; } |
|
| 191 | + | if event.value == abi::id(CHILDREN[hart]) { |
|
| 192 | + | assert (seen & (1 << hart)) == 0; |
|
| 193 | + | set seen |= 1 << hart; set found = true; |
|
| 194 | + | let args = @sliceOf(memory(ARGUMENTS[hart]) as *mut u64, 7); |
|
| 195 | + | assert args[5] == package.codeAddress and args[6] == 4; |
|
| 196 | + | } |
|
| 197 | + | } |
|
| 198 | + | assert found; |
|
| 199 | + | } |
|
| 200 | + | assert seen == boot::PLATFORM.harts; |
|
| 201 | + | try! events::refresh(&mut domains::STORE.events, PARENT, &parent.memory.ring); |
|
| 202 | + | assert loader::STATE.live[job.index] and not loader::STATE.busy; |
|
| 203 | + | let retained = loader::STATE.resident[job.index].code.count + loader::STATE.resident[job.index].metadata.count; |
|
| 204 | + | sync::leave(guard); |
|
| 205 | + | let mut done = false; |
|
| 206 | + | for attempt in 0..100000 { |
|
| 207 | + | let guard = sync::enter(); |
|
| 208 | + | set done = domains::STORE.dead == 0 and pages::STORE.backings.pool.retiredCount == 0; |
|
| 209 | + | if done { sync::leave(guard); break; } |
|
| 210 | + | let request = try! dispatch::request(0, remote::Action::Reschedule); |
|
| 211 | + | sync::leave(guard); |
|
| 212 | + | assert try! dispatch::awaitRequest(0, request) == 0; |
|
| 213 | + | } |
|
| 214 | + | assert done; |
|
| 215 | + | assert freeFrames() + retained == FREE; |
|
| 216 | + | let recovered = capacity(); |
|
| 217 | + | for i in 0..4 { assert recovered[i] == SLOTS[i]; } |
|
| 218 | + | invariants::check(&TABLE); |
|
| 219 | + | for byte in "cycles final recovery and invariants passed\n" { put(byte); } |
|
| 220 | + | let maximum = sync::maximum(); |
|
| 221 | + | assert maximum > 0 and maximum < 1000000; |
|
| 222 | + | for byte in "cycles metadata instructions: " { put(byte); } |
|
| 223 | + | number(maximum); |
|
| 224 | + | put(10); |
|
| 225 | + | let waiting = sync::maximumWait(); |
|
| 226 | + | assert waiting > 0; |
|
| 227 | + | for byte in "cycles acquisition instructions: " { put(byte); } |
|
| 228 | + | number(waiting); |
|
| 229 | + | put(10); |
|
| 230 | + | finish(); |
|
| 231 | + | } |
|
| 232 | + | ||
| 233 | + | /// Write a fixed-width diagnostic value. |
|
| 234 | + | fn number(value: u64) { |
|
| 235 | + | let digits = "0123456789abcdef"; |
|
| 236 | + | for i in 0..16 { put(digits[((value >> ((15 - i) as u64 * 4)) & 15) as u32]); } |
|
| 237 | + | } |
test/cycles/machine.ras
added
+31 -0
| 1 | + | //! Start all initialized harts after the fixture publishes its shared domains. |
|
| 2 | + | .text; |
|
| 3 | + | call @kernel::boot::initialize; |
|
| 4 | + | call @kernel::dispatchcheck::start; |
|
| 5 | + | call @kernel::boot::run; |
|
| 6 | + | ebreak; |
|
| 7 | + | .export @kernel::dispatchcheck::memory; |
|
| 8 | + | .export @kernel::dispatchcheck::kernelGp; |
|
| 9 | + | .export @kernel::dispatchcheck::completion; |
|
| 10 | + | .export @kernel::dispatchcheck::finish; |
|
| 11 | + | .export @kernel::dispatchcheck::put; |
|
| 12 | + | @kernel::dispatchcheck::memory |
|
| 13 | + | ret; |
|
| 14 | + | @kernel::dispatchcheck::kernelGp |
|
| 15 | + | mv %a0 %gp; |
|
| 16 | + | ret; |
|
| 17 | + | @kernel::dispatchcheck::completion |
|
| 18 | + | la %a0 @complete; |
|
| 19 | + | ret; |
|
| 20 | + | @complete |
|
| 21 | + | call @kernel::dispatchcheck::verify; |
|
| 22 | + | ebreak; |
|
| 23 | + | @kernel::dispatchcheck::put |
|
| 24 | + | li %t0 0x10000000; |
|
| 25 | + | sb %a0 0(%t0); |
|
| 26 | + | ret; |
|
| 27 | + | @kernel::dispatchcheck::finish |
|
| 28 | + | li %t0 0x10001000; |
|
| 29 | + | li %t1 0x5555; |
|
| 30 | + | sw %t1 0(%t0); |
|
| 31 | + | ebreak; |
test/cycles/run
added
+42 -0
| 1 | + | #!/bin/sh |
|
| 2 | + | # Compile a dependency, controllers, and a worker loaded after dispatch starts. |
|
| 3 | + | set -eu |
|
| 4 | + | emulator=${RAD_EMULATOR:-emulator} |
|
| 5 | + | harts=${1:-1 2 8} |
|
| 6 | + | work=$(mktemp -d) |
|
| 7 | + | trap 'rm -rf "$work"' EXIT HUP INT TERM |
|
| 8 | + | for package in spin job; do |
|
| 9 | + | mkdir "$work/$package" |
|
| 10 | + | cp "test/cycles/$package.rad" "$work/$package.rad" |
|
| 11 | + | cp kernel/kernel/abi.rad kernel/kernel/sys.rad "$work/$package/" |
|
| 12 | + | set -- -pkg support -mod test/cycles/support.rad -pkg "$package" -mod "$work/$package.rad" \ |
|
| 13 | + | -mod "$work/$package/abi.rad" -mod "$work/$package/sys.rad" |
|
| 14 | + | if [ "$package" = spin ]; then |
|
| 15 | + | cp kernel/mmio.rad "$work/spin/" |
|
| 16 | + | set -- "$@" -mod "$work/spin/mmio.rad" |
|
| 17 | + | fi |
|
| 18 | + | "$emulator" -memory-size=385024 -data-size=348160 -stack-size=1024 -run bin/radiance.rv64.dev "$@" -entry "$package" -ril "$work" |
|
| 19 | + | done |
|
| 20 | + | mkdir "$work/kernel" |
|
| 21 | + | cp kernel/kernel.rad "$work/kernel.rad" |
|
| 22 | + | printf '\nexport mod dispatchcheck;\nexport mod dispatchinput;\nexport mod invariants;\n' >> "$work/kernel.rad" |
|
| 23 | + | cp kernel/kernel/*.rad "$work/kernel/" |
|
| 24 | + | cp test/cycles/kernel/dispatchcheck.rad test/smp/kernel/invariants.rad "$work/kernel/" |
|
| 25 | + | for package in support spin job; do |
|
| 26 | + | length=$(wc -c < "$work/$package.ril") |
|
| 27 | + | printf '/// Complete trusted %s package.\nexport static %s: [u8; %s] = [\n' "$package" "$package" "$length" >> "$work/kernel/dispatchinput.rad" |
|
| 28 | + | od -An -v -tu1 "$work/$package.ril" | awk '{ for (i = 1; i <= NF; i++) printf "%s,", $i; print "" }' >> "$work/kernel/dispatchinput.rad" |
|
| 29 | + | printf '];\n' >> "$work/kernel/dispatchinput.rad" |
|
| 30 | + | done |
|
| 31 | + | sh test/acceptance/compile "$emulator" "$work" |
|
| 32 | + | cat test/cycles/machine.ras kernel/kernel/*.ras > "$work/cycles.ras" |
|
| 33 | + | "$emulator" -memory-size=385024 -data-size=348160 -stack-size=1024 -run bin/kernel.build.rv64 \ |
|
| 34 | + | -- "$work/std.ril" "$work/kernel.ril" "$work/cycles.ras" "$work/cycles.rv64" |
|
| 35 | + | for count in $harts; do |
|
| 36 | + | if [ "${KERNEL_REPLAY:-0}" = 1 ]; then |
|
| 37 | + | sh test/acceptance/replay cycles "$emulator" "$work/cycles.rv64" "$count" -max-steps=10000000000 |
|
| 38 | + | else |
|
| 39 | + | "$emulator" -machine -harts="$count" -memory-size=262144 -max-steps=10000000000 -run "$work/cycles.rv64" |
|
| 40 | + | fi |
|
| 41 | + | printf 'cycles: %s-hart load, spawn, yield, fault, and recovery passed\n' "$count" |
|
| 42 | + | done |
test/cycles/spin.rad
added
+108 -0
| 1 | + | //! Concurrent load, spawn, yield, fault, and teardown cycles. |
|
| 2 | + | use support; |
|
| 3 | + | export mod abi; |
|
| 4 | + | export mod sys; |
|
| 5 | + | export mod mmio; |
|
| 6 | + | ||
| 7 | + | /// Ordered shared-memory access boundary for the single event consumer. |
|
| 8 | + | @intrinsic fn memoryFence(); |
|
| 9 | + | ||
| 10 | + | /// Controller resources and retained completion metadata. |
|
| 11 | + | record Arguments: Copy { |
|
| 12 | + | /// Readable binary worker package. |
|
| 13 | + | source: abi::Handle, |
|
| 14 | + | /// Exact package byte length. |
|
| 15 | + | length: u64, |
|
| 16 | + | /// Read-only clock capability. |
|
| 17 | + | clock: abi::Handle, |
|
| 18 | + | /// Page that owns this argument record. |
|
| 19 | + | page: abi::Handle, |
|
| 20 | + | /// Reserved worker interval in clock ticks. |
|
| 21 | + | quantum: u64, |
|
| 22 | + | /// Shared worker code base reported to the checker. |
|
| 23 | + | codeBase: u64, |
|
| 24 | + | /// Number of fully checked worker lifetimes. |
|
| 25 | + | completed: u64, |
|
| 26 | + | } |
|
| 27 | + | ||
| 28 | + | /// Published event wire record. |
|
| 29 | + | record Event: Copy { |
|
| 30 | + | /// Notification kind. |
|
| 31 | + | kind: u16, |
|
| 32 | + | /// Reserved zero bits. |
|
| 33 | + | reserved: u16, |
|
| 34 | + | /// Terminal status or fault code. |
|
| 35 | + | code: u32, |
|
| 36 | + | /// Generation-bearing child identity. |
|
| 37 | + | value: u64, |
|
| 38 | + | } |
|
| 39 | + | ||
| 40 | + | /// Shared single-consumer event ring. |
|
| 41 | + | record Ring: Copy { |
|
| 42 | + | /// Published event slots. |
|
| 43 | + | data: [Event; 256], |
|
| 44 | + | /// Consumer progress. |
|
| 45 | + | head: u32, |
|
| 46 | + | /// Producer progress. |
|
| 47 | + | tail: u32, |
|
| 48 | + | /// Ring index mask. |
|
| 49 | + | mask: u32, |
|
| 50 | + | } |
|
| 51 | + | ||
| 52 | + | /// Kernel startup pointers for one controller. |
|
| 53 | + | record Env: Copy { |
|
| 54 | + | /// Writable arguments retained by the parent. |
|
| 55 | + | argsPointer: *unsafe mut Arguments, |
|
| 56 | + | /// Argument record byte size. |
|
| 57 | + | argsSize: u64, |
|
| 58 | + | /// Installed event capability. |
|
| 59 | + | eventsHandle: u64, |
|
| 60 | + | /// Shared event-ring pointer. |
|
| 61 | + | eventsPointer: *unsafe mut Ring, |
|
| 62 | + | } |
|
| 63 | + | ||
| 64 | + | /// Repeat publication lookup and private worker lifetimes on this hart. |
|
| 65 | + | @default unsafe fn main(env: *Env) { |
|
| 66 | + | assert env.argsSize == @sizeOf(Arguments) as u64; |
|
| 67 | + | let mut args = env.argsPointer; |
|
| 68 | + | let initial = sys::currentContext(); |
|
| 69 | + | for turn in 0..4 { |
|
| 70 | + | assert support::advance() == turn as u64 + 1; |
|
| 71 | + | let mut image = abi::Handle(0); |
|
| 72 | + | while image == abi::Handle(0) { |
|
| 73 | + | set image = try sys::imageLoad(abi::Handle(0), args.source, 0, args.length) catch error { |
|
| 74 | + | assert error == abi::Error::Busy; |
|
| 75 | + | continue; |
|
| 76 | + | }; |
|
| 77 | + | } |
|
| 78 | + | let loaded = try! sys::queryImage(image); |
|
| 79 | + | if turn == 0 { set args.codeBase = loaded.codeBase; } |
|
| 80 | + | assert loaded.codeBase == args.codeBase; |
|
| 81 | + | let child = try! sys::domainCreate(abi::Handle(0), image); |
|
| 82 | + | let identity = sys::queryDomain(child).id; |
|
| 83 | + | let stack = try! sys::pageAllocate(abi::Handle(0), 4); |
|
| 84 | + | let extent = sys::queryPage(stack); |
|
| 85 | + | let moved = try! sys::capabilityTransfer(stack, child, abi::RIGHTS_MASK as u64); |
|
| 86 | + | let shared = try! sys::capabilityGrant(args.page, child, abi::READ as u64); |
|
| 87 | + | try! sys::domainActivate(child, extent.base + extent.count * 4096, args as *unsafe opaque, (turn % 2) as u64); |
|
| 88 | + | let current = sys::currentContext(); |
|
| 89 | + | assert current.context == initial.context and current.hart == initial.hart; |
|
| 90 | + | let later = try! sys::budgetSplit(abi::Handle(current.budget), mmio::read64(args.clock, 0) + args.quantum); |
|
| 91 | + | try! sys::yield(child); |
|
| 92 | + | assert sys::currentContext().budget == *later; |
|
| 93 | + | let mut ring = env.eventsPointer; |
|
| 94 | + | let head = ring.head; |
|
| 95 | + | let tail = ring.tail; |
|
| 96 | + | memoryFence(); |
|
| 97 | + | assert head <> tail and ring.mask == 255; |
|
| 98 | + | let event = ring.data[head & ring.mask]; |
|
| 99 | + | assert event.value == identity and event.reserved == 0; |
|
| 100 | + | if turn % 2 == 0 { assert event.kind == 4 and event.code == 9; } |
|
| 101 | + | else { assert event.kind == 3 and event.code == 3; } |
|
| 102 | + | memoryFence(); |
|
| 103 | + | set ring.head = head + 1; |
|
| 104 | + | try! sys::capabilityDrop(image); |
|
| 105 | + | set args.completed = turn as u64 + 1; |
|
| 106 | + | } |
|
| 107 | + | sys::exit(68); |
|
| 108 | + | } |
test/cycles/support.rad
added
+9 -0
| 1 | + | //! Shared library code with private state in each domain graph. |
|
| 2 | + | /// Per-instance invocation count. |
|
| 3 | + | static COUNT: u64 = 0; |
|
| 4 | + | ||
| 5 | + | /// Advance this domain's private library state. |
|
| 6 | + | export fn advance() -> u64 { |
|
| 7 | + | set COUNT += 1; |
|
| 8 | + | return COUNT; |
|
| 9 | + | } |
test/runtime/kernel/dispatchcheck.rad
+8 -0
| 129 | 129 | ||
| 130 | 130 | /// Verify cancellation, competing admission, progress, and resident code reuse. |
|
| 131 | 131 | export unsafe fn verify() { |
|
| 132 | 132 | for byte in "runtime admission metadata instructions: " { put(byte); } |
|
| 133 | 133 | number(sync::maximum()); put(10); |
|
| 134 | + | let admissionWait = sync::maximumWait(); |
|
| 135 | + | assert admissionWait > 0; |
|
| 136 | + | for byte in "runtime admission acquisition instructions: " { put(byte); } |
|
| 137 | + | number(admissionWait); put(10); |
|
| 134 | 138 | let progress = @sliceOf(PROGRESS, 4); |
|
| 135 | 139 | let guard = sync::enter(); |
|
| 136 | 140 | let first = CONTEXTS[0]; |
|
| 137 | 141 | for byte in "runtime first progress and owner: " { put(byte); } |
|
| 138 | 142 | number(progress[0]); put(32); number(abi::id(loader::STATE.owner)); put(10); |
| 210 | 214 | for byte in "runtime retry published executable code\n" { put(byte); } |
|
| 211 | 215 | let maximum = sync::maximum(); |
|
| 212 | 216 | for byte in "runtime metadata instructions: " { put(byte); } |
|
| 213 | 217 | number(maximum); put(10); |
|
| 214 | 218 | assert maximum > 0 and maximum < 1000000; |
|
| 219 | + | let waiting = sync::maximumWait(); |
|
| 220 | + | assert waiting > 0; |
|
| 221 | + | for byte in "runtime acquisition instructions: " { put(byte); } |
|
| 222 | + | number(waiting); put(10); |
|
| 215 | 223 | finish(); |
|
| 216 | 224 | } |
test/smp/kernel/dispatchcheck.rad
+8 -0
| 1 | 1 | //! One domain executing separate user contexts on every online hart. |
|
| 2 | 2 | use std::mem; |
|
| 3 | 3 | use std::arch::rv64::shared; |
|
| 4 | 4 | use kernel::abi; |
|
| 5 | + | use kernel::invariants; |
|
| 5 | 6 | use kernel::frames; |
|
| 6 | 7 | use kernel::slots; |
|
| 7 | 8 | use kernel::backing; |
|
| 8 | 9 | use kernel::pages; |
|
| 9 | 10 | use kernel::capability; |
| 276 | 277 | expiredCall(); |
|
| 277 | 278 | if (boot::PLATFORM.harts & 2) <> 0 { idleWakeup(); } |
|
| 278 | 279 | interruptOwnership(); |
|
| 279 | 280 | interruptStorm(); |
|
| 280 | 281 | if (boot::PLATFORM.harts & 2) <> 0 { terminalWakeup(); cancelAllocation(); reclaimedDomains(); } |
|
| 282 | + | invariants::check(&TABLE); |
|
| 283 | + | for byte in "smp final ownership and interval invariants passed\n" { put(byte); } |
|
| 281 | 284 | let maximum = sync::maximum(); |
|
| 282 | 285 | assert maximum > 0 and maximum < 1000000; |
|
| 283 | 286 | for byte in "smp metadata instructions: 0x" { put(byte); } |
|
| 284 | 287 | number(maximum); |
|
| 285 | 288 | put(10); |
|
| 289 | + | let waiting = sync::maximumWait(); |
|
| 290 | + | assert waiting > 0; |
|
| 291 | + | for byte in "smp acquisition instructions: 0x" { put(byte); } |
|
| 292 | + | number(waiting); |
|
| 293 | + | put(10); |
|
| 286 | 294 | finish(); |
|
| 287 | 295 | } |
|
| 288 | 296 | ||
| 289 | 297 | /// Validate elapsed authority against the current clock at the serialized boundary. |
|
| 290 | 298 | unsafe fn expiredCall() { |
test/smp/kernel/invariants.rad
added
+73 -0
| 1 | + | //! Final ownership and interval checks over published kernel objects. |
|
| 2 | + | use kernel::abi; |
|
| 3 | + | use kernel::boot; |
|
| 4 | + | use kernel::slots; |
|
| 5 | + | use kernel::capability; |
|
| 6 | + | use kernel::domains; |
|
| 7 | + | use kernel::budgets; |
|
| 8 | + | use kernel::interrupts; |
|
| 9 | + | use kernel::sync; |
|
| 10 | + | ||
| 11 | + | /// Select authoritative capability storage, including the fixture's boot owner. |
|
| 12 | + | /// The bootstrap table and domain memory must outlive the metadata transaction. |
|
| 13 | + | unsafe fn table(owner: abi::Ref, bootstrap: &capability::Table) -> *unsafe capability::Table { |
|
| 14 | + | if owner == bootstrap.owner { return bootstrap as *unsafe capability::Table; } |
|
| 15 | + | let domain = try! domains::get(&domains::STORE, owner); |
|
| 16 | + | assert domain.state <> domains::Lifecycle::Dead; |
|
| 17 | + | assert domain.memory.table.owner == owner; |
|
| 18 | + | return &domain.memory.table; |
|
| 19 | + | } |
|
| 20 | + | ||
| 21 | + | /// Check live references, exclusive execution ownership, and disjoint CPU windows. |
|
| 22 | + | /// Each budget or IRQ check uses a separate bounded metadata transaction. |
|
| 23 | + | export unsafe fn check(bootstrap: &capability::Table) { |
|
| 24 | + | let guard = sync::enter(); |
|
| 25 | + | let mut occupied: u32 = 0; |
|
| 26 | + | for i in 0..domains::STORE.contextSlots.len { |
|
| 27 | + | if domains::STORE.contextSlots[i].state <> slots::State::Live { continue; } |
|
| 28 | + | let context = domains::STORE.contexts[i]; |
|
| 29 | + | let owner = try! domains::get(&domains::STORE, context.owner); |
|
| 30 | + | assert owner.state <> domains::Lifecycle::Dead; |
|
| 31 | + | if let hart = context.hart { |
|
| 32 | + | assert hart < 8 and (boot::PLATFORM.harts & (1 << hart)) <> 0; |
|
| 33 | + | assert (occupied & (1 << hart)) == 0; |
|
| 34 | + | set occupied |= 1 << hart; |
|
| 35 | + | } |
|
| 36 | + | } |
|
| 37 | + | sync::leave(guard); |
|
| 38 | + | for i in 0..budgets::STORE.slots.len { |
|
| 39 | + | let guard = sync::enter(); |
|
| 40 | + | if budgets::STORE.slots[i].state == slots::State::Live { |
|
| 41 | + | let object = abi::Ref { index: i, generation: budgets::STORE.slots[i].generation }; |
|
| 42 | + | let window = try! budgets::get(&budgets::STORE, object); |
|
| 43 | + | assert window.start < window.end and window.hart < 8; |
|
| 44 | + | assert (boot::PLATFORM.harts & (1 << window.hart)) <> 0; |
|
| 45 | + | let owner = table(window.owner, bootstrap); |
|
| 46 | + | let entry = try! capability::get(&*owner, window.handle); |
|
| 47 | + | assert entry.kind == abi::Kind::Budget and entry.object == object; |
|
| 48 | + | if let context = window.context { |
|
| 49 | + | let bound = try! domains::context(&domains::STORE, window.owner, context); |
|
| 50 | + | assert bound.owner == window.owner; |
|
| 51 | + | } |
|
| 52 | + | for j in i + 1..budgets::STORE.slots.len { |
|
| 53 | + | if budgets::STORE.slots[j].state <> slots::State::Live { continue; } |
|
| 54 | + | let other = budgets::STORE.windows[j]; |
|
| 55 | + | if other.hart == window.hart { |
|
| 56 | + | assert window.end <= other.start or other.end <= window.start; |
|
| 57 | + | } |
|
| 58 | + | } |
|
| 59 | + | } |
|
| 60 | + | sync::leave(guard); |
|
| 61 | + | } |
|
| 62 | + | for i in 0..interrupts::STORE.count { |
|
| 63 | + | let guard = sync::enter(); |
|
| 64 | + | if interrupts::STORE.slots[i].state == slots::State::Live { |
|
| 65 | + | let object = abi::Ref { index: i, generation: interrupts::STORE.slots[i].generation }; |
|
| 66 | + | let irq = try! interrupts::get(&interrupts::STORE, object); |
|
| 67 | + | let owner = table(irq.owner, bootstrap); |
|
| 68 | + | let entry = try! capability::get(&*owner, irq.handle); |
|
| 69 | + | assert entry.kind == abi::Kind::Interrupt and entry.object == object; |
|
| 70 | + | } |
|
| 71 | + | sync::leave(guard); |
|
| 72 | + | } |
|
| 73 | + | } |