F9, an experimental microkernel used to construct flexible embedded
systems inspired by famous L4 microkernel.
The motivation of F9 microkernel is to deploy modern kernel techniques to
support running real-time and time-sharing applications (for example, wireless
communications) for ARM Cortex-M series microprocessors with efficiency
(performance + power consumption) and security (memory protection + isolated
execution) in mind.
F9 follows the fundamental principles of microkernels in that it implements address spaces, thread management, and IPC only in the privileged kernel.
Designed and customized for ARM Cortex-M, supporting NVIC (Nested Vectored Interrupt Controller), Bit Banding, MPU (Memory Protection Unit).
Energy efficient scheduling and tickless timer which allow the ARM Cortex-M to wake up only when needed, either at a scheduled time or on an interrupt event. Therefore, it results in better current consumption than the common approach using the system timer, SysTick, which requires a constantly running and high frequency clock.
KProbes, dynamic instrumentation system inspired by Linux Kernel, allowing developers to gather additional information about kernel operation without recompiling or rebooting the kernel. It enables locations in the kernel to be instrumented with code, and the instrumentation code runs when the ARM core encounters that probe point. Once the instrumentation code completes execution, the kernel continues normal execution.
Each thread has its own TCB (Thread Control Block) and addressed by its global id. Also dispatcher is responsible for switching contexts. Threads with the same priority are executed in a round-robin fashion.
Memory management is split into three concepts:
System calls are provided to manage address spaces:
Regarding the interaction between a user thread and the microkernel, the concept of UTCB (user-level thread-control blocks) is being taken on. A UTCB is a small thread-specific region in the thread's virtual address space, which is always mapped. Therefore, the access to the UTCB can never raise a page fault, which makes it perfect for the kernel to access system-call arguments, in particular IPC payload copied from/to user threads.
The kernel provides synchronous IPC (inter-process communication), for which short IPC carries payload in CPU registers only and full IPC copies message payload via the UTCBs of the communicating parties.
Debugging and profiling mechanisms:
F9 Microkernel is freely redistributable under the two-clause BSD License.
Use of this source code is governed by a BSD-style license that can be found
F9 Microkernel supports the following boards:
Building F9 Microkernel requires an arm-none-eabi- toolchain with Cortex-M4F support. The known working toolchains are as following
Other build dependency includes: (for Debian/Ubuntu)
Configuration is the initial step in the build of F9 Microkernel for your
target, and you can use
make config to specify the options from which to
choose. Regardless of the configuration method you use or the actual
configuration options you choose, the build system will generate a
file at the end of the configuration and will generate a configuration header
include/autoconf.h for C programs.
Then, just execute
make to get the generated files in directory
For flashing and debugging on the STM32F40x, stlink is required.
stlink in your path, command "make flash" will flash your
STM32F4DISCOVERY board with built F9 binary image.
When developing on top of F9 Microkernel, you do not have the luxury of using a source level debugger such as gdb. There are still a number of techniques at your disposal to assist debugging, however. KDB (in-kernel debugger) is built and run at boot by default, and here are the supported commands:
Through USART, KDB can be operated interactively on USART4 (default), USART2,
or USART1 of STM32F4DISCOVERY depending on the selected option when you execute
For 32F429IDISCOVERY, the pins are as follows:
You can established serial connection with the board using a serial to USB converter (for STM32F4DISCOVERY):
or (for 32F429IDISCOVERY):
Select the appropriate terminal emulator and configure it for 115200 baud,
8 data bits, no parity, one stop bit. For GNU/Linux, program
screen can be
used for such purpose. Installation on Ubuntu / Debian based systems:
sudo apt-get install screen
Then, attach the device file where a serial to USB converter is attached:
screen /dev/ttyUSB0 115200 8n1
Once you want to quit screen, press: Ctrl-a k
F9 Microkernel deploys Linux Kernel style build system, and the corresponding files are described as following:
You can modify source file board/
<BOARD_NAME>/board.[ch] to specify the
preferable resource assignment. To get acquainted with the configuration of
F9 Microkernel internals, file
include/autoconf.h is the entry point: