Memory

Memory is a capability#

A Kore program never handles a physical address. Physical memory reaches it only as capabilities, each derived from the one before:

A mapping is a derived capability, so taking one away is an ordinary revoke of that leaf, and revoking the lease takes every mapping beneath it with it. Every lease's backing is zeroed when the lease is derived, whether its frames are fresh or reused, so no program reads what another left behind.

Asking for memory#

Most programs get memory from the memory service, the lessor, rather than from the kernel directly. It answers four verbs:

Alloc states requirements, not placements. AllocProps is 24 bytes, and the memory service's request carries the same fields:

The kernel's placement policy picks the backing that satisfies them: memory near the requesting CPU, within the device's DMA reach, contiguous if asked.

Leases#

A lease is carved from a region with LeaseReq (16 bytes):

• Alignment is about page size. A backing aligned to 2 MiB or 1 GiB lets each later mapping use large pages, so a DMA pool can ride one 2 MiB TLB entry instead of 512 small ones. It's a placement request only: it doesn't round the size or promise large pages by itself.
• LEASE_SEALED makes the lease swappable but sealed. When a page is evicted, the kernel encrypts and authenticates it under its own key, so neither the lessor nor the swap backend ever sees plaintext or can alter it undetected. It's opt-in per lease, because sealed pages don't compress.
• LEASE_EXEC asks for an executable lease; see executable memory.

A lease has one owner and can be mapped into several address spaces and device domains at once, all over the same frames: sharing memory never copies it. Revoking the lease unmaps it everywhere and frees it exactly once.

Mapping#

Into your own address space#

ShareReq (24 bytes) installs a lease in the caller's own space:

Write and execute together are refused in one request, and execute is honored only on an executable lease. The user/supervisor bit is never on the wire: the kernel derives it from the target address space. DERIVE_KIND_OWNED_MAP maps a whole lease at a kernel-chosen address and keeps the installed mapping as a capability.

A stack takes RegionMapReq instead. The caller names the virtual window and how many guard pages to leave below and above it; the kernel allocates the backing and installs the map with the gaps.

Views handed to you#

A lessor often has no handle to its client's address space. So it carves a detached view off a lease it holds, with WindowCarveReq (a page-aligned offset and length inside the lease), and hands the view over. The view is geometry only: nothing is mapped yet.

The receiver installs it with VIEW_MAP (ViewMapReq, 8 bytes) into one of the windows its address-space geometry was stamped with:

The request carries no address, length, destination or access mask. Each one comes from the receiver's stamped geometry and the authenticated view, so a client can't be talked into mapping something somewhere it didn't plan for. With VIEW_MAP_SINK, a view in the MAP window that reads a client-funded ring asynchronously survives its lessor: if the lease dies, its pages are pointed at a sink page instead of unmapped, so the reader sees meaningless bytes rather than a fault.

Narrowing a mapping#

PROTECT clears read, write or execute bits on a range of the caller's own space. It can only take rights away, never add them.

Executable memory#

Memory is writable or executable, never both, and the rule holds above the page tables rather than only in them:

• On the wire. A share that asks for write and execute together is refused.
• Executable leases. LEASE_EXEC is honored only for a task that holds a live ExecMint capability, which only the image service is given. Its shares may be executable, and writable shares of it are refused for good.
• Writable to executable. An ordinary lease becomes executable only through the EXEC revoke, which removes every writable alias first. EXEC_RETURN makes it writable again, for JIT code reuse.

Giving memory back#

The revoke flavors are memory's lifecycle:

• Plain revoke retires a capability, and everything derived from it goes with it.
• UNMAP retires a mapping and hands back the bare physical extent.
• PAGED is the lessor's eviction: the mapping goes, but paged-out markers stay, so the tenant's next touch reaches its space's pager instead of faulting hard.
• RETURN is the lessor taking a view back. Every CPU mapping of that window, by any receiver in any space, is removed, and the kernel reports the window's extent itself, so the lessor re-pools a range that is provably unaliased, never one a client claimed.
• UNSHARE removes exactly one mapping of a lease.

Memory a device reads and writes is a lease too, mapped into the device's IOMMU domain instead of an address space. That side is on Devices.