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!