The kernel · L2

Capabilities

In sysk, the right to do something is a value you hold. A task can print, send, receive or touch a device only through a value it was handed, and the type checker makes sure nobody can make one they were not meant to have.

A capability is a value with no data

Most operating systems check permissions when you ask: a task names a file or a device and the kernel looks up whether it may. sysk has no names to look up. To write to the console you need a Console; to stop the machine, a Halt. These are sysp structs with no fields, declared private:

; kernel/caps.sysp
(private struct Root)
(private struct Console)
(private struct Halt)

(fn console ((root Root)) Console (effects) (new Console))
(fn halt ((h Halt) (code i64)) never (effects io) (requires (and (<= 0 code) (<= code 255))) (machine-exit code))

private means only code in kernel/caps.sysp can write (new Console). Everyone else can only receive one, as an argument, from someone who has one. A function's parameters are therefore a complete list of what it can do. The hardware externs (uart-put, machine-exit) are private too, so there is no way around the values.

Where every capability comes from

There are two sources. boot.S hands kmain the only Root, from which the kernel derives its Console and Halt. task-main holds the only Wire, the right to wire the system: with it, the generated code mints each task's channel handles and its device. Select a task to see what it holds.

Handles are resources

Channel handles, Tx and Rx, are capabilities with data: which channel, how many messages are left, how many bytes each. They are resource structs, which sysp treats like buffers: each has exactly one owner, it cannot be copied (O001), and it cannot be dropped (O002). The only way to be rid of one is close-tx or close-rx, which require that no messages are left. So a task that walks away from a conversation halfway does not compile. See Channels.

Devices are capabilities too

A device is a Device, a private struct in kernel/devices.sysp with one field: the base of the device's 4096-byte page of registers (sysk 023; before, the UART was a fieldless Uart). Only device makes one, and it takes a Wire, so only the generated wiring can, with the base arch/rv64/devices.sysk gives. The manifest hands it to one task with (device uart) or (device virtio-blk), and the hardware agrees: only that task's PMP regions include the page. The field is private, so a driver cannot read or change it; it reaches the page only through mmio-read8, mmio-read32, mmio-write8 and mmio-write32, whose contracts prove each offset inside the page. Holding the Device is also what lets a task acknowledge its interrupt (device-ack takes it), and the kernel completes only the claim it holds for the caller's own device. See IO and drivers. A device that reads and writes memory itself, the disk, is held to memory its driver lent it by two more resources, Queue and Lent: see Storage.

The right to start jobs

Jobs (sysk 017) is a resource too, minted by the wiring for the one task the manifest names as launcher. Judging a job consumes it and starting the job turns it into the job's output end; only ending the job, once that output is drained, gives it back. So a launcher holds at most one job, and a task without it cannot start any: what the launcher can hand a job is only the pool, never a device or another task's channel. See Jobs.

Serving jobs

Service (sysk 031) is the right to serve a pool service: its holder, the one task the manifest hands (serves NAME), gets the server's ends of the service's two streams while a job that binds them runs, a lease at a time, and must close the lease when the job's requests end. Like Jobs, it keeps where its holder is in that protocol, and like a handle it must be got rid of (service-end). See Files for jobs.

Reading the kernel

Sys (sysk 028) is the right to read the kernel's tree of files: its tasks, its channels, the time. Fieldless, private to kernel/files.sysp, made only with a Wire for the tasks the manifest hands (sys); like a Clock, any number of tasks may hold one. What it lets a task do is narrow: ask sys-serve, which answers in one atomic block and writes nothing but that task's own fids. See Files.

Try to forge one

Each of these is a test that must fail to compile.