Upcoming release planned
by Mcleod, Kent (Data61, Kensington NSW)
I'm announcing that we are planning a new versioned release of seL4,
capDL and CAmkES in about 3 weeks - around 11 November.
We want to provide an opportunity for people to report issues or
provide patches that can be fixed/incorporated for the versioned
The last versioned release occurred almost 12 months ago and we plan
on returning to a shorter release cycle of several weeks per cycle.
Feel free to raise new issues across our GitHub repositories and we
will also try to address any currently outstanding issues that have
Here is a highlight list of what changes are going to be in the
upcoming versioned release:
- Add GrantReply access right for endpoint capabilities. `seL4_Call`
is permitted on endpoints with either the Grant or the GrantReply
access rights. Capabilities can only be transferred in a reply message
if receiver's endpoint capability has the Grant right. The GrantReply
access right allows endpoints to be configured for two-way
communication without also providing the right to transfer authority
via capability transfer.
- Merging of the mixed-criticality scheduling (MCS) branch into
master. Previously the MCS branch only received versioned releases.
Merging it into master under a build configuration (KernelIsMCS) makes
it easier to keep up to date with changes to master and other
tooling/libraries in-between versioned releases. Verification work is
- Continued development of the newly added RISC-V platform to support
- Auto-generation of Arm and RISC-V kernel platform definitions from a
provided devicetree as well as support for passing a devicetree to the
root task via the seL4_BootInfo structure. Interrupt controllers,
timers and other devices required by the kernel can also be selected
in the devicetree provided that the kernel already has a compatible
- Support for AArch64 hypervisors is in active development with
initial support for Cortex-A53 and Cortex-A57 cores
- De-duplicating kernel platform configurations and code in order to
reduce the effort required to support additional platforms.
- New platforms added: BeagleBone Blue, Hardkernel ODROID-C2,
Freescale i.MX8M, i.MX8M Mini, Arm FVP (based on
foundation-v8-gicv3.dts), QEMU ARM virt platform (with 3 CPUs:
cortex-A15, cortex-A53 and cortex-A57) and possibly PINE64 ROCKPro64.
- Implement RFC-3: Cross-platform thread-local storage (TLS) support.
https://sel4.atlassian.net/browse/RFC-3. This provides a way for a
thread to access or modify a thread-specific pointer without requiring
a capability to itself. On architectures that don't provide
unprivileged write access to this pointer a new syscall
`seL4_SetTLSBase` is added that performs this operation. The kernel no
longer reserves a register for holding a thread's IPC buffer and it is
the thread's responsibility for managing this. `libsel4` declares a
pointer to a thread's IPC buffer using a `__thread` keyword and a new
user-level library `sel4runtime` can be used to provide a minimal
supporting runtime. Additionally, the IPC buffer's userData field is
no longer used for holding a pointer to the IPC buffer.
- Better SMP Arm IRQ handling: Support is added for creating IRQ
handler capabilities for core-local interrupts (PPIs) for each core
and for also specifying a target core for global interrupts (SPIs) via
the new invocation `IRQControl_GetTriggerCore`.
- Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was
used for updating the mapping attributes of a page without changing
its virtual address. Now ARCH_Page_Map can be performed on an existing
mapping to achieve the same result. The ARCH_Page_Remap invocation has
been removed from all configurations.
- Support for compiling the kernel with Clang.
For a more complete list see the CHANGES file in the seL4 repository.
- Support for the new seL4 Endpoint GrantReply access right for CAmkES
connector types. This allows multi-sender/single-receiver connectors
such as `seL4RPCCall` that don't also provide the ability for
arbitrary capability transfer from sender to receiver. Previously the
`seL4RPC` connector was used instead of `seL4RPCCall` to create an
Endpoint without a Grant right. This used a combination of `seL4_Send`
and `seL4_Wait` to communicate without the ability for capability
transfer, however this only supports a single sender and single
- Better support for configuring components with a provided
devicetree. This support includes adding a seL4DTBHardware connector
that can be used instead of seL4HardwareMMIO and seL4HardwareInterrupt
and can be used to extract IRQs and MMIO register information out of
the devicetree node rather than specifying the info directly. This
connector can also be used to access a devicetree within a component
at for querying further device information. There is also a connector
seL4VMDTBPassthrough that can be used for specifying devices to pass
through to a `camkes-arm-vm` VM component.
- CapDL Refinement framework. These are generated Isabelle proof
scripts to prove that the generated capDL respects the isolation
properties expected from its CAmkES system specification. Only the
AARCH32 platform is supported. The generated capDL is a specification
of seL4 objects and capabilities that will implement the CAmkES system
specification. This specification is then given to a system
initialiser to create the objects and capabilities and load the
- Support for RISC-V systems.
capDL refers to the capability distribution language and tools
contained in https://github.com/seL4/capdl. CAmkES uses these tools
for generating a capDL specification and then uses the
`capdl-loader-app` as it's seL4 root task for initialising the system.
As we are in the process of developing additional loaders we are going
to start providing versioned releases of the capDL set of tools.
Changes since the last seL4 release:
- Support for the new seL4 Endpoint GrantReply access rights in the
CapDL spec. Endpoint capabilities in the capDL spec can now have Read,
Write, Grant and GrantReply rights.
- Static Untyped allocation of spec objects. This is support for
performing offline pre-allocation of spec objects to the Untyped
objects that are expected to be provided in the seL4_BootInfo by the
kernel. Having a static allocation of spec objects to Untypeds allows
for more simple loaders that do not have to perform resource
allocation during initialisation. This feature is optional and a spec
is still valid if objects aren't allocated from Untyped objects.
- Support for loading RISC-V systems.