1<!-- SPDX-License-Identifier: CC-BY-SA-4.0 --> 2 3# Revision History for seL4 4 5<!-- 6 Document maintainers: Wrap lines in this file at 120 characters. 7 8 Kernel engineers: When making changes to code (rather than documentation or comments) in the kernel repository, 9 include a change item entry here, at the end of the list for the upcoming release, describing the change, and 10 evaluate whether the compatibility breakage level must be promoted as a consequence. As some rules of thumb: 11 * If the change affects only the sources of the kernel (`src/`, `/include`), it is a BINARY-COMPATIBLE change. 12 * If the change adds visible C preprocessor or language symbols in `libsel4/`, it is a BINARY-COMPATIBLE change. 13 * If the change alters existing symbol definitions, types, or implementations in `libsel4/`, it is a 14 SOURCE-COMPATIBLE change. 15 * Otherwise, it is BREAKING. 16--> 17 18The following is a high-level description of changes to the seL4 kernel project, grouped by release. It is aimed at 19engineers who desire a summary of changes in more coarse-grained form than the Git commit history. Each release 20description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BREAKING relative to the previous release. 21 22Further information about [seL4 releases](https://docs.sel4.systems/sel4_release/) is available. 23 24--- 25Upcoming release: BINARY COMPATIBLE 26 27## Changes 28 29 30## Upgrade Notes 31--- 3212.0.0 2020-10-30: BREAKING 33## Changes 34 35 36* Update licensing to reflect project transfer to seL4 Foundation. SPDX tags are now used to identify the licenses for 37 each file in the project. Generally, kernel-level code is licensed under GPLv2 and user-level code under the 2-clause 38 BSD license. 39* Update contribution guidelines: 40 * the seL4 foundation requires DCO process instead of a CLA 41* Functional correctness verification for the RISC-V 64-bit HiFive Unleashed platform configuration 42 (RISCV64_verified.cmake with no fastpath or FPU enabled) 43* Update caveats file: 44 - The recycle operation has been removed 45 - More detail on what versions are verified 46 - Update comments on real time use of seL4 47* Improve seL4 manual. 48 - Fix aarch64 seL4_ARM_PageDirectory object API docs: 49 seL4_ARM_PageDirectory_Map is passed a vspace cap not an upper page directory cap. 50 - Increase documentation coverage for Arm object invocations 51 - Rework introduction of system calls in Kernel Services and Objects chapter. 52 - Improve discussion of Receive and Wait syscall behaviour between MCS and non-MCS systems. 53 - Explicitly mention grantreply rights in the exceptions section. 54 - Document schedcontext size_bits meaning. 55 - Remove metion of system criticality. 56 - Add SchedContext to object size discussion. 57 - Fix initial thread's CNode guard size. 58 - Update BootInfo struct table. 59 - Update padding field in UntypedDesc table 60* Update seL4_DebugSnapshot to provide a CapDL dump of the capability layout of 61 a running system for Arm, x86_64 and riscv32 configurations. 62* KernelBenchmarksTrackUtilisation: 63 - Add feature support for SMP configurations 64 - For each thread also track number of times scheduled, number of kernel entries and amount of cycles spent inside the 65 kernel and also add core-wide totals for each. 66* Add 2 new benchmark utilization syscalls 67 - seL4_BenchmarkDumpAllThreadsUtilisation: Prints a JSON formatted record of total and per-thread utilisation 68 statistics about the system. This currently includes a thread's total cycles scheduled, total number of times 69 scheduled, total cycles spent in the kernel and total number of times entering the kernel and then totals of each 70 for all threads on the current core. 71 - seL4_BenchmarkResetAllThreadsUtilisation: Resets the current counts of every user thread on the current core. 72* Added seL4_DebugPutString libsel4 function for printing a null-terminated string via calling seL4_DebugPutChar(). 73* Introduced a new config flag, KernelInvocationReportErrorIPC, to enable userError format strings to be written to 74 the IPC buffer. Another config bool has been introduced to toggle printing the error out and this can also be set at 75 runtime. LibSel4PrintInvocationErrors is a libsel4 config used to print any kernel error messages reported in the IPC 76 buffer. 77* Repair barriers in clh_lock_acquire (SMP kernel lock). Strengthen the clh_lock_acquire to use release on the 78 atomic_exchange that makes the node public. Otherwise, (on ARM & RISCV) the store to the node value which sets its 79 state to CLHState_Pending can become visible some time after the node is visible. In that window of time, the next 80 thread which attempts to acquire the lock will still see the old state (CLHState_Granted) and enters the critical 81 section, leading to a mutual exclusion violation. 82* Replace all #ifdef header guards with #pragma once directives in libsel4 header files 83* gcc.cmake: 84 - Add option for coloured gcc output. Setting GCC_COLORS in the environment will result in -fdiagnostics-color=always 85 being provided to gcc. Ordinarily gcc would suppress coloured output when ninja redirects its stderr during normal 86 builds. 87 - Remember CROSS_COMPILER_PREFIX across CMake invocations. The variable would become unset in certain contexts. 88 - Add support for Arm cross-compilers on Red Hat distros. 89* Fastpath optimisation: 90 - Reorganise the code layout on Arm. 91 - bitfield_gen: explicit branch predictions. 92 - Optimize instruction cache access for fastpath. 93* Extend Clang support to all kernel configurations. Support targets LLVM versions between 9 and 11. 94* hardware_gen.py: Add elfloader output target for hardware_gen script. This generates header files describing the 95 platform's CPU configuration as well as device information such as compatibility strings and memory regions to the 96 elfloader that are consistent with the kernel's own definitions. 97* Fix bootinfo allocation bug when user image pushed against page directory boundary. The bootinfo is mapped in at the 98 end of the user image in the initial thread's vspace. The kernel initialisation code wasn't calculating the 99 bootinfo size correctly which could lead to a kernel fault when trying to map the bootinfo in when the parent page 100 table object hadn't been allocated. 101* Use autoconf definition for `RetypeMaxObjects` in <sel4/types.h>. This ensures that the definition stays consistent 102 with what the kernel is configured with. 103* Fix up timers and clock frequencies 104 - Remove beaglebone kernel timer prescaling. Previously the timer frequency was incorrectly set to to half (12MHz) its 105 configured frequency (24MHz). 106 - Set TX1 kernel timer frequency config to 12MHz and not 19.2MHz as this is the standard frequency of the input clock 107 source (m_clock). 108 - Set KZM kernel timer frequency config to 35MHz and not 18.6MHz based on sampling the timer frequency. 109 - imx31: add missing dts entry for the epit2 timer. 110 - Set non-mcs i.MX6 kernel timer frequency config to 498MHz and not 400MHz as this is based on the frequency of the 111 input clock source (PLL1) 112 - Zynq7000: Set kernel timer frequency to 320MHz. 113 - Qemu-arm-virt: Set kernel timer frequency to 6.25MHz. 114* Do not generate data symbols for enums in libsel4 as they end up as bss symbols and cause linker errors on newer 115 compiler versions. 116* Update padding field definition in seL4_UntypedDesc to make the struct word aligned. Previously, this struct wasn't 117 correctly word aligned on 64-bit platforms. This change removes the padding1 and padding2 fields and replaces them 118 with a padding field that is a variable number of bytes depending on the platform. 119* Add GitHub actions scripts. These scripts replicate internal CI checks directly on GitHub 120 121### MCS 122 123* Stop scheduling contexts from being bound to tcb's that already have scheduling contexts. 124* Fix x86 `KERNEL_TIMER_IRQ` definition. Previously, MCS preemption point handling would check the wrong interrupt on 125 x86 platforms. 126* smp: tcb affinity modification bug. When changing the affinity of a thread on a remote core, the reschedule 127 operation wasn't being performed. 128* Allow `replyGrant` for fault handlers. The MCS kernel so far insisted on full grant rights for fault handler caps, 129 but replyGrant is sufficient and consistent with the default kernel config. 130* All scheduling contexts compare their time with time in assigned core instead of currently executing core. 131* Prevent recursion on timeout faults by suspending a passive server that receives a timeout fault. 132* Add KernelStaticMaxBudgetUs to bound the time the user provides to configure scheduling contexts to avoid malicious 133 or erroneous overflows of the scheduling math. Make the default max period/budget 1 hour. 134* rockpro64: enable mcs configurations 135 136### Arm 137 138* arm: Add seL4_BenchmarkFlushL1Caches syscall to manually flush L1 caches in benchmark configurations. 139* New fault type when running in Arm hypervisor mode: seL4_Fault_VPPIEvent 140 - The kernel can keep track of IRQ state for each VCPU for a reduced set of PPI IRQs and deliver IRQ events as 141 VCPU faults for these interrupt numbers. 142 - Additionally a new VCPU invocation is introduced: seL4_ARM_VCPU_AckVPPI. 143 This is used to acknowledge a virtual PPI that was delivered as a fault. 144* Virtualise Arm Timer and VTimer interrupts to support sharing across VCPUs. 145 - A VCPU will now save and restore VTimer registers for the generic timer and also deliver a VTimer IRQ via a 146 seL4_Fault_VPPIEvent fault. This enables multiple VCPUs bound to the same physical core to share this device. 147* Build config option for whether WFE/WFI traps on VCPUs when running in Arm hypervisor mode 148* Arm: Add VMPIDR and VMPIDR_EL2 registers to VCPU objects for programming a VCPU's 'Virtualization Multiprocessor 149 ID Register' on aarch32 and aarch64. 150* Arm, vcpu, smp: Remote IPI call support for VIRQS. Injecting a VIRQ into a vcpu running on a different core will 151 IPI the remote core to perform the IRQ injection. 152* zynqmp: Disable hardware debug APIs as the platform doesn't support kernel hardware debug API. 153* zynqmp: Add support for aarch32 hyp 154* Gicv3: include cluster id when sending ipis. 155* qemu-arm-virt: 156 - Generate platform dtb based on KernelMaxNumNodes config value. 157 - Reserve the first 512MiB of Ram as device untyped for use in virtualization configurations. 158 159#### Aarch32 160 161* Moved TPIDRURO (PL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means 162 changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs. 163* aarch32: Restrict cache flush operation address range in hyp mode. It's required that cache flushing in hyp mode 164 is performed through the kernel window mapping as the kernel is unable to flush addresses outside of this mapping 165 without causing an access fault. 166* arm_hyp: Move PGD definitions out of libsel4 as they don't correspond to any public interfaces and are only used 167 internally by the kernel to manage its own address space. 168 169#### Aarch64 170 171* aarch64: Fix a bug where saving ELR_EL1 when managing a VCPU object was reading from ELR_EL1 instead of writing to it. 172* aarch64: Fix a bug where saving FAR_EL1 when managing a VCPU object was only writing to the low 32 bits of the 64-bit 173 FAR_EL1 register. 174* aarch64: Add missing faults to seL4_getArchFault. seL4_getArchFault is a libsel4 helper that constructs fault messages 175 out of the IPC buffer message registers but it wasn't aware of all possible fault types. 176* aarch64,vcpu: Add CNTKCTL_EL1 register to `vcpu_t`. This register tracks timer delegation to EL0 from EL1 and 177 needs to be switched for different VCPUs. 178* aarch64: Adds missing vcpu cases for some aarch64-specific functions on capabilities. 179* cortex-a53,hyp: Reduce seL4_UserTop when on a cortex-a53 platform and KernelArmHypervisorSupport is set. 180 - This is because the kernel uses the last slot in the top level VSpace object for storing the assigned VMID and so 181 any addresses that are addressed by the final slot are not accessible. This would apply to any CPU that have 40bit 182 stage 2 translation input address. 183* Arm SMMUv2 kernel API and TX2 smmuv2 driver. This supports using an SMMU to provide address translation and memory 184 protection for device memory access to platforms that implement a compatible Arm SMMUv2 System mmu. The kernel 185 implementation supports using an SMMU to restrict memory access of VM guest pass-through devices, or for isolating 186 devices and their drivers' memory accesses to the rest of a running system. 187 188### x86 189 190* Fix printf typo in `apic_init`. 191* x86_64: Fix PCID feature constant to use the correct bit. 192* Fix interrupt flag reset upon nested interrupt resume, `c_nested_interrupt`. This fixes an issue where ia32 kernels 193 would crash if receiving a nested interrupt. 194 195### RISC-V 196 197* Functional correctness of seL4/RISCV now formally verified at the C level. 198* Hifive: Enable seL4_IRQControl_GetTrigger object method. This method allocates an IRQ handler by ID and whether it is 199 level or edge triggered. Note: HiFive PLIC interrupts are all positive-level triggered. 200* Add search for additonal gcc riscv toolchains if the first one cannot be found. 201* Add support for rocketchip soc. Support Rocketchip SoC maps to Xilinx ZC706 board and ZCU102 board 202* Add support for polarfire soc. 203* Clear reservation state on slowpath exit as the RISC-V ISA manual requires supervisor code to execute a dummy sc 204 instruction to clear reservations "during a preemptive context switch". 205* Pass DTB through to userlevel in extra bootinfo fields similar to on Arm. 206* Use full width of scause to prevent large exception numbers to be misinterpreted as syscalls. 207* Fix page map bug. 208 - Previously, it was possible in decodeRISCVFrameInvocation for the rwx rights of the new PTE to become 000 after 209 masking with cap rights. This would turn the frame PTE into a page table PTE instead, and allow the user to create 210 almost arbitrary mappings, including to kernel data and code. The defect was discovered in the C verification of the 211 RISC-V port. 212* Remove seL4_UserException_FLAGS. This field was unused and was never set to anything by the kernel. 213* Add FPU config options for RISCV 214 - Two options, KernelRiscvExtD and KernelRiscvExtF, are added to represent the D and F floating-point extensions. 215 KernelHaveFPU is enabled when the floating-point extensions are enabled. The compiler ABI will also be changed to 216 lp64d for hardfloat builds. 217* Add RISCV64_MCS_verified.cmake config for in-progress MCS verification 218* riscv32: Remove incorrectly provided constants for 512MiB 'huge pages' which is not part of the specification. 219* riscv: Lower .boot alignment to 4KiB. This makes the final kernel image more compact. 220 221## Upgrade Notes 222 223* The project's licensing updates don't change the general licensing availability of the sources. 224 More information can be found: https://github.com/seL4/seL4/blob/master/LICENSE.md 225* Any references to the padding1 or padding2 fields in seL4_UntypedDesc require updating to 226 the new padding field. It is expected that these fields are unused. 227* Any platforms that have had changed kernel timer frequencies will see different scheduling 228 behavior as kernel timer ticks will occur at different times as kernel ticks are configured 229 in microseconds but then converted to timer ticks via the timer frequency. Any time-sensitive 230 programs may need to be re-calibrated. 231* Any riscv32 programs that were using the constants RISCVGigaPageBits or seL4_HugePageBits will 232 see a compilation error as the constants have been deleted as they aren't supported in the riscv32 spec. 233* Any riscv programs that refer to the seL4_UserException_FLAGS field will need to remove this reference. This field was 234 never initialised by the kernel previously and has now been removed. 235* Any riscv programs using the LR/SC atomics instructions will see reservations invalidated after kernel entries. It is 236 expected that this will not require any changes as reservations becoming invalid is normal behavior. 237* On cortex-a53 platforms when KernelArmHypervisorSupport is set have 1 less GiB of virtual memory addresses available 238 or 2GiB less on TX2 with the SMMU feature enabled. This is captured by the change in definition of the seL4_UserTop 239 constant that holds the larges virtual address accessible by user level. 240* On aarch32 the TPIDRURO register(PL0 Read-Only Thread ID register) has been removed from the VCPU object and added to 241 the TCB object. A VCPU is typically bound to a TCB so after updating the access, a thread with a VCPU attached will 242 still support having a TPIDRURO managed. 243* On Arm hypervisor configurations, PPI virtual timer interrupts are now delivered via seL4_Fault_VPPIEvent faults and 244 it is not possible to allocate an interrupt handler for these interrupts using the normal interrupt APIs. A VPPI 245 interrupt is received via receiving a fault message on a VCPU fault handler, and acknowledged by an invocation on 246 the VCPU object. VPPI interrupts that target a particular VCPU can only be generated while the VCPU thread is 247 executing. 248 249--- 25011.0.0 2019-11-19: BREAKING 251 252## Changes 253 254* Add GrantReply access right for endpoint capabilities. 255 - seL4_Call is permitted on endpoints with either the Grant or the GrantReply access rights. 256 - Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right. 257* `seL4_CapRights_new` now takes 4 parameters 258* seL4_CapRightsBits added to libsel4. seL4_CapRightsBits is the number of bits 259 to encode seL4_CapRights. 260* `seL4_UserTop` added 261 - a new constant in libsel4 that contains the first virtual address unavailable to 262 user level. 263* Add Kernel log buffer to aarch64 264* Support added for Aarch64 hypervisor mode (EL2) for Nvidia TX1 and TX2. This is not verified. 265* Support for generating ARM machine header files (memory regions and interrupts) based on a device tree. 266* Support added for ARM kernel serial driver to be linked in at build time based on the device tree compatibility string. 267* Support added for compiling verified configurations of the kernel with Clang 7. 268* RISC-V: handle all faults 269 - Pass all non-VM faults as user exceptions. 270* arm-hyp: pass ESR in handleUserLevelFault 271* aarch64: return ESR as part of user level fault 272* Created new seL4_nbASIDPoolsBits constant to keep track of max nb of ASID pools. 273* Support added for Hardkernel ODROID-C2. 274* Added extended bootinfo header for device tree (SEL4_BOOTINFO_HEADER_FDT). 275* Support added for passing a device tree from the bootloader to the root task on ARM. 276* Add seL4_VSpaceBits, the size of the top level page table. 277* The root cnode size is now a minimum of 4K. 278* Hifive board support and RISC-V external interrupt support via a PLIC driver. 279* Update seL4_FaultType size to 4bits. 280* Fix seL4_MappingFailedLookupLevel() for EPTs on x86. 281 - add SEL4_MAPING_LOOKUP_NO_[EPTPDPT, EPTPD, EPTPT] which now correspond to 282 the value returned by seL4_MappingFailedLookupLevel on X86 EPT mapping calls. 283* BeagleBone Black renamed from am335x to am335x-boneblack. 284* Supported added for BeagleBone Blue (am335x-boneblue). 285* Remove IPC Buffer register in user space on all platforms 286* Add managed TLS register for all platforms 287* Add configurable system call allowing userspace to set TLS register without capability on all platforms. 288* Non-hyp support added for Arm GICv3 interrupt controller. 289* Add initial support for i.MX8M boards. 290 - Support for i.MX8M Quad evk AArch64 EL2 and EL1, AArch32 smode only is accessible via the imx8mq-evk platform. 291 - Support for i.MX8M Mini evk AArch64 EL2 and EL1, AArch32 smode only is accessible via the imx8mm-evk platform. 292* Add FVP platform with fixed configuration. This currently assumes A57 configuration described in tools/dts/fvp.dts. 293* Arm SMP invocation IRQControl_GetTriggerCore added 294 - Used to route a specify which core an IRQ should be delivered on. 295* Kernel log buffer: Specify on which core an IRQ was delivered. 296* Add new seL4_DebugSendIPI syscall to send arbitrary SGIs on ARM when SMP and DEBUG_BUILD are activated. 297* Support for aarch64-hyp configurations with 40-bit physical addresses (PA) added. 298 - The aarch64 api now refers to VSpaces rather than PageGlobalDirectories, 299 as depending on the PA the top level translation structure can change. 300 - all `seL4_ARM_PageGlobalDirectory` invocations are now `seL4_ARM_VSpace` invocations. 301 - new constants 'seL4_ARM_VSpaceObject` and `seL4_VSpaceIndexBits`. 302* Merged MCS kernel feature. 303 - this is not verified and is under active verification. 304 - The goals of the MCS kernel is to provide strong temporal isolation and a basis for reasoning about time. 305* Moved aarch64 kernel window 306 - aarch64 kernel window is now placed at 0, meaning the kernel can access memory 307 below where the kernel image is mapped. 308* aarch64: Moved TPIDRRO_EL0 (EL0 Read-Only Thread ID register) to TCB register context from VCPU registers. This means 309 changes to this register from user level have to go via seL4_TCB_Write Registers instead of seL4_ARM_VCPU_WriteRegs. 310* Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page 311 without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same 312 result. The ARCH_Page_Remap invocation has been removed from all configurations. 313* riscv64: Experimental SMP support for RISCV64 on HiFive. 314* Support added for QEMU ARM virt platform, with 3 CPUs: cortex-a15, cortex-a53 and cortex-a57 315 - PLATFORM=qemu-arm-virt 316 - ARM_CPU={cortex-a15, cortex-a53, cortex-a57} 317 - QEMU_MEMORY=1024 (default) 318* Support added for rockpro64. 319* RISCV: Add support for Ariane SoC 320* Unify device untyped initialisation across x86, Arm and RISC-V 321 - Access to the entire physical address range is made available via untypes. 322 - The kernel reserves regions that user level is not able to access and doesn't hand out untypeds for it. 323 - Ram memory is part of this reservation and is instead handed out as regular Untypeds. 324 - Memory reserved for use by the kernel or other reserved regions are not accessible via any untypeds. 325 - Devices used by the kernel are also not accessible via any untypeds. 326 327## Upgrade Notes 328 329* Usages of Endpoints can now use seL4_Call without providing Grant rights by downgrading the Grant to GrantReply 330* The kernel no longer reserves a register for holding the address of a thread's IPC buffer. It is now expected that the 331 location of the IPC buffer is stored in a __thread local variable and a thread register is used to refer to each 332 thread's thread local variables. The sel4runtime is an seL4 runtime that provides program entry points that setup 333 the IPC buffer address and serves as a reference for how the IPC buffer is expected to be accessed. 334* All `seL4_ARM_PageGlobalDirectory` invocations need to be replaced with `seL4_ARM_VSpace`. 335* Usages of ARCH_Page_Remap can be replaced with ARCH_Page_Map and require the original mapping address to be provided. 336* Device untypeds are provided to user level in different sizes which may require more initial processing to break them 337 down for each device they refer to. 338 339--- 34010.1.1 2018-11-12: BINARY COMPATIBLE 341 342## Changes 343 * Remove theoretical uninitialised variable use in infer_cpu_gic_id for binary translation validation 344 345## Upgrade Notes 346 * 10.1.0 has a known broken test in the proofs. 10.1.1 fixes this test. 347 348--- 34910.1.0 2018-11-07: SOURCE COMPATIBLE 350 351## Changes 352 353 * structures in the boot info are not declared 'packed' 354 - these were previously packed (in the GCC attribute sense) 355 - some field lengths are tweaked to avoid padding 356 - this is a source-compatible change 357 * ARM platforms can now set the trigger of an IRQ Handler capability 358 - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability 359 and set the trigger (edge or level) in the interrupt controller. 360 * Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) 361 * AARCH64 support added for raspberry pi 3 platform. 362 * Code generation now use jinja2 instead of tempita. 363 * AARCH32 HYP support added for running multiple ARM VMs 364 * AARCH32 HYP VCPU registers updated. 365 * A new invocation for setting TLSBase on all platforms. 366 - seL4_TCB_SetTLSBase 367 * Kbuild/Kconfig/Makefile build system removed. 368 369--- 37010.0.0 2018-05-28: BREAKING 371 372- Final version of the kernel which supports integration with Kbuild based projects 373- Future versions, including this one, provide a CMake based build system 374 375For more information see https://docs.sel4.systems/Developing/Building. 376 377## Changes 378 379 * x86 IO ports now have an explicit IOPortControl capability to gate their creation. IOPort capabilities may now only 380 be created through the IOPortControl capability that is passed to the rootserver. Additionally IOPort capabilities 381 may not be derived to have smaller ranges and the IOPortControl will not issue overlapping IOPorts 382 * 32-bit support added for the initial prototype RISC-V architecture port 383 384## Upgrade Notes 385 386 * A rootserver must now create IOPort capabilities from the provided IOPortControl capability. As IOPorts can not 387 have their ranges further restricted after creation it must create capabilities with the final desired granularity, 388 remembering that since ranges cannot overlap you cannot issue a larger and smaller range that have any IO ports 389 in common. 390 391--- 3929.0.1 2018-04-18: BINARY COMPATIBLE 393 394## Changes 395 * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs 396 which use any of the following functions may break, if the program relies on these functions to mask the 397 `label` field to the previous width of 20 bits. 398 - `seL4_MessageInfo_new` 399 - `seL4_MessageInfo_get_label` 400 - `seL4_MessageInfo_set_label` 401 * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or 402 or multicore support on the Spike simulation platform. There is *no verification* for this platform. 403 404## Upgrade Notes 405--- 4069.0.0 2018-04-11: BREAKING 407 408= Changes = 409 * Debugging option on x86 for syscall interface to read/write MSRs (this is an, equally dangerous, alternative to 410 dangerous code injection) 411 * Mitigation for Meltdown (https://meltdownattack.com) on x86-64 implemented. Mitigation is via a form of kernel 412 page table isolation through the use of a Static Kernel Image with Microstate (SKIM) window that is used for 413 trapping to and from the kernel address space. This can be enabled/disabled through the build configuration 414 depending on whether you are running on vulnerable hardware or not. 415 * Mitigation for Spectre (https://spectreattack.com) on x86 against the kernel implemented. Default is software 416 mitigation and is the best performing so users need to do nothing. This does *not* prevent user processes from 417 exploiting each other. 418 * x86 configuration option for performing branch prediction barrier on context switch to prevent Spectre style 419 attacks between user processes using the indirect branch predictor 420 * x86 configuration option for flushing the RSB on context switch to prevent Spectre style attacks between user 421 processes using the RSB 422 * Define extended bootinfo header for the x86 TSC frequency 423 * x86 TSC frequency exported in extended bootinfo header 424 * `archInfo` is no longer a member of the bootinfo struct. Its only use was for TSC frequency on x86, which 425 can now be retrieved through the extended bootinfo 426 * Invocations to set thread priority and maximum control priority (MCP) have changed. 427 - For both invocations, users must now provide a TCB capability `auth` 428 - The requested MCP/priority is checked against the MCP of the `auth` capability. 429 - Previous behavior checked against the invoked TCB, which could be subject to the confused deputy 430 problem. 431 * seL4_TCB_Configure no longer takes prio, mcp as an argument. Instead these fields must be set separately 432 with seL4_TCB_SetPriority and seL4_TCB_SetMCPriority. 433 * seL4_TCB_SetPriority and seL4_TCB_SetMCPriority now take seL4_Word instead of seL4_Uint8. 434 - seL4_MaxPrio remains at 255. 435 * seL4_TCB_SetSchedParams is a new method where MCP and priority can be set in the same sytsem call. 436 * Size of the TCB object is increased for some build configurations 437 438= Upgrade notes = 439 * seL4_TCB_Configure calls that set priority should be changed to explicitly call seL4_TCB_SetSchedParams 440 or SetPriority 441 * seL4_TCB_Configure calls that set MCP should be changed to explicitly call seL4_TCB_SetSchedParams 442 or seL4_TCB_SetMCPriority 443 444--- 4458.0.0 2018-01-17 446 447= Changes = 448 * Support for additional zynq platform Zynq UltraScale+ MPSoC (Xilinx ZCU102, ARMv8a, Cortex A53) 449 * Support for multiboot2 bootloaders on x86 (contributed change from Genode Labs) 450 * Deprecate seL4_CapData_t type and functions related to it 451 * A fastpath improvement means that when there are two runnable threads and the target thread is the highest priority 452in the scheduler, the fastpath will be hit. Previously the fastpath would not be used on IPC from a high priority 453thread to a low priority thread. 454 * As a consequence of the above change, scheduling behaviour has changed in the case where a non-blocking IPC is sent 455between two same priority threads: the sender will be scheduled, rather than the destination. 456 * Benchmarking support for armv8/aarch64 is now available. 457 * Additional x86 extra bootinfo type for retrieving frame buffer information from multiboot 2 458 * Debugging option to export x86 Performance-Monitoring Counters to user level 459 460= Upgrade notes = 461 * seL4_CapData_t should be replaced with just seL4_Word. Construction of badges should just be `x` instead of 462 `seL4_CapData_Badge_new(x)` and guards should be `seL4_CNode_CapData_new(x, y)` instead of 463 `seL4_CapData_Guard_new(x, y)` 464 * Code that relied on non-blocking IPC to switch between threads of the same priority may break. 465 466--- 4677.0.0 2017-09-05 468 469= Changes = 470 * Support for building standalone ia32 kernel added 471 * ia32: Set sensible defaults for FS and GS selectors 472 * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0 473 * More seL4 manual documentation added for aarch64 object invocations 474 * Default NUM_DOMAINS set to 16 for x86-64 standalone builds 475 * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change ''' 476 * Add a CMake based build system 477 * x86: Increase TCB size for debug builds 478 * libsel4: x86: Remove nested struct declarations ''' This is a source code level breaking change ''' 479 * Bugfix: x86: Unmap pages when delete non final frame caps 480 481= Upgrade notes = 482 * This release is not source compatible with previous releases. 483 * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already 484 been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types 485 will need to be updated to reflect this change. 486 * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if 487 VESA BIOS Extensions (VBE) information is being used. 488 489= Known issues = 490 * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform, 491 which is a non verified configuration of the kernel. We are working on fixing this problem, and will likely do a 492 point release once it is fixed. 493 494--- 495For previous releases see https://docs.sel4.systems/sel4_release/ 496