From fab6a96ac4c53b60669ceaf69b0569b0a2abccc3 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 24 Jun 2024 19:08:57 +1000 Subject: [PATCH 1/3] CHANGES: rename into CHANGES.md so that GitHub properly renders the file as markdown. Signed-off-by: Gerwin Klein --- CHANGES => CHANGES.md | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename CHANGES => CHANGES.md (100%) diff --git a/CHANGES b/CHANGES.md similarity index 100% rename from CHANGES rename to CHANGES.md From c329084755eb87d6434fc1a093f83e5a5b7a6f9a Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 24 Jun 2024 19:18:52 +1000 Subject: [PATCH 2/3] CHANGES: clean up markdown Make sure text is rendered correctly on different markdown engines. - avoid bare URLs - consistent list indent and spacing - consistent heading style - use level-2 head for release Signed-off-by: Gerwin Klein --- CHANGES.md | 255 ++++++++++++++++++++++++++++++----------------------- 1 file changed, 146 insertions(+), 109 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 42e5305a..ed89362c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,13 +1,14 @@ -Revision history for CAmkES +# Version history for CAmkES -For more information see the release notes at https://docs.sel4.systems/camkes_release/ +For more information see the release notes at -This file should be word wrapped to 120 characters + --- -Upcoming release -## Changes +## Upcoming release + +### Changes * Added RISC-V in `is_64_bit_arch()` * Added helpers `is_arch_arm()` and `is_arch_riscv()` @@ -16,12 +17,15 @@ Upcoming release * Extended DTB interrupt property parsing to support either one value or three values per interrupt. For three values, ignore the first value on RISC-V. -## Upgrade Notes +### Upgrade Notes + --- -camkes-3.10.0 2021-06-10 + +## camkes-3.10.0 2021-06-10 + Using seL4 version 12.1.0 -## Changes +### Changes * Fixed new line generation in `show_attribute_value`. * Added const expression attributes to help convert CAmkES attributes to literals. @@ -42,7 +46,7 @@ Using seL4 version 12.1.0 * Sped up proofs for cdl-refine. * Fixed a CMake argument marshalling bug in the `execute_process_with_stale_check` function. -### Upgrade Notes +#### Upgrade Notes * DMA pools now require an option to be set explicitly to be made to be cache-able. In a `.camkes` CAmkES assembly file, add the following `.dma_pool_cached = True;` in the 'configuration' block to make a component's @@ -50,88 +54,108 @@ Using seL4 version 12.1.0 cached DMA memory from that pool. --- -camkes-3.9.0 2020-10-27 + +## camkes-3.9.0 2020-10-27 + Using seL4 version 12.0.0 -## Changes +### Changes * Enforce system-V stack ordering for libc. - - This allows `musllibc` to initialise and infer the location of `auxv` from `envp` consistently. + - This allows `musllibc` to initialise and infer the location of `auxv` from `envp` consistently. * Add `uint64_t` and `int64_t` types to language. - - This introduced two new data types into the CAmkES language to support larger types. + - This introduced two new data types into the CAmkES language to support larger types. * Remove `elf.h`, now defined in sel4runtime. * Camkes,rumprun: fix tls management implementation: - - `.tdata*` and `.tbss*` linker symbol declarations are suppressed until the final link step. + - `.tdata*` and `.tbss*` linker symbol declarations are suppressed until the final link step. * Fix `generate_seL4_SignalRecv` in `Context.py` and update `rpc-connector.c` template accordingly. - - `seL4SignalRecv` only exists on MCS, split the two calls for compatibility. + - `seL4SignalRecv` only exists on MCS, split the two calls for compatibility. * Save preprocessed camkes files to allow for easier debugging. * CMake: Skip fetching gpio list for pc99 platforms. - - Most PC99 platforms do not have GPIO pins. + - Most PC99 platforms do not have GPIO pins. * Support for running odroidc2 in camkes-arm-vm. Get the IRQ trigger type through the interrupt node in the dts. * Add gpio query engine. - - The engine takes in a YAML file containing a list of GPIO pins and sorts out the 'gpio' queries so that the connector templates for the `seL4GPIOServer` can generate the appropriate structures and functions. + - The engine takes in a YAML file containing a list of GPIO pins and sorts out the 'gpio' queries so that the + connector templates for the `seL4GPIOServer` can generate the appropriate structures and functions. * Add option `CAmkESNoFPUByDefault`. - - By enabling CAmkESNoFPUByDefault camkes will compile all user-level libraries (except musllibc) with compilation flags to not use the FPU. A component that wishes to use the FPU must override the flags itself. + - By enabling CAmkESNoFPUByDefault camkes will compile all user-level libraries (except musllibc) with compilation + flags to not use the FPU. A component that wishes to use the FPU must override the flags itself. * Update `seL4InitHardware` template for api change. - - The configuration name for the list of devices to bind is now a component attribute instead of an interface attribute. + - The configuration name for the list of devices to bind is now a component attribute instead of an interface + attribute. * `libsel4camkes` Support registering DMA memory that is both cached and uncached. * Add sel4bench dependency into `camkes/templates` to allow for cycle counting. * `component.common.c`: use correct label for dma pool. - - When calling `register_shared_variable` from a component context the label needs to be provided. -* Add `seL4DTBHW` connector. This connector variant is similar to `seL4DTBHardware`, but takes a hardware component on the from end. -* `seL4DTBHardware` bug fix, use global interface name. This prevents the allocator from throwing an error when the same interface name is used in a different component. + - When calling `register_shared_variable` from a component context the label needs to be provided. +* Add `seL4DTBHW` connector. This connector variant is similar to `seL4DTBHardware`, but takes a hardware component on + the from end. +* `seL4DTBHardware` bug fix, use global interface name. This prevents the allocator from throwing an error when the same + interface name is used in a different component. * Camkes connector extensions + DMA improvements: - - libsel4camkes: Implement DMA cache for Arm - - component.common.c: Support additional DMA setting. Allow setting the cache and base paddr value of the DMA pool. - - Add single_threaded attribute which when set adds the `seL4SingleThreadedComponent` templates. - - Allow connectors to declare CMake libraries for each end of the connection. This allows a connector to have most of its implementation in a library and only use the template for initialisation and configuration. - - camkes-gen.cmake: Create component target stub. This is equivalent to creating a Component with no customization but would still contain things based on its Camkes definition, such as connector artifacts. + - libsel4camkes: Implement DMA cache for Arm + - component.common.c: Support additional DMA setting. Allow setting the cache and base paddr value of the DMA pool. + - Add single_threaded attribute which when set adds the `seL4SingleThreadedComponent` templates. + - Allow connectors to declare CMake libraries for each end of the connection. This allows a connector to have most of + its implementation in a library and only use the template for initialisation and configuration. + - camkes-gen.cmake: Create component target stub. This is equivalent to creating a Component with no customization but + would still contain things based on its Camkes definition, such as connector artifacts. * Component.common.c: Move init() to C constructor - - Connectors that don't use threads use runtime constructors for their initialisation. + - Connectors that don't use threads use runtime constructors for their initialisation. * Libsel4camkes: camkes_call_hardware_init_modules -Provide this public function for starting hardware modules that have been registered. + - Provide this public function for starting hardware modules that have been registered. * Add `global_rpc_endpoint_badges` macro. - - This macro assigns badges for different connectors that share the global-rpc-endpoint object for a component instance. -* Libsel4camkes: irq backend for global-connectors. This adds a way for calling registered IRQ notification handlers for connectors that don't have their own threads. + - This macro assigns badges for different connectors that share the global-rpc-endpoint object for a component + instance. +* Libsel4camkes: irq backend for global-connectors. This adds a way for calling registered IRQ notification handlers for + connectors that don't have their own threads. * Add seL4DMASharedData connector and add appropriate library functionality in `libsel4camkes`. - - This connector sets up a dataport connector that is added to the DMA pool that the camkes runtime tracks for each component. + - This connector sets up a dataport connector that is added to the DMA pool that the camkes runtime tracks for each + component. * Add support for connector header files and component header templates. - - A connector can now define template header files that will be included by `camkes.h`. Similarly, component header templates will be instantiated and then automatically included by `camkes.h`. + - A connector can now define template header files that will be included by `camkes.h`. Similarly, component header + templates will be instantiated and then automatically included by `camkes.h`. * Support creating TCB pools and assigning domains to them in camkes templates. - - Assign domain IDs for TCBs in the thread pool based on values provided by the config option array values. -* Generalise jinja linter to support non-camkes use cases. The Jinja linter can now be used on any arbitrary Jinja template. -* Add support in `libsel4camkes` for matching interrupts even if they are defined -with different base types. + - Assign domain IDs for TCBs in the thread pool based on values provided by the config option array values. +* Generalise jinja linter to support non-camkes use cases. The Jinja linter can now be used on any arbitrary Jinja + template. +* Add support in `libsel4camkes` for matching interrupts even if they are defined with different base types. * Add interface registration to `libsel4camkes` via `interface_registration.h` as part of the driver framework. -* Revive graph.dot output file for each asssembly. This can be loaded with a -program like `xdot` to view a diagram of the camkes system. +* Revive graph.dot output file for each asssembly. This can be loaded with a program like `xdot` to view a diagram of + the camkes system. * Virtqueues: - - Add virtqueue recieve. - - Set virtqueue size on creation to the number of rings and descriptor tables have. - - Add `virtqueue_get_client_id` macro for automatically assigning client IDs to distinguish different virtqueue channels within a single component instance. - - Link channel ID to name, this allows components to bind to channels via naming them rather than knowing their IDs. -* Add Arm irq type support to `seL4HardwareInterrupt` template. This allows IRQs on Arm to have the trigger mode and target core configured. + - Add virtqueue recieve. + - Set virtqueue size on creation to the number of rings and descriptor tables have. + - Add `virtqueue_get_client_id` macro for automatically assigning client IDs to distinguish different virtqueue + channels within a single component instance. + - Link channel ID to name, this allows components to bind to channels via naming them rather than knowing their IDs. +* Add Arm irq type support to `seL4HardwareInterrupt` template. This allows IRQs on Arm to have the trigger mode and + target core configured. * Allow `size` to be number as well as a string in `marshal.c` template. -* Add `global_endpoint_badges` macro used by the global-endpoints mechanism to assign badge -values based on a full system composition. +* Add `global_endpoint_badges` macro used by the global-endpoints mechanism to assign badge values based on a full + system composition. * Make `public allocate_badges` method which is used to standardize badge allocation across many connectors. -* Add support for a component definition to specify a template C source file. This file will be passed through the template tool before passed to the C compiler. - - This is how components can allocate objects required from a loader without having to define special connector types. -* Add `msgqueue` mechanism which allows componets to sent messages. This is essentially another layer ontop of the virtqueue functionality. +* Add support for a component definition to specify a template C source file. This file will be passed through the + template tool before passed to the C compiler. + - This is how components can allocate objects required from a loader without having to define special connector types. +* Add `msgqueue` mechanism which allows componets to sent messages. This is essentially another layer ontop of the + virtqueue functionality. * Accept Red Hat ARM cross-compilers in `check_deps.py`. * Simplify the logic for combining the connections in the stage9 parser. This improves processing times. * Camkes-tool: - - Add priority to muslc so that its initialsation comes after camkes. This relates to recent changes in sel4runtime. - - Add an interface `dataport_caps` for accessing dataport caps that is used by the seL4SharedDataWithCaps template. + - Add priority to muslc so that its initialsation comes after camkes. This relates to recent changes in sel4runtime. + - Add an interface `dataport_caps` for accessing dataport caps that is used by the seL4SharedDataWithCaps template. * Tools: define `camkes_tool_processing` when running the C preprocessor. * Remove `template` keyword from camkes language. - - This is driven by wanting to make it easier to extend camkes generation build rules with more inputs than a single template file and make it possible better manage non-template code that needs to run when generating templates. + - This is driven by wanting to make it easier to extend camkes generation build rules with more inputs than a single + template file and make it possible better manage non-template code that needs to run when generating templates. --- -camkes-3.8.0 2019-11-19 + +## camkes-3.8.0 2019-11-19 + Using seL4 version 11.0.0 -## Changes +### Changes * 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 @@ -167,18 +191,18 @@ Using seL4 version 11.0.0 - This was a feature that was available in 2.x.x but removed in 3.0.0. --- -camkes-3.7.0 2018-11-12 -Using seL4 version 10.1.1 -## Changes +## camkes-3.7.0 2018-11-12 +Using seL4 version 10.1.1 -## Upgrade Notes --- -camkes-3.6.0 2018-11-07 + +## camkes-3.6.0 2018-11-07 + Using seL4 version 10.1.0 -## Changes +### Changes * AARCH64 is now supported. * CakeML components are now supported. @@ -186,101 +210,114 @@ Using seL4 version 10.1.0 * Components can now make dtb queries to parse device information from dts files. * Component definitions for serial and timer added on exynos5422, exynos5410, pc99. * Preliminary support for Isabelle verification of generated capDL. - - See cdl-refine-tests/README for more information + - See cdl-refine-tests/README for more information * Simplify and refactor the alignment and section linking policy for generated Camkes binaries. * Dataports are now required to declare their size in the ADL. * Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. - - This change is BREAKING. + - This change is BREAKING. * Remove Kbuild based build system. * Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. * Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. -## Upgrade Notes +### Upgrade Notes * Any dataport definitions that did not specify a size must be updated to use a size. * Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. * Projects must now use the new Cmake based build system. --- -camkes-3.5.0 2018-05-28 + +## camkes-3.5.0 2018-05-28 + Using seL4 version 10.0.0 This release is the last release with official support for Kbuild based projects. This release and future releases use CMake as the build system for building applications. -## Changes +### Changes + * Remove `crit` and `max_crit` fields from TCB CapDL Object These fields were previously added to support an earlier version of seL4-mcs that gave threads criticality fields. This feature was removed from seL4-mcs. This also means that the arguments to camkes-tool, `--default-criticality` and `--default-max-criticality`, have also been removed. -## Upgrade Notes +### Upgrade Notes + * Calls to `camkes.sh` that used the above arugments will need to be updated. --- -camkes-3.4.0 2018-04-18 -Using seL4 version 9.0.1 -## Changes +## camkes-3.4.0 2018-04-18 +Using seL4 version 9.0.1 -## Upgrade Notes --- -camkes-3.3.0 2018-04-11 + +## camkes-3.3.0 2018-04-11 + Using seL4 version 9.0.0 -## Changes +### Changes + * Hardware dataport with large frame sizes issue has been fixed * Bug fix: Enumerating connections for hierarchical components with custom connection types is now done correctly * Bug fix: Data structure caching is now correctly invalidated between builds * Initial CMake implementation for CAmkES. See the CAmkES test apps for examples. -## Upgrade notes +### Upgrade notes + * No special upgrade requirements. -## Known issues +### Known issues + * Hierarchical components that export dataport connectors create compilation errors as the templates cannot accurately tell that the connector of the parent component is exported from the child and no code should be generated. A temporary workaround involves making the dataport connection explicitly available to the parent component. --- -camkes-3.2.0 2018-01-17 + +## camkes-3.2.0 2018-01-17 + Using seL4 version 8.0.0 -= Changes = - * New ADL Syntax: Allow struct elements to have defaults. - See the following ADL files for examples of Struct and Attribute behavior. - https://github.com/SEL4PROJ/rumprun/blob/master/platform/sel4/camkes/rumprun.camkes - https://github.com/seL4/camkes/tree/master/apps/structs - https://github.com/seL4/camkes/tree/master/apps/attributes - * Added experimental Rumprun support: - This functionality is experimental and may not work as expected. See the following examples: - https://github.com/seL4/camkes/tree/master/apps/rumprun_ethernet - https://github.com/seL4/camkes/tree/master/apps/rumprun_hello - https://github.com/seL4/camkes/tree/master/apps/rumprun_pthreads - https://github.com/seL4/camkes/tree/master/apps/rumprun_rust - More information about the Rumprun unikernel on seL4 can be found here: - https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd-drivers-on-sel4/ - * New Templates: Remote GDB debugging support - On ia32 platforms a GDB server can be used to debug a component using the GDB server remote serial protocol. - documentation: https://github.com/seL4/camkes-tool/blob/master/docs/DEBUG.md - * Added "hardware_cached" attribute to hardware dataports - This feature had been added to camkes-2.x.x but hadn't been forward ported to camkes-3.x.x. - documentation: https://github.com/seL4/camkes-tool/blob/master/docs/index.md#cached-hardware-dataports - -= Known issues = - * Hardware dataports that are large enough to use larger frame sizes are currently broken. There is an issue with -large frame promotion and hardware dataports where the capDL loader is unable to map the promoted memory. This can be -demonstrated by running the testhwdataportlrgpages app on either arm_testhwdataportlrgpages_defconfig or -x86_testhwdataportlrgpages_defconfig configurations. If this functionality is required, hold off upgrading until this -issue is fixed. - -= Upgrade notes = - * ADL files: ADL syntax changes in this release should not break any existing ADL files. - * Templates: - - seL4HardwareMMIO template now has an option to map hardware memory as cached. The default setting is uncached - which is the same as the old behaviour. +### Changes + +* New ADL Syntax: Allow struct elements to have defaults. + See the following ADL files for examples of Struct and Attribute behavior. + + + +* Added experimental Rumprun support: + This functionality is experimental and may not work as expected. See the following examples: + + + + + More information about the Rumprun unikernel on seL4 can be found here: + +* New Templates: Remote GDB debugging support + On ia32 platforms a GDB server can be used to debug a component using the GDB server remote serial protocol. + documentation: +* Added "hardware_cached" attribute to hardware dataports + This feature had been added to camkes-2.x.x but hadn't been forward ported to camkes-3.x.x. + documentation: + +### Known issues + +* Hardware dataports that are large enough to use larger frame sizes are currently broken. There is an issue with large + frame promotion and hardware dataports where the capDL loader is unable to map the promoted memory. This can be + demonstrated by running the testhwdataportlrgpages app on either arm_testhwdataportlrgpages_defconfig or + x86_testhwdataportlrgpages_defconfig configurations. If this functionality is required, hold off upgrading until this + issue is fixed. + +### Upgrade notes + +* ADL files: ADL syntax changes in this release should not break any existing ADL files. +* Templates: + - seL4HardwareMMIO template now has an option to map hardware memory as cached. The default setting is uncached + which is the same as the old behaviour. --- -For previous releases see https://docs.sel4.systems/camkes_release/ + +For previous releases see From cfa9e602b8ee4c0f4c08e390d67cd71c42186fc6 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 24 Jun 2024 19:49:43 +1000 Subject: [PATCH 3/3] CHANGES: bring up to date for upcoming release Signed-off-by: Gerwin Klein --- CHANGES.md | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 53 insertions(+), 2 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ed89362c..1c881e42 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,5 @@ # Version history for CAmkES -For more information see the release notes at - --- @@ -10,15 +8,68 @@ For more information see the release notes at