diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 60190ac54..17bc5d5bf 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -12,6 +12,8 @@ on: branches: [main] paths-ignore: - '**.md' + - 'platforms.yml' + - '.linkcheck-ignore.yml' tags: # Run on version tags, for releases. - '*.*.*' diff --git a/.github/workflows/pr.yml b/.github/workflows/pr.yml index 12e9d5028..8593a4ef0 100644 --- a/.github/workflows/pr.yml +++ b/.github/workflows/pr.yml @@ -6,7 +6,14 @@ name: PR -on: [pull_request, workflow_dispatch] +on: + workflow_dispatch: + + pull_request: + paths-ignore: + - '**.md' + - 'platforms.yml' + - '.linkcheck-ignore.yml' jobs: pr-checks: diff --git a/CHANGES.md b/CHANGES.md index 2d2659b1b..2e2d95e47 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,5 +1,136 @@ # Revision History for Microkit +## Release 2.3.0 + +This release contains quite a few new features: + + * x86_64 IOMMU support (this entails a breaking change) + * seL4_BootInfo support, for reading runtime parameters on x86_64 + * Various improvements to x86_64 virtual machines, such as being able to + stop/start their execution. + * Support for 'Cap Sharing' to give PDs access to specific TCBs or SCs, + useful for userspace schedulers. + * Support for the seL4 Domain Scheduler. + +There are also a variety of bug fixes, especially for x86_64 systems, and +support for two new boards. + +### Breaking changes + +* x86_64 systems are now built with the IOMMU turned on by default, as we have + added new syntax to allow for the IOMMU to be configured (see below). + However, previously the IOMMU was disabled in seL4, so systems which did DMA + on x86_64 will now *stop working* without specifying the IOMMU setup. + +* x86_64 IOAPIC IRQs had an inverted polarity; `polarity="low"` became high + and `polarity="high"` became low. + +* vCPUs now default to the same core as the VMM, instead of core 0. If you + were relying on this behaviour, you should explicitly specify core 0. + +* PCI 'bus:dev:func' syntax is no longer supported, use the correct 'bus:dev.func' + syntax instead. This was an implementation bug which was more permissive + than it was supposed to be. + +* Virtual Machines on x86_64: + + * No longer support budget/period/priority. This did not work previously, + as they share a TCB/SC with the VMM. + + * The VMM on x86_64 cannot have children, nor receive PPCs. + This was previously allowed but had several complex restrictions (such as + not receiving messages after a `vmenter`) so have been disallowed. + +* If you were not using the `libmicrokit` linker script (e.g. rust-seL4 users), + the `__sel4_ipc_buffer_obj` is no longer declared in the linker script, and + is instead allocated by the tool at a fixed virtual address above the stack + which is now reserved. If you were assuming a specific virtual address for the + IPC buffer, this would be broken. + +### Feature changes + +* Update to 16.0.0 release of seL4. + +* Support an 'fpu' attribute on protection domains, following [RFC-18]( + https://sel4.github.io/rfcs/implemented/0180-fpu-switching.html), which allows + for FPU access to be disabled on a per-PD basis. + +* The debug-only (unverified) HardwareDebugAPI has been enabled and is available + on most x86_64 and AArch64 platforms. + +* A new 'cap sharing' feature. The SDF now supports a `` element and + support for placing caps to TCBs, SchedContexts, and VSpaces of other PDs + into the CSpace of the current PD. This can be useful for user space schedulers + that are not the fault-handlers (i.e. use parent-child hierarchy). + +* It is now possible to turn x86 vCPUs (VMs) on or off. + Use the new `microkit_vcpu_x86_on` and `microkit_vcpu_x86_off` APIs + +* AArch64 EL1 (non-hypervisor) platforms are now supported. + +* There is a new (experimental) `--viper-output` argument to the tool, which + is part of some new (experimental) verification work of Microkit PDs using + the [Viper tools from ETH Zürich](http://viper.ethz.ch). + +* Microkit PDs are now a 2-level CSpace. This should not have any impact on + users. + +* It is now possible to create memory regions that are prefilled with bootinfo + from the capDL initialiser. This includes the VBE, MBMAP, ACPI RSDP, Framebuffer, + and TSC frequency types exported by seL4. + +* New function `microkit_pd_resume()` which resumes a stopped child PD. Previously, + only stop and start (which does resume but requires a program counter) existed. + +* New support for configuring the IOMMU on x86_64 systems with the + `` element. See the `x86_64_iommu_dma_test` example packaged + in the SDK for more details, as well as the manual section on IOMMU. + Only 4KiB pages are supporting for the IOMMU due to kernel limitations. + +* Support for the seL4 domain schedule now that the [RFC-20 Runtime Schedules]( + https://sel4.github.io/rfcs/implemented/0200-domain-schedules.html) has been + added to seL4. This is useful for systems which want isolated subsystems + with limited information flow between them. + +### Bug fixes + +* TQMA8XQP1GB loader address has been fixed as it was collided with reserved + regions in memory. +* IOAPIC IRQ polarity was inverted. +* The loader now only maps in the loader memory, UART, and kernel regions, as + otherwise (instruction) speculative accesses to device memory can occur. + Please see [PR 464 for more details](https://github.com/seL4/microkit/pull/464). +* A `microkit_deferred_notify()` or `microkit_deferred_irq_ack()` would be + lost if you sent a reply from a `protected()` call, or from a `fault()` handler. + Now we perform `seL4_Send` on the Notification or IRQHandler capability + before replying to the PPC or Fault. +* A bug with [high-address regions allocated the wrong memory]( + https://github.com/seL4/rust-sel4/issues/319) in the capDL initialiser was + fixed. +* A bug with certain systems that caused the Microkit tool to panic with the + below message has been fixed. + + ``` + thread 'main' (414114) panicked at tool/microkit/src/capdl/allocation.rs:225:17: + assertion `left == right` failed + ``` + +### Board support + +* 'stm32mp2' for the STM32MP2 evaluation board. +* 'qemu_virt_aarch64_el1' for QEMU/KVM on Linux AArch64 hosts (which don't support + nested virtualisation). + +### Notes for developers + +* There is a new `--override-kernel` option to the tool that allows one to + use an SDK build of Microkit but with a different seL4 kernel ELF. +* We now have basic CI that runs Microkit images on real hardware. +* We now recommend the use of the [Google repo-manifest 'microkit-manifest']( + https://github.com/seL4/microkit-manifest) which tracks the supported version + of seL4 to be used for testing the Microkit. It also records the latest build + of the main branch which passed CI. + ## Release 2.2.0 This release contains various bug fixes, minor features, and new board support. diff --git a/Cargo.lock b/Cargo.lock index 1d941e334..05b6a61e9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -135,7 +135,7 @@ checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" [[package]] name = "initialiser" -version = "2.2.0-dev" +version = "2.3.0" dependencies = [ "sel4-capdl-initializer", ] @@ -194,7 +194,7 @@ checksum = "88904434abc2901f197fe8cc55f0445e7ded921dba5911dad2e2b39b48e663c4" [[package]] name = "microkit-tool" -version = "2.2.0-dev" +version = "2.3.0" dependencies = [ "rkyv", "roxmltree", diff --git a/VERSION b/VERSION index 97ade1520..276cbf9e2 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -2.2.0-dev +2.3.0 diff --git a/docs/manual.md b/docs/manual.md index 9fbd2e3bc..654d54a1a 100644 --- a/docs/manual.md +++ b/docs/manual.md @@ -4,7 +4,7 @@ --> --- -title: Microkit User Manual (v2.2.0) +title: Microkit User Manual (v2.3.0) documentclass: article classoption: - english @@ -516,7 +516,8 @@ The format of the system description is described in a subsequent chapter. Usage: - microkit [-h] [OPTIONS] --board BOARD --config CONFIG [--search-path SEARCH_PATH ...] system + microkit [-h] [OPTIONS] --board BOARD --config CONFIG \ + [--search-path SEARCH_PATH ...] system See `microkit --help` for a full list of options. diff --git a/initialiser/Cargo.toml b/initialiser/Cargo.toml index 37559e813..d3f30d5f4 100644 --- a/initialiser/Cargo.toml +++ b/initialiser/Cargo.toml @@ -6,7 +6,7 @@ [package] name = "initialiser" -version = "2.2.0-dev" +version = "2.3.0" edition = "2021" rust-version = "1.88.0" diff --git a/platforms.yml b/platforms.yml index 3f0b3d06a..0588a8110 100644 --- a/platforms.yml +++ b/platforms.yml @@ -14,6 +14,9 @@ # This list is ordered based on the order in what the platforms were added # in. platforms: + - name: stm32mp2 + cmake_plat: stm32mp2 + since: 2.3.0 - name: kria_k26 cmake_plat: zcu102 since: 2.2.0 @@ -94,6 +97,3 @@ platforms: - name: zcu102 cmake_plat: zcu102 since: 1.3.0 - - name: stm32mp2 - cmake_plat: stm32mp257f-ev1 - since: dev diff --git a/tool/microkit/Cargo.toml b/tool/microkit/Cargo.toml index 2e89b1eef..3380f8c8d 100644 --- a/tool/microkit/Cargo.toml +++ b/tool/microkit/Cargo.toml @@ -6,7 +6,7 @@ [package] name = "microkit-tool" -version = "2.2.0-dev" +version = "2.3.0" edition = "2021" rust-version = "1.94.0"