Specify kernel API surface #2

New Issue

Open

opened 2019-03-11 09:31:35 +00:00 by berkus · 0 comments

berkus commented

2019-03-11 09:31:35 +00:00

Owner

Low-level calls
Kernel object types
Capability-based calls
IPC
Cap management
AddressSpace management
Thread TCB management

Basic IPC is done via syscalls:

Send
- send to a capability
Non-blocking Send
- non-blocking send to a capability
Call
- call a capability (send followed by recv?)
Recv
- receive from an endpoint
Non-blocking Recv
- receive but don't block if nothing to receive
Reply
- send to a one-off reply capability
Reply-then-Recv
- send reply atomically followed by a recv

^ These are performed on capabilities.

Yield
- the only non-capabiility syscall that yields cpu slice to the thread with the same or lower priority.

Kernel makes use of the following primitive types:

Capability Nodes
Thread Control Blocks
Low-level interrupt support: IRQControl, IRQHandlers
Protection domain: Space
Raw memory: Untyped

Note:
seL4_UntypedObject,
seL4_TCBObject,
seL4_EndpointObject,
seL4_NotificationObject,
seL4_CapTableObject,

non-arch-specific objects in seL4

* Low-level calls * Kernel object types * Capability-based calls * IPC * Cap management * AddressSpace management * Thread TCB management Basic IPC is done via syscalls: * Send * send to a capability * Non-blocking Send * non-blocking send to a capability * Call * call a capability (send followed by recv?) * Recv * receive from an endpoint * Non-blocking Recv * receive but don't block if nothing to receive * Reply * send to a one-off reply capability * Reply-then-Recv * send reply atomically followed by a recv ^ These are performed on capabilities. * Yield * the only non-capabiility syscall that yields cpu slice to the thread with the same or lower priority. Kernel makes use of the following primitive types: * Capability Nodes * Thread Control Blocks * Low-level interrupt support: IRQControl, IRQHandlers * Protection domain: Space * Raw memory: Untyped Note: seL4_UntypedObject, seL4_TCBObject, seL4_EndpointObject, seL4_NotificationObject, seL4_CapTableObject, non-arch-specific objects in seL4