[seL4] RELEASE: Announcing seL4 4.0.0

Parthasarathi.Susarlaajay at data61.csiro.au Parthasarathi.Susarlaajay at data61.csiro.au
Tue Dec 13 13:40:10 AEDT 2016

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
* 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.
  + 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

The release tarballs can be directly downloaded from:

[259d9eadaddef579c2b98b91cf40d13a  4.0.0.tar.gz]

The manual for this release can be downloaded here: 

* 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
E parthasarathi.susarla at data61.csiro.au

CSIRO's Digital Productivity business unit and NICTA have joined forces
to create digital powerhouse Data61

More information about the Devel mailing list