lona.kernel¶

Low-level seL4 kernel intrinsics. Used by VM runtime and system code, not application developers.

System Info¶

`arch`¶

Get current CPU architecture.

(arch)  ; → :x86_64 or :aarch64

Use for architecture-specific code paths (e.g., selecting page table types).

;; @todo @x86_64
(arch)  ; => :x86_64

;; @todo @aarch64
(arch)  ; => :aarch64

;; @todo
(keyword? (arch))  ; => true
;; arch returns one of the supported architectures
(or (= (arch) :x86_64) (= (arch) :aarch64))  ; => true

IPC Operations¶

seL4 IPC is synchronous and uses endpoints.

`send!`¶

Blocking send.

(send! endpoint msg-info)  ; Blocks until received

`send-nb!`¶

Non-blocking send.

(send-nb! endpoint msg-info)  ; Returns immediately

Message dropped if no receiver.

;; @todo
;; Non-blocking send returns immediately
(def ep endpoint)  ; assume endpoint exists
(def mi (msg-info 0 0 0))
(send-nb! ep mi)  ; => :ok

`recv!`¶

Blocking receive.

(recv! endpoint)  ; → [msg-info badge]

;; @todo
;; recv! returns a tuple
(def result (recv! endpoint))
(tuple? result)  ; => true

`recv-nb!`¶

Non-blocking receive.

(recv-nb! endpoint)  ; → [msg-info badge] or nil

;; @todo
;; Non-blocking receive returns nil if no message
(def result (recv-nb! endpoint))
(or (nil? result) (tuple? result))  ; => true

`call!`¶

RPC: send + receive.

(call! endpoint msg-info)  ; → [reply-info badge]

;; @todo
;; call! returns a tuple
(def mi (msg-info 0 0 0))
(def result (call! endpoint mi))
(tuple? result)  ; => true

`reply!`¶

Reply to caller.

(reply! msg-info)  ; Reply to last call

;; @todo
(def mi (msg-info 0 0 0))
(reply! mi)  ; => :ok

`reply-recv!`¶

Reply + receive (server fast-path).

(reply-recv! endpoint msg-info)  ; → [msg-info badge]

;; @todo
(def mi (msg-info 0 0 0))
(def result (reply-recv! endpoint mi))
(tuple? result)  ; => true

`yield!`¶

Voluntarily give up the current timeslice, allowing other threads to run.

(yield!)

;; @todo
(yield!)  ; => nil

Implementation note: Currently implemented via seL4's seL4_SchedContext_YieldTo. This is an implementation detail and may change; do not rely on specific yield-to semantics.

Notification Operations¶

Asynchronous signaling.

`signal!`¶

Signal notification.

(signal! notification)

ORs badge into notification word, wakes waiters.

;; @todo
(def n (make-notification))
(signal! n)  ; => :ok

`wait!`¶

Wait for notification.

(wait! notification)  ; → badge

Blocks until signaled, returns and clears word.

;; @todo
;; wait! returns an integer badge
(def n (make-notification))
(signal! n)
(integer? (wait! n))  ; => true

`poll!`¶

Poll notification.

(poll! notification)  ; → badge or nil

;; @todo
(def n (make-notification))
(poll! n)  ; => nil

(signal! n)
(integer? (poll! n))  ; => true

TCB Operations¶

Thread Control Block management.

`tcb-configure!`¶

Configure TCB.

(tcb-configure! tcb opts)

Options: :fault-ep, :cspace-root, :cspace-data, :vspace-root, :vspace-data, :ipc-buffer, :ipc-buffer-addr.

;; @todo
(tcb-configure! tcb %{:cspace-root cnode :vspace-root vspace})  ; => :ok

`tcb-set-space!`¶

Set TCB's CSpace and VSpace.

(tcb-set-space! tcb opts)

;; @todo
(tcb-set-space! tcb %{:cspace-root cnode :vspace-root vspace})  ; => :ok

`tcb-set-ipc-buffer!`¶

Set IPC buffer.

(tcb-set-ipc-buffer! tcb frame vaddr)

;; @todo
(tcb-set-ipc-buffer! tcb frame (vaddr 0x4000u64))  ; => :ok

`tcb-set-priority!`¶

Set priority (0-255).

(tcb-set-priority! tcb authority priority)

;; @todo
(tcb-set-priority! tcb auth 100)  ; => :ok

`tcb-set-mc-priority!`¶

Set max controlled priority.

(tcb-set-mc-priority! tcb authority mcp)

;; @todo
(tcb-set-mc-priority! tcb auth 200)  ; => :ok

`tcb-set-sched-params!`¶

Set scheduling parameters (MCS).

(tcb-set-sched-params! tcb authority opts)

Options: :priority, :mcp, :sched-context, :fault-ep.

;; @todo
(tcb-set-sched-params! tcb auth %{:priority 100 :mcp 200})  ; => :ok

`tcb-set-affinity!`¶

Pin to CPU core.

(tcb-set-affinity! tcb core-id)

;; @todo
(tcb-set-affinity! tcb 0)  ; => :ok

`tcb-resume!`¶

Make thread runnable.

(tcb-resume! tcb)

;; @todo
(tcb-resume! tcb)  ; => :ok

`tcb-suspend!`¶

Pause thread.

(tcb-suspend! tcb)

;; @todo
(tcb-suspend! tcb)  ; => :ok

`tcb-read-regs`¶

Read registers from suspended thread.

(tcb-read-regs tcb count suspend?)  ; → %{:pc :sp :regs [...]}

;; @todo
(def regs (tcb-read-regs tcb 10 false))
(map? regs)            ; => true
(contains? regs :pc)   ; => true
(contains? regs :sp)   ; => true
(contains? regs :regs) ; => true

`tcb-write-regs!`¶

Write registers.

(tcb-write-regs! tcb resume? flags regs)

;; @todo
(tcb-write-regs! tcb false 0 %{:pc 0x1000u64 :sp 0x2000u64})  ; => :ok

`tcb-bind-notification!`¶

Bind notification to TCB.

(tcb-bind-notification! tcb notification)

;; @todo
(def n (make-notification))
(tcb-bind-notification! tcb n)  ; => :ok

`tcb-unbind-notification!`¶

Unbind notification.

(tcb-unbind-notification! tcb)

;; @todo
(tcb-unbind-notification! tcb)  ; => :ok

CNode Operations¶

Capability space management.

`cap-copy!`¶

Copy capability with rights mask.

(cap-copy! dest-cn dest-slot src-cn src-slot rights)

;; @todo
(cap-copy! dest-cn 1 src-cn 2 #{:read})  ; => :ok

`cap-mint!`¶

Copy with badge.

(cap-mint! dest-cn dest-slot src-cn src-slot rights badge)

;; @todo
(cap-mint! dest-cn 1 src-cn 2 #{:read :write} 0x1234)  ; => :ok

`cap-move!`¶

Move capability.

(cap-move! dest-cn dest-slot src-cn src-slot)

;; @todo
(cap-move! dest-cn 1 src-cn 2)  ; => :ok

`cap-mutate!`¶

Move with modified guard.

(cap-mutate! dest-cn dest-slot src-cn src-slot guard)

;; @todo
(cap-mutate! dest-cn 1 src-cn 2 0)  ; => :ok

`cap-delete!`¶

Delete capability.

(cap-delete! cnode slot)

;; @todo
(cap-delete! cnode 5)  ; => :ok

`cap-revoke!`¶

Delete capability and all derivatives.

(cap-revoke! cnode slot)

;; @todo
(cap-revoke! cnode 5)  ; => :ok

`cap-rotate!`¶

Atomic three-way move.

(cap-rotate! dest-cn dest-slot pivot-cn pivot-slot src-cn src-slot badge)

;; @todo
(cap-rotate! dest-cn 1 pivot-cn 2 src-cn 3 0x5678)  ; => :ok

`cap-save-caller!`¶

Save reply capability.

(cap-save-caller! cnode slot)

;; @todo
(cap-save-caller! cnode 10)  ; => :ok

Untyped Operations¶

`untyped-retype!`¶

Convert untyped to typed objects.

(untyped-retype! untyped type size-bits dest-cn dest-slot count)

Common types: :tcb, :endpoint, :notification, :cnode, :sched-context

Frame types: :frame-4k, :frame-2m, :frame-1g

Page table types (architecture-specific):

x86_64	ARM64 (aarch64)	Description
`:pml4`	`:pgd`	Root page table (VSpace root)
`:pdpt`	`:pud`	Level 2
`:page-directory`	`:pmd`	Level 3
`:page-table`	`:pte`	Level 4 (leaf)

Use (arch) to detect architecture and select appropriate types:

(def vspace-root-type
  (match (arch)
    :x86_64  :pml4
    :aarch64 :pgd))

;; @todo
(untyped-retype! untyped :endpoint 0 dest-cn 0 1)  ; => :ok

;; @todo
(untyped-retype! untyped :frame-4k 12 dest-cn 0 4)  ; => :ok

Scheduling Operations (MCS)¶

`sched-configure!`¶

Configure scheduling context.

(sched-configure! sched-control sc opts)

Options: :budget, :period, :extra-refills, :badge, :flags.

;; @todo
(sched-configure! sched-control sc %{:budget 100000 :period 1000000})  ; => :ok

`sched-context-bind!`¶

Bind TCB or notification.

(sched-context-bind! sc object)

;; @todo
(sched-context-bind! sc tcb)  ; => :ok

`sched-context-unbind!`¶

Unbind all objects.

(sched-context-unbind! sc)

;; @todo
(sched-context-unbind! sc)  ; => :ok

`sched-context-unbind-object!`¶

Unbind specific object.

(sched-context-unbind-object! sc object)

;; @todo
(sched-context-unbind-object! sc tcb)  ; => :ok

`sched-context-consumed`¶

Get consumed CPU time.

(sched-context-consumed sc)  ; → nanoseconds

;; @todo
(integer? (sched-context-consumed sc))  ; => true
(>= (sched-context-consumed sc) 0)      ; => true

IRQ Operations¶

`irq-control-get!`¶

Create IRQ handler capability.

(irq-control-get! irq-control irq-num dest-cn dest-slot)

;; @todo
(irq-control-get! irq-control 33 dest-cn 0)  ; => :ok

`irq-handler-ack!`¶

Acknowledge interrupt.

(irq-handler-ack! handler)

;; @todo
(irq-handler-ack! handler)  ; => :ok

`irq-handler-set-notification!`¶

Set notification for IRQ.

(irq-handler-set-notification! handler notification)

;; @todo
(def n (make-notification))
(irq-handler-set-notification! handler n)  ; => :ok

`irq-handler-clear!`¶

Remove IRQ handler.

(irq-handler-clear! handler)

;; @todo
(irq-handler-clear! handler)  ; => :ok

VSpace Operations¶

`page-map!`¶

Map frame into address space.

(page-map! frame vspace vaddr rights attrs)

Rights: :read, :write, :execute

Attrs: :cached, :uncached, :device, :write-combine

;; @todo
(page-map! frame vspace (vaddr 0x4000u64) #{:read :write} :cached)  ; => :ok

`page-unmap!`¶

Unmap frame.

(page-unmap! frame)

;; @todo
(page-unmap! frame)  ; => :ok

`page-get-address`¶

Get physical address.

(page-get-address frame)  ; → paddr

;; @todo
(paddr? (page-get-address frame))  ; => true

`page-table-map!`¶

Map page table.

(page-table-map! pt vspace vaddr attrs)

;; @todo
(page-table-map! pt vspace (vaddr 0x200000u64) :cached)  ; => :ok

`page-table-unmap!`¶

Unmap page table.

(page-table-unmap! pt)

;; @todo
(page-table-unmap! pt)  ; => :ok

`asid-pool-assign!`¶

Assign ASID to VSpace.

(asid-pool-assign! pool vspace)

;; @todo
(asid-pool-assign! pool vspace)  ; => :ok

Debug Operations¶

Available when kernel built with DEBUG_BUILD.

`debug-put-char!`¶

Output to kernel serial.

(debug-put-char! ch)

;; @todo
(debug-put-char! \A)  ; => :ok

`debug-halt!`¶

Halt system.

(debug-halt!)

;; @todo
;; debug-halt! halts the entire system - cannot test interactively
;; (debug-halt!)  ; Would halt system

`debug-dump-scheduler!`¶

Dump scheduler state.

(debug-dump-scheduler!)

;; @todo
(debug-dump-scheduler!)  ; => :ok

`debug-cap-identify`¶

Identify capability type.

(debug-cap-identify cap)  ; → type keyword

;; @todo
(keyword? (debug-cap-identify frame))  ; => true
(debug-cap-identify frame)             ; => :frame

`debug-name-thread!`¶

Set thread name.

(debug-name-thread! tcb name)

;; @todo
(debug-name-thread! tcb "worker-1")  ; => :ok

Appendix: Expected Derived Functions¶

All functions in this namespace are intrinsics. No derived functions expected.

lona.kernel¶

System Info¶

arch¶

IPC Operations¶

send!¶

send-nb!¶

recv!¶

recv-nb!¶

call!¶

reply!¶

reply-recv!¶

yield!¶

Notification Operations¶

signal!¶

wait!¶

poll!¶

TCB Operations¶

tcb-configure!¶

tcb-set-space!¶

tcb-set-ipc-buffer!¶

tcb-set-priority!¶

tcb-set-mc-priority!¶

tcb-set-sched-params!¶

tcb-set-affinity!¶

tcb-resume!¶

tcb-suspend!¶

tcb-read-regs¶

tcb-write-regs!¶

tcb-bind-notification!¶

tcb-unbind-notification!¶

CNode Operations¶

cap-copy!¶

cap-mint!¶

cap-move!¶

cap-mutate!¶

cap-delete!¶

cap-revoke!¶

cap-rotate!¶

cap-save-caller!¶