Protection Domain Declarations

ProtectionDomainDecl ::= 'ProtectionDomain' ident '(' priority (',' irq)? (',' budget)? (',' period)? ')' ';'
priority             ::= integer_literal       // 0 ≤ p ≤ 254
irq                  ::= integer_literal       // 0 ≤ irq ≤ 159
budget               ::= integer_literal       // microseconds, default 1000
period               ::= integer_literal       // microseconds, default = budget

A protection-domain declaration introduces one named seL4 Microkit protection domain (PD): an isolated thread of execution with its own address space, scheduling parameters, and (optionally) one IRQ binding. Each ProtectionDomain listed in a .fis system file pairs with one .fi program file by name.

Fields

• Name — snake_case identifier. The matching <name>.fi file holds the PD’s mappings, constructor block, events, and processes.
• Priority — required, range 0..=254. Out-of-range values are rejected with a parse-time error. Higher numbers run first under the Microkit fixed-priority scheduler.
• IRQ — optional, range 0..=159. When present, the PD is wired to receive that hardware interrupt on the reserved irq channel and can observe it via irq?N / irq!N events.
• Budget — optional, microseconds; defaults to 1000. Microkit schedules the PD for at most budget microseconds out of every period.
• Period — optional, microseconds; defaults to whatever budget was set to. Setting period > budget produces a sub-rate scheduling policy.

The trailing fields are positional: to pin only the period, both irq and budget must precede it.

Validation

• priority must be in 0..=254.
• A PD name is unique within the system file.
• A PD that is referenced from a Channel or from the System = composition must be declared.
• A PD without a corresponding <name>.fi is rejected at link time (not at parse time).

Examples

// Three PDs with distinct priorities; IRQ on the outer driver only.
ProtectionDomain eth_outer(99, 159);
ProtectionDomain dd(150);
ProtectionDomain eth_inner(199, 155);

// A simulator with a low priority and no IRQ binding.
ProtectionDomain simulate(50);

// Explicit budget / period pair (sub-rate scheduling).
ProtectionDomain monitor(120, 0, 200, 1000);  // priority 120, IRQ 0, 200 µs / 1 ms

System composition

A .fis file ends with a System = ... clause that names the PDs to include and their composition operator (currently always |||, interleave). Every PD referenced in System must be declared above:

System = eth_outer ||| dd ||| eth_inner ||| simulate;

PDs declared but omitted from System are dead code and currently produce no error; this may tighten in a future revision.