We are pleased to announce the release of 4.0.0 of seL4. Listed below are a few of the key changes in this release:
* 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.
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. * Add seL4_BenchmarkFlushCaches() for arm and ia32. * 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 adress 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.
Please note that this release is not source compatible with earlier releases of seL4, please read https://research.csiro.au/tsblog/introduc ing-device-untyped-memory-sel4/ for more information regarding the changes.
The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/4.0.0.tar.gz
[259d9eadaddef579c2b98b91cf40d13a 4.0.0.tar.gz]
The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf
Contributors: * Adrian Danis * Alexander Boettcher * Amirreza Zarrabi * Anna Lyons * Christian Helmuth * Corey Richardson * Donny Yang * Hesham Almatary * Jeff Waugh * Joel Beeren * Kent McLeod * Kofi Doku Atuah * Matthew Brecknell * Matthew Fernandez * Matt Rice * Rafal Kolanski * Stephen Sherratt * Thomas Sewell * Xin,Gao
Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues
-- Partha Susarla Kernel engineer DATA61 | CSIRO E parthasarathi.susarla@data61.csiro.au www.data61.csiro.au
CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61