Introducing seL4 4.0.0

Announcing the release of seL4 4.0.0 with the following changes:

General:

• Reorder bootinfo structure.
• Add missing seL4_AllRights macro in libsel4.
• Disallow kernel from using a device frame as an IPC buffer.
• Syscall docs in manual now generated by doxygen.
• Changes to make verification easier.
• Various documentation fixes.
• Benchmarks refactoring.
• Coding style fixes.
• Support for TLB and Cache management.
• Preemptible backwards memzero for Retype.
• Support for TCB operations in X86 multicore.
• Support for raspberry-pi 3.
• Add seL4_BenchmarkFlushCaches() for arm and ia32.

ARM specific changes:

• ARM Hyp refactoring.
• Update VCPU fault definitions.
• Add userspace invocations for hardware debugging.
• Enable PMU export for V8.
• Support ARM MPCore registers.
• Fix config dependency for ‘IPC Buffer location’.
• Use new cap rights structures in iospace.
• Move initial setting of TPIDRURW register.
• Support for prefetcher on Cortex-A9.
• Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C.
• am335x: Prevent out of bounds array access.

TK1

• Remove temporary SMMU memory mapping support.
• Correct SMMU PD and PT indexing.
• Split the mux controller from the misc region.

OMAP:

• Fix issues with OMAP IRQ Code.

X86 specific changes:

• Add userspace invocations for hardware debugging.
• Avoid writing the fs/gs base unless necessary.
• Explicitly declare address of .phys.bss.
• Add BSS regions for BOOT and PHYS code.
• Write FS and GS base when restoring user context.
• Initialize store area when using XSAVE variant instructions.
• Efficiently pack objects for fastpath.
• Increase IPI words to 3.
• Support for x2APIC.
• Support larger XSAVE region sizes.
• Change ia32 to use fs register for IPC buffer.
• Update the bootinfo for number of cores.
• Initial support for SMP vt-x.
• Split CPU ID management into mode and general.
• Fix cpuid family/model composition.
• Add X86_64 support.

Implementation improvements

• Several enhancements for both x86 and ARM have been made. Please see the commit log for details.

Upgrade notes

• This release breaks both API and ABI and is not source compatible with the earlier versions. Read more here: https://research.csiro.au/tsblog/introducing-device-untyped-memory-sel4/

Full changelog

Use git log 3.2.0..4.0.0 in https://github.com/seL4/seL4

More details

See the 4.0.0 manual included in the release for detailed descriptions of the new features. Or ask on the mailing list!

Other releases

See the full list of seL4 releases.