Hi all,
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 release.
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 been neglected.
Here is a highlight list of what changes are going to be in the upcoming versioned release:
## seL4
- 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 still on-going.
- Continued development of the newly added RISC-V platform to support in-progress verification.
- 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 driver.
- 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.
## CAmkES
- 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 receiver.
- 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 system.
- Support for RISC-V systems.
## capDL
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.