seL4 Version 6.0.0 Release

Announcing the release of seL4 6.0.0 with the following changes:

Highlights

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).

ARM 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.

Changes

  • 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 https://github.com/seL4/seL4

More details

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