Sessions: the authority plane

Three verbs#

The whole authority vocabulary is three op-codes:

Code 3 is retired and refused; it will never be reused. There is no read, write, map or call primitive. Mapping memory, spawning a task, killing one, programming an interrupt and notifying a peer are each one of the three, with a flavor selected by the operation's kind byte and the kind of resource it acts on.

A session#

A session is a batch of operations the kernel commits as one transaction, in one trap:

1. Validate. Every operation is checked against the caller's arena: bounds, vacancy, resource kind, rights and the holder stamp.
2. Prepare. The batch is folded without side effects.
3. Commit. All of it applies, or none of it does, with a single revocation pass for the whole batch.
4. Write back. Results land in the caller's arena slots, and the return word reports the status and, on refusal, the index of the operation that failed.

Operations can name the results of earlier operations in the same session by slot, so a session reads like straight-line code over slots. A forward reference is Malformed. Building a process — its address space, pages and capabilities — is one session, which ends by founding it. A founded process is dormant; starting it is a second session, a TASK_START on the returned handle.

Commits are optimistic: two sessions whose capability footprints don't overlap commit in parallel, and a lost race reports Conflict, which means retry.

The descriptor#

All fields are little-endian and readable at any byte offset.

SessionHeader            8 bytes
  count     u16  @0      number of operations
  abi       u16  @2      DESCRIPTOR_ABI (4)
  flags     u16  @4      parking flags
  reserved  u16  @6      must be zero

InvocationWire[count]    16 bytes each
  op        u16  @0      Derive, Revoke or Rendezvous
  requested u8   @2      rights requested for the result
  kind      u8   @3      resource kind, or a flavor selector
  subject   u32  @4      slot of the capability acted on
  result    u32  @8      slot the result lands in
  arg       u32  @12     offset into the argument region, or u32::MAX for none

Argument region          follows the operations
  [park block, if flags request one] then each operation's payload

The kind byte disambiguates op × kind. Zero means unspecified, values in the resource-kind band name the kind to produce, and high values (from 0xdd) select a flavor. An unknown flavor byte on a derive is refused, never run as a plain derive.

Derive flavors#

Most of the system's verbs are derive flavors. The full roster, with byte values and argument structs, is in session.rs; by purpose:

Some flavors are effects: they mint nothing, and their result slot stays vacant or receives a bind-inert report. A few effects apply after the capability fold commits, because hardware can refuse at that point (DEVICE_ACTIVATE, DEVICE_QUIESCE, ARENA_EXTEND); they must stand alone in their session. A spawn session must end with its founding run.

Revoke flavors#

EXEC and EXEC_RETURN are the only ways memory changes between writable and executable, which is how Kore keeps W^X above the page tables.

Rendezvous#

Channels have two ends, ChanSend and ChanRecv:

• A rendezvous on a receive end posts a landing slot for the next transfer. An optional RecvPolicyReq types the post: the kind and minimum rights it will accept.
• A rendezvous on a send end re-derives the capability in its result slot into the peer's posted slot, with the rights in requested. Sending requires DERIVE on the presented capability. The receiver's copy is re-stamped to the receiver as holder; the sender's bytes are never shared.
• Sending with no posted peer refuses the whole session with WouldBlock, which means it did not commit.

A send can instead carry a NoticeReq (a cookie and a payload): a bind-inert doorbell notice that needs only ACCESS on the send end. RENDEZVOUS_KIND_REQUEST_KICK (0xff) is the argument-free service-request kick, and RENDEZVOUS_KIND_EXACT_MOVE (0xfe) moves an affine capability keeping its kind, rights, lineage and tag.

Status codes#

Faults are reported coarsely by design: Forged doesn't say which check failed.

Parking#

A session can park its thread after it commits. The header's flags pick what wakes it:

Unknown bits are Malformed. When several conditions are armed, the first to fire wins and sets the status. The park block sits at the front of the argument region: ParkReq entries, then SleepReq (deadline in nanoseconds) and IrqParkReq as selected.

Limits#