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-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 (VFPv4-D16)

• 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:

Extensions for embedded real-time:

• L4_TimerNotify: Hardware timer with notification delivery
• L4_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:

Note: POSIX timer functions (timer_create, timer_settime) have limited functionality. Core threading, synchronization, and clock_gettime/nanosleep are fully operational.

Supported POSIX interfaces:

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:

make config    # Configure build options (Kconfig)
make           # Build F9 kernel → build/<BOARD>/f9.elf
make flash     # Flash to STM32F4 board (requires stlink)

make qemu

Press Ctrl+A then X to exit QEMU. Press ? for KDB debug menu (requires CONFIG_KDB).

QEMU uses the B-L475E-IOT01A machine with ARM semihosting for output and USART1 for KDB input. Both -semihosting and -serial mon:stdio are added automatically.

• STM32F4DISCOVERY (STM32F407VG)
• STM32F429I-DISC1 (STM32F429ZI)
• NUCLEO-F429ZI (STM32F429ZI)
• B-L475E-IOT01A (STM32L475VG) - QEMU target with FPU and MPU emulation

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:

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.