F9 is an L4-inspired microkernel designed for ARM Cortex-M, targeting real-time embedded systems with hard determinism requirements. It implements the fundamental microkernel principles—address spaces, threads, and IPC, while adding advanced features from industrial RTOSes.
- Hard Real-Time: Deterministic scheduling with preemption-threshold support
- Security: MPU-based memory protection and isolated execution
- Efficiency: Tickless scheduling, O(1) dispatcher, energy-aware operation
- Verifiability: Formal verification properties and comprehensive test coverage
- Priority Bitmap Scheduler: O(1) thread selection, supporting 32 priority levels
- Preemption-Threshold Scheduling (PTS): ThreadX-style deterministic scheduling reducing context switches in critical sections
- Priority Inheritance Protocol: Automatic priority boosting to prevent priority inversion
- Round-Robin: Fair scheduling within same priority level
- Tickless Operation: Wake only on scheduled events or interrupts for power efficiency
- MPU-Based Protection: Hardware memory isolation using ARM MPU (8 regions)
- Flexible Pages: Power-of-2 aligned memory regions mapped to MPU regions
- Address Spaces: Composed of flexible pages with Grant/Map/Flush operations
- Memory Pools: Physical address areas with specific attributes
- Synchronous IPC: L4-style message passing with blocking semantics
- Short IPC: Register-only payload (MR0-MR7) for low latency
- Full IPC: UTCB-based message copying for larger payloads
- UTCBs: Always-mapped user-level thread control blocks for fast syscall argument access
- ARM Cortex-M3/M4/M4F: Optimized for Cortex-M architecture
- NVIC: Nested Vectored Interrupt Controller integration
- Bit Banding: Hardware bit manipulation support (where available)
- FPU: Lazy context switching for Cortex-M4F floating-point unit
- KDB: In-kernel debugger with thread, memory, and timer inspection
- KProbes: Dynamic instrumentation without recompilation (Linux kernel-inspired)
- Profiling: Thread uptime, stack usage, memory fragmentation analysis
- Test Suite: Automated regression tests with QEMU integration
F9 provides two API layers for application development:
The kernel exposes an L4-family system call interface derived from L4Ka::Pistachio and seL4. Key syscalls:
| Syscall | Description |
|---|---|
L4_Ipc |
Synchronous message passing between threads |
L4_ThreadControl |
Create, configure, and delete threads |
L4_Schedule |
Set thread scheduling parameters |
L4_SpaceControl |
Configure address spaces |
L4_ExchangeRegisters |
Read/write thread register state |
L4_SystemClock |
Read system time (microseconds) |
L4_KernelInterface |
Access Kernel Interface Page (KIP) |
Extensions for embedded real-time:
L4_TimerNotify: Hardware timer with notification deliveryL4_NotifyWait/L4_NotifyPost/L4_NotifyClear: Lightweight notification primitives
A user-space compatibility layer implementing IEEE Std 1003.13-2003 profiles for portable real-time applications:
| Profile | Description | Status |
|---|---|---|
| PSE51 | Minimal Realtime System | API Compliant |
| PSE52 | Realtime Controller System | Partial |
Note: POSIX timer functions (timer_create, timer_settime) have limited functionality.
Core threading, synchronization, and clock_gettime/nanosleep are fully operational.
Supported POSIX interfaces:
| Category | Functions |
|---|---|
| Threads | pthread_create, pthread_join, pthread_detach, pthread_self, pthread_equal, pthread_cancel, pthread_testcancel |
| Mutexes | pthread_mutex_* (normal, recursive, errorcheck), pthread_mutex_timedlock |
| Condition Variables | pthread_cond_wait, pthread_cond_signal, pthread_cond_broadcast, pthread_cond_timedwait |
| Spinlocks | pthread_spin_init, pthread_spin_lock, pthread_spin_trylock, pthread_spin_unlock |
| Semaphores | sem_init, sem_wait, sem_trywait, sem_timedwait, sem_post, sem_getvalue |
| Time | clock_gettime, nanosleep |
The POSIX layer is implemented entirely in user space atop the native notification system, requiring no kernel modifications. See user/lib/posix for implementation details.
Comprehensive documentation is available in the Documentation/ directory:
| Document | Description |
|---|---|
| quick-start.md | Build, flash, and debug instructions |
| scheduler.md | Priority bitmap scheduler and PTS implementation |
| threads.md | Thread management, TCB structure, lifecycle |
| memory.md | Memory pools, flexible pages, MPU regions |
| ipc.md | Synchronous IPC, message passing, UTCBs |
| interrupt.md | NVIC integration, interrupt handling |
| ktimer.md | Timer subsystem, tickless scheduling |
| kprobes.md | Dynamic instrumentation system |
| init-hooks.md | Kernel initialization sequence |
| build-system.md | Kconfig-based build system |
make config # Configure build options (Kconfig)
make # Build F9 kernel → build/<BOARD>/f9.elf
make flash # Flash to STM32F4 board (requires stlink)make qemuPress Ctrl+A and then X to exit QEMU. Press ? in KDB for debug menu (requires CONFIG_KDB).
- STM32F4DISCOVERY (STM32F407VG)
- STM32F429I-DISC1 (STM32F429ZI)
- NUCLEO-F429ZI (STM32F429ZI)
- Netduino Plus 2 (STM32F405RG) - QEMU only, used for automated testing
For detailed instructions including toolchain setup, serial configuration, and debugging, see Documentation/quick-start.md.
F9 uses a Linux kernel-style build system via Kconfiglib.
Run make config to configure options via menu. Key options:
| Option | Description |
|---|---|
CONFIG_DEBUG |
Serial I/O for debugging |
CONFIG_KDB |
In-kernel debugger (press ? for menu) |
CONFIG_KPROBES |
Dynamic instrumentation system |
CONFIG_SYMMAP |
Symbol map for profiling |
CONFIG_KTIMER_TICKLESS |
Tickless scheduling (power efficiency) |
CONFIG_MAX_THREADS |
Maximum number of threads |
CONFIG_MAX_KT_EVENTS |
Maximum kernel timer events |
CONFIG_PANIC_DUMP_STACK |
Dump stack on kernel panic |
CONFIG_QEMU |
QEMU emulation workarounds |
For build system details, see Documentation/build-system.md.
F9 Microkernel is freely redistributable under the two-clause BSD License. See the LICENSE file for details.