seL4 Version 6.0.0 Release

Announcing the release of seL4 6.0.0 with the following changes:


ARM 32-bit SMP

  • Works (and tested) only on Sabre/ARM with up to 4 cores.
  • Using the big kernel lock (same as x86 implementation).
  • Boot core is assumed to have an ID of 0.
  • Kernel bootstraps and initialises data structures only on the boot core.
  • Root task proceeds on the boot core.
  • Cores are assumed to have linear IDes.

ARM IPI caveats:

  • Reserving the first two per-core SGIs for seL4’s IPI operations: 0 to do a remote call, 1 to reschedule.
  • Relying on GIC.
  • Reschedule IPIs are sent when migrating a thread.
  • Remote call IPIs are sent if TLB and/or cache maintenance operations are required.
  • Remote FPU operations (when migrating threads that use HW FPU).


ARMv7 32-bit support is added to implement a lazy FP save/restore mechanism, required for user threads when they use the FPU. The following caveats exist:

  • Only support synchronous exceptions. No support for asynchronous ones.
  • VFP opcodes are used instead of normal instructions to discard compiler warnings/errors.
  • Support is limited to specific ARM subarchitectures we support and tested this feature on.
  • Disable the FPU by default if users are not using it to avoid channels.
  • FPU support is not verified yet.
  • Will not work properly if using a VM that’s running alongside other VMs/threads that are using the FPU.
  • Any trapped FPU instruction (e.g. traps that need support code or deprecated vectored VFP operations) are forwarded to the user as a fault.


  • aarch32 - Implement lazy FP save/restore
  • ARM SMP support
  • add seL4_DebugDumpScheduler debug syscall
  • x86: Split large structs into portions (See upgrade notes below)
  • License fixups

Upgrade notes

  • This release is not source compatible with previous releases.
  • seL4_DebugDumpScheduler has had its only argument removed as it was unused.
  • On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if VESA BIOS Extensions (VBE) information is being used.

Full changelog

Use git log 5.2.0..6.0.0 in

More details

See the 6.0.0 manual included in the release or ask on the mailing list!