Execution and JIT

Relevant source files

The interpreter

Interpreter<P> implements BpfExecutor and is the only execution engine on the shipped path. BpfManager::execute_program is the call site for legacy programs. On this branch it goes through a shared with_bpf_runtime(maps, f) helper: obtain the current CPU’s execution context, borrow that CPU’s BPF scratch stack, install a per-execution BpfExecution record built from the program’s captured map bindings (used by helpers to resolve and lease maps), and run Interpreter::execute_with_stack. Managed instances reuse the same helper with their own exact local bindings, and host tests substitute a thread-local execution record so the real helpers can run off-target.

Behaviour of execute_with_stack:

The stack slice must be at least MAX_STACK_SIZE bytes. Only the verifier-recorded stack suffix (program.stack_size()) is zeroed before each run, not a caller-supplied size.
R1 holds a pointer to the BpfContext; R10 points to the top of the stack.
A program counter loop executes ALU, jump, load, store, call and wide-load instructions. A run that executes more than MAX_INSN_COUNT instructions fails with BpfError::Timeout; an out-of-range pc is OutOfBounds.
Helper calls look the ID up in the verifier’s shared descriptor table (get_helper_descriptor). An ID that the verifier knows but that has no runtime implementation returns InvalidHelper. Stack-backed pointer arguments have their provenance reconstructed from the live stack borrow before the helper is invoked.
BpfExecutor::execute is a convenience wrapper that allocates a fresh stack; it is documented for tests, benchmarks and cold paths. The kernel hook path uses the reused buffer so that no heap allocation occurs on interrupt paths.
Nested BPF execution on one CPU is rejected with ReentrantExecution.

BpfContext is repr(transparent) over a private raw record (data, data_end, data_meta, interrupt latency, boot time, heap KiB, image MiB). It carries a lifetime for the borrowed payload and is !Send and !Sync. Only layouts marked with the sealed BpfPod trait (the hook event structs) can be turned into a context with from_struct.

Runtime errors (BpfError) include the managed-only ManagedContextInvalid, ManagedRequestDuplicate, ManagedRequestInvalid and ManagedMapFailure added on this branch, plus DivisionByZero, OutOfBounds, StackOverflow, InvalidHelper, Timeout, InvalidInstruction, NotLoaded, OutOfMemory, ResourceLimit, ObjectBusy, PermissionDenied, ReentrantExecution, VerificationFailed, SignatureRejected, AdmissionRejected, GpioFanoutExceeded and ReadOnlyMap.

The default executor function default_executor always returns the interpreter (“for now, always return interpreter”).

ALU32 and endian semantics

Commit 2111f87 aligned the shared interpreter with what the verifier already assumed:

ALU32 operations truncate both operands to 32 bits before computing and zero-extend the result. This changes 32-bit DIV, MOD and right shifts when upper bits are set.
Shift counts are masked to 0x1f for ALU32 and 0x3f for ALU64 (main masked every shift with 0x3f), and 32-bit ARSH sign-extends from bit 31.
END (byte swap) honours its source bit: 0 converts to little endian, 1 to big endian, at widths 16, 32 and 64. main swapped unconditionally, which is wrong on a little-endian host for the to_le form.

A unit test (interpreter_alu_width_and_endian_semantics_match_ebpf) pins these cases.

Managed execution

Interpreter::execute_managed_with_stack is a separate entry used only by the managed control slot. It takes a ManagedProgram (never a VerifiedProgram), a frozen ManagedControlContextV1 payload and a stack; the kernel’s BehaviorInstance::execute wraps it in with_bpf_runtime with the instance’s exact local map bindings. It allocates nothing and never dispatches to hardware.

Item	Behaviour
Context	`ManagedControlContextV1`: 56 bytes, `version` 1, `size` 56, then `cycle_id`, `scheduled_ns`, `actual_ns`, `sensor_ns`, `sensor_value` (`i64`), `sensor_valid` (0 or 1), `reserved` 0. A malformed context fails with `ManagedContextInvalid`
Helper 1009 `bpf_managed_motor_pair_v1`	Two canonical sign-extended per-mille values in `[-1000, 1000]`; success records the pair in invocation-local storage
Second request	`ManagedRequestDuplicate`; the whole invocation fails even if bytecode ignores the helper’s return
Out-of-range or non-canonical request	`ManagedRequestInvalid`
Map failure on a declared binding	`ManagedMapFailure`; no request is returned
Result	`ManagedInvocationResult { request: Option<ManagedMotorPair> }`; `None` means no request was made and `motor_pair()` maps it to `(0, 0)`

The kernel, not the interpreter, then submits one complete pair through the actuation path or enters the trusted stop path. See Executor.

Profiles and execution

Profiles are sealed, build-time constants (see Overview for the table). For execution the relevant ones are MAX_STACK_SIZE, MAX_INSN_COUNT, and JIT_ALLOWED. Embedded and cloud both execute synchronously at the hook; the embedded profile additionally enforces the WCET and utilization budgets at load and attach time (Verifier). Per ARCHITECTURE.md, there is no second BPF scheduler and no enqueueing: hooks execute matching programs inline from an immutable snapshot.

Selecting a profile does not select an engine: PhysicalProfile::JIT_ALLOWED is false for both CloudProfile and EmbeddedProfile, and the profile test suite asserts it.

JIT policy (ADR 0004)

ADR-0004 (status: accepted, dated 2026-07-14) decides:

axiomOS v1.0 is interpreter-only. No shipped profile enables a JIT, and JIT is not on the release critical path.
Experimental JIT code must not provide kernel allocator symbols, executable mappings, or production call sites.
The existing AArch64 per-execution compiler and allocator path “will be removed from the shipped kernel_bpf surface or relocated to an experiment”; retaining it behind an undocumented feature is declared insufficient.
A future JIT needs a new superseding ADR and must satisfy six conditions: compile exactly once after verification and before publication; the verified program owns an immutable code image until epoch-safe unload; code is written into non-executable pages and transitioned once to read-only executable (never writable and executable together); compilation, allocation, protection changes and cache maintenance are fully fallible and transactional; hook dispatch performs no compilation, allocation, mapping or protection changes; and differential tests compare every supported instruction and helper with the interpreter, including malformed and resource-failure cases.

The profile comments record the motivating audit finding (C-06): the earlier AArch64 cloud JIT used a 256 MiB RWX bump allocator, recompiled on every hook fire and never freed.

What the code still contains

Compiler modules remain in the crate, so the repository state is slightly ahead of the ADR’s intended end state:

Module	Gate	Notes
`execution/jit_aarch64.rs` (`Arm64JitCompiler`, `Arm64JitExecutor`)	`target_arch = "aarch64"` with the `experimental-aarch64-jit` feature, or `cfg(test)`	Declares extern `bpf_jit_alloc_exec`, `bpf_jit_free_exec` and `aarch64_jit_sync_cache`. A repository search found no definitions of these symbols outside the module itself, and `experimental-aarch64-jit` is not enabled by any manifest searched
`execution/jit/mod.rs` (x86_64)	`cloud-profile` and `target_arch = "x86_64"`	Compiled into cloud x86_64 builds as a code generator; its source comments say executable memory handling would be done “in real impl”, and nothing selects it for execution

The Cargo.toml comment for the feature states it is “excluded from every shipped profile until code images have an owned, compile-on-load RW-to-RX lifecycle”. The module header in execution/mod.rs says the unsafe AArch64 JIT is erased from shipped builds. The kernel integration contains no RWX allocator.

On main, some comments predated the interpreter-only decision (for example BpfManager::bench_execute said the production path was “JIT on AArch64”). This branch removes that comment, makes bench_execute crate-private, and has BENCH_EXEC report the program’s wcet_cycles, the modeled nanoseconds (wcet_cycles * CYCLE_UNIT_NS) and the counter frequency so the verifier-cost corpus can compare measured interpreter time with the model. The cost-model comments now say the historical JIT measurements do not qualify the shipped interpreter.

tests/semantic_consistency.rs checks that the same bytecode produces the same results across profiles, the verify_then_exec fuzz target checks that verified programs execute without panicking in the interpreter, and tests/profile_contracts.rs pins the externally visible profile constants. The unit tests in interpreter.rs use a helpers_stub module that provides the extern "C" helper symbols on the host.