Refine top-level documentation

Author: jserv

README.md

@@ -1,169 +1,129 @@
-F9 Microkernel
-==============
+# F9 Microkernel
 
-This is `F9`, an experimental microkernel used to construct flexible embedded
-systems inspired by famous [L4 microkernel](http://en.wikipedia.org/wiki/L4_microkernel_family).
-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.
-
-
-Characteristics of F9 Microkernel
-=================================
+F9 is an experimental microkernel for building flexible embedded systems,
+inspired by the [L4 microkernel family](https://en.wikipedia.org/wiki/L4_microkernel_family).
+It aims to bring modern kernel techniques to ARM Cortex-M microprocessors,
+enabling real-time and time-sharing applications (such as wireless communications)
+with a focus on efficiency (performance and power consumption) and security
+(memory protection and isolated execution).
 
+## Characteristics
 * 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
+* Energy-efficient scheduling and tickless timer allow the ARM Cortex-M to
+  wake up only when needed, either at a scheduled time or on an interrupt event.
+  This results in lower power consumption compared to the traditional SysTick
+  approach, which requires a constantly running high-frequency clock.
+* KProbes, a dynamic instrumentation system inspired by the 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.
-
+* Each thread has its own TCB (Thread Control Block) and is addressed by its
+  global ID. The dispatcher is responsible for context switching. Threads
+  with the same priority are scheduled in round-robin fashion.
 * Memory management is split into three concepts:
-  - Memory pool, which represent area of physical address space with specific
-    attributes.
-  - Flexible page, which describes an always size aligned region of an address
-    space. Unlike other L4 implementations, flexible pages in F9 represent MPU
-    region instead.
-  - Address space, which is made up of these flexible pages.
-
+  - Memory pool: an area of physical address space with specific attributes.
+  - Flexible page: a size-aligned region of an address space. Unlike other L4
+    implementations, flexible pages in F9 represent MPU regions.
+  - Address space: composed of flexible pages.
 * System calls are provided to manage address spaces:
   - Grant: The memory page is granted to a new user and cannot be used anymore
     by its former user.
   - Map: This implements shared memory – the memory page is passed to another
     task but can be used by both tasks.
   - Flush: The memory page that has been mapped to other users will be flushed
     out of their address space.
-
-* 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.
-
+* User threads interact with the microkernel through UTCBs (User-level Thread
+  Control Blocks). A UTCB is a small thread-specific region in the thread's
+  virtual address space that is always mapped. Since UTCB access never raises
+  a page fault, it is ideal for the kernel to access system call arguments,
+  particularly IPC payload copied from/to user threads.
+* The kernel provides synchronous IPC (inter-process communication). Short IPC
+  carries payload in CPU registers only, while full IPC copies message payload
+  via the UTCBs of the communicating parties.
 * Debugging and profiling mechanisms:
   - configurable debug console
   - memory dump
   - thread profiling: name, uptime, stack allocated/current/used
   - memory profiling: kernel table, pool free/allocated size, fragmentation
 
-
-Licensing
-=========
-
-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
-in the `LICENSE` file.
-
-
-Quick Start
-===========
-
+## Quick Start
 F9 Microkernel supports the following boards:
-* [STM32F4DISCOVERY](http://www.st.com/web/en/catalog/tools/FM116/SC959/SS1532/PF252419)
-* [32F429IDISCOVERY](http://www.st.com/web/catalog/tools/FM116/SC959/SS1532/PF259090)
-  - Both are based on ARM Cortex-M4F core, but F9 should work well on any STM32F40x/STM32F429/STM32F439
-microcontroller.
-* [STM32-P103](https://www.olimex.com/Products/ARM/ST/STM32-P103/)
-  - Powered by Cortex-M3 based microcontroller, STM32F103RBT6
-
-Building F9 Microkernel requires an arm-none-eabi- toolchain with Cortex-M4F support. The known working toolchains are as following
-* [Sourcery CodeBench](http://www.mentor.com/embedded-software/sourcery-tools/sourcery-codebench/editions/lite-edition/)
-  - ARM Processors: EABI Release
-  - Verified versions: arm-2012.03, arm-2013.05, arm-2013.11, arm-2014.05
-* [GNU Tools for ARM Embedded Processors](https://launchpad.net/gcc-arm-embedded)
-  - Verified versions: 4.8-2013-q4-major, 4.8-2014q2-update
-
-Other build dependency includes: (for Debian/Ubuntu)
-* libncurses5-dev
-
-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 `.config`
-file at the end of the configuration and will generate a configuration header
-file, `include/autoconf.h` for C programs.
-
-Then, just execute `make` to get the generated files in directory `build`.
-
-For flashing and debugging on the STM32F40x, [stlink](https://github.com/texane/stlink) is required.
-With `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:
-
-* a: dump address spaces
-* m: dump memory pools
-* t: dump threads
-* s: show softirqs
-* n: show timer (now)
-* e: dump ktimer events
-* K: print kernel tables
-
-Through USART, KDB can be operated interactively on USART4 (default), USART2,
-or USART1 of STM32F4DISCOVERY depending on the selected option when you execute
-`make config`:
-* USART4: PA0 (TX), PA1  (RX)
-* USART2: PA2 (TX), PA3  (RX)
-* USART1: PA9 (TX), PX10 (RX)
-
-For 32F429IDISCOVERY, the pins are as follows:
-* USART4: PC11 (TX), PC10 (RX) (default config)
-* USART2: PD5 (TX), PD6 (RX)
-* USART1: PA9 (TX), PA10 (RX)
-
-You can established serial connection with the board using a serial to USB
-converter (for STM32F4DISCOVERY):
-* USB2TTL RX ---> PA0 / PA2 / PA9
-* USB2TTL TX ---> PA1 / PA3 / PA10
-
-or (for 32F429IDISCOVERY):
-* USB2TTL RX ---> PC11 / PD5 / PA9
-* USB2TTL TX ---> PC10 / PD6 / PA10
-
-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:
+* [STM32F4DISCOVERY](https://www.st.com/en/evaluation-tools/stm32f4discovery.html)
+* [STM32F429I-DISC1](https://www.st.com/en/evaluation-tools/32f429idiscovery.html)
+  - Both are based on ARM Cortex-M4F core. F9 should work on any STM32F40x/STM32F429/STM32F439 microcontroller.
+* Netduino Plus 2 (STM32F405RGT6)
+  - Supported by upstream [QEMU for emulation](https://www.qemu.org/docs/master/system/arm/stm32.html), making it ideal for development and testing without hardware.
+
+Building F9 Microkernel requires an arm-none-eabi toolchain with Cortex-M4F support:
+* [Arm GNU Toolchain](https://developer.arm.com/downloads/-/arm-gnu-toolchain-downloads)
+  - Download the AArch32 bare-metal target (arm-none-eabi) package.
+
+Configuration is the first build step. Run `make config` to select options.
+The build system generates a `.config` file and a configuration header
+`include/autoconf.h` for C programs.
+
+Run `make` to build. Output files are placed in the `build` directory.
+
+For flashing and debugging on STM32F4 boards, [stlink](https://github.com/stlink-org/stlink)
+is required. With `st-flash` in the PATH, `make flash` programs the
+STM32F4DISCOVERY board with the built F9 binary image.
+
+Source-level debugging with gdb is possible via OpenOCD or stlink, but may be
+limited on resource-constrained targets. KDB (in-kernel debugger) is enabled by
+default and provides essential kernel inspection. Press `?` to display the menu:
+
+| Key | Function                        |
+|-----|---------------------------------|
+| `a` | Dump address spaces             |
+| `e` | Dump ktimer events              |
+| `K` | Print kernel tables             |
+| `m` | Dump memory pools               |
+| `M` | Dump MPU status                 |
+| `n` | Show timer (now)                |
+| `p` | Show sampling (requires SYMMAP) |
+| `s` | Show softirqs                   |
+| `t` | Dump threads                    |
+| `v` | Show tickless scheduling status |
+
+KDB communicates via USART. The port can be selected during `make config`.
+
+For STM32F4DISCOVERY:
+
+| Port   | TX Pin | RX Pin |
+|--------|--------|--------|
+| USART4 | PA0    | PA1    |
+| USART2 | PA2    | PA3    |
+| USART1 | PA9    | PA10   |
+
+For STM32F429I-DISC1:
+
+| Port   | TX Pin | RX Pin |
+|--------|--------|--------|
+| USART4 | PC11   | PC10   |
+| USART2 | PD5    | PD6    |
+| USART1 | PA9    | PA10   |
+
+For Netduino Plus 2 under QEMU, the default configuration uses USART1, which
+QEMU routes to the console. Run with:
+
+    qemu-system-arm -M netduinoplus2 -nographic -serial mon:stdio \
+        -kernel build/netduinoplus2/f9.elf
+
+For physical boards, connect a USB-to-serial adapter and use a terminal emulator
+at 115200 baud, 8N1. For example, with `screen`:
 
     screen /dev/ttyUSB0 115200 8n1
 
-Once you want to quit screen, press: Ctrl-a k
+Press Ctrl-a k to exit screen.
 
-
-Build Configurations
-====================
-
-F9 Microkernel deploys Linux Kernel style build system, and the corresponding
-files are described as following:
+## Build Configurations
+F9 Microkernel uses a Linux kernel-style build system (Kconfig/Kconfiglib).
+The key build files are:
 
 * toolchain.mk:
   - toolchain-specific configurations; common cflags and ldflags
@@ -173,28 +133,31 @@ files are described as following:
   - board-specific configurations; CHIP model, peripherals
 * rules.mk: the magic of build system
 
-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:
+Board-specific resource assignments can be modified in `board/<BOARD_NAME>/board.[ch]`.
+The configuration header `include/autoconf.h` documents the available options:
 
 * `CONFIG_DEBUG`
-  - Enable serial input/out for debugging purpose. An additional service for
-    serial I/O character operations will be included.
+  - Enable serial I/O for debugging. An additional service for serial character
+    operations will be included.
 * `CONFIG_KDB`
   - Enable in-kernel debugger.
 * `CONFIG_KPROBES`
-  - Enable kernel probes, the lightweight dynamic instrumentation system.
-* `CONFIG_BITMAP_BITBAND`
-  - Generate bitmap address in bit-band region
-  - Bit-banding maps a complete word of memory onto a single bit in the
-    bit-band region. For example, writing to one of the alias words will set
-    or clear the corresponding bit in the bitband region.
-  - When writing to the alias regions bit 0 of the 32 bit word is used to set
-    the value at the bit-banding region. Reading from the alias address will
-    return the value from the bit-band region in bit 0 and the other bits will
-    be cleared.
+  - Enable KProbes, the lightweight dynamic instrumentation system.
+* `CONFIG_SYMMAP`
+  - Generate symbol map for KProbes and profiling support.
+* `CONFIG_KTIMER_TICKLESS`
+  - Enable tickless scheduling for improved power efficiency.
+* `CONFIG_KTIMER_TICKLESS_VERIFY`
+  - Track and verify tickless scheduling status (depends on KTIMER_TICKLESS).
 * `CONFIG_MAX_`xxx series
-  - limits of threads, ktimer events, async events, address spaces, flexible
-    pages.
+  - Limits for threads, ktimer events, async events, address spaces, and
+    flexible pages.
 * `CONFIG_PANIC_DUMP_STACK`
-  - Dump kernel stack while panic.
+  - Dump kernel stack on panic.
+* `CONFIG_QEMU`
+  - Enable workarounds for QEMU emulation (auto-enabled for Netduino Plus 2).
+
+## Licensing
+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
+in the `LICENSE` file.