Memory
sysk uses no MMU, so every address means the same thing to everyone. sysk divides that one address space by rule: each task owns a stack and a heap, the kernel owns everything else, and messages are copied between them so no task ever touches another's memory.
The map
Where everything is in the image the last make docs built, lowest address first, read from the ELF's symbol table. RAM starts at 0x8000_0000; the devices sit at fixed addresses below it.
| Address | Region | Size | Size, log scale | Who may touch it |
|---|
Where it comes from: arch/rv64/link.ld places code, constants, data and .bss; ctx.S reserves the stacks; the boot arena runs from the end of .bss to 0x8400_0000, half of the 128 MiB; the upper half is unused. Code, constants and stacks start on whole pages: QEMU caches PMP checks only for those, and tasks ran three times slower before.
Three kinds of memory
- Stacks. Each task has two of bytes: a user stack it runs on, and a kernel stack its traps and system calls run on. Up to tasks (8 before sysk 027), so twice as many stacks are reserved in
.bss. - The boot arena.
sysp_allocinalloc.Sis a bump allocator: it hands out zeroed, 16-byte aligned memory and never takes any back. The kernel uses it while booting, for its own tables and for the words of every task's heap. After the first task starts nothing calls it again, and sysp proves that: no function reachable fromtask-mainor the timer has thealloceffect. - A heap per task. The manifest gives each task a heap size,
(heap 128): 128 bytes of blocks. At boot the kernel allocates that many bytes of words, plus nine words for the free-list heads, and hands them to the task, which makes its own heap from them. The allocator is ordinary sysp, running inside the task.
Inside a task's heap
A heap is a buffer of 64-bit words. The first nine are the heads of nine free lists, one per size class; blocks come after them. A bump pointer marks how far blocks have ever been handed out. To allocate, the heap takes a block from its class's free list if there is one, otherwise from above the bump pointer. Freeing puts the block at the front of its class's list.
alloc and dealloc in kernel/heap.sysp. An allocation the heap could not satisfy is refused here; in sysk, it would not compile, because alloc requires (can-alloc h n).A job slot (sysk 017) runs one program after another in the same heap. Between them its runner calls heap-renew, which empties every free list and puts the bump pointer back: the heap as heap-new made it, so the next program's heap-budget holds. Only the generated runner names it, at a point where no block is in use; see Jobs.
What sysp proves about it
- Every index is in bounds. Free-list heads, links and block offsets are all array indices, and each is proven to be inside the words.
- A block comes back zeroed:
allocensures(zeroed result), so no task sees what was in a block before. - The heap is a budget.
allocrequires(can-alloc h n). A task states up front what all its allocations need, as(heap-budget h 10): ten words of room, enough for an 8-byte message (2 words) and a 64-byte line (8 words). If the manifest gives it a heap that is too small, the system does not compile. - A freed buffer cannot be used.
dealloctakes the buffer, and buffers are linear, so using it afterwards is an ownership error (O001).
Two primitives are trusted. sysp has no pointer arithmetic, so block_view (a block of words seen as bytes) and block_offset (a buffer back to its block) are assembly, in arch/rv64/heap.S. block_offset checks the buffer is word-aligned, lies among this heap's blocks and is no longer than its class, and stops the machine (status 2) if not. That a buffer starts on a block is an assumption, listed in docs/trusted.md: only block_view makes buffers inside a heap. The allocator also checks a free-list link before it follows it, so a task scribbling over a block it still holds cannot make its heap hand out memory outside its words.