1Revision history for CAmkES 2 3For more information see the release notes at https://docs.sel4.systems/camkes_release/ 4 5This file should be word wrapped to 120 characters 6 7--- 8Upcoming release 9 10## Changes 11 12 13## Upgrade Notes 14--- 15camkes-3.9.0 2020-10-27 16Using seL4 version 12.0.0 17 18## Changes 19 20* Enforce system-V stack ordering for libc. 21 - This allows `musllibc` to initialise and infer the location of `auxv` from `envp` consistently. 22* Add `uint64_t` and `int64_t` types to language. 23 - This introduced two new data types into the CAmkES language to support larger types. 24* Remove `elf.h`, now defined in sel4runtime. 25* Camkes,rumprun: fix tls management implementation: 26 - `.tdata*` and `.tbss*` linker symbol declarations are suppressed until the final link step. 27* Fix `generate_seL4_SignalRecv` in `Context.py` and update `rpc-connector.c` template accordingly. 28 - `seL4SignalRecv` only exists on MCS, split the two calls for compatibility. 29* Save preprocessed camkes files to allow for easier debugging. 30* CMake: Skip fetching gpio list for pc99 platforms. 31 - Most PC99 platforms do not have GPIO pins. 32* Support for running odroidc2 in camkes-arm-vm. Get the IRQ trigger type through the interrupt node in the dts. 33* Add gpio query engine. 34 - 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. 35* Add option `CAmkESNoFPUByDefault`. 36 - 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. 37* Update `seL4InitHardware` template for api change. 38 - The configuration name for the list of devices to bind is now a component attribute instead of an interface attribute. 39* `libsel4camkes` Support registering DMA memory that is both cached and uncached. 40* Add sel4bench dependency into `camkes/templates` to allow for cycle counting. 41* `component.common.c`: use correct label for dma pool. 42 - When calling `register_shared_variable` from a component context the label needs to be provided. 43* Add `seL4DTBHW` connector. This connector variant is similar to `seL4DTBHardware`, but takes a hardware component on the from end. 44* `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. 45* Camkes connector extensions + DMA improvements: 46 - libsel4camkes: Implement DMA cache for Arm 47 - component.common.c: Support additional DMA setting. Allow setting the cache and base paddr value of the DMA pool. 48 - Add single_threaded attribute which when set adds the `seL4SingleThreadedComponent` templates. 49 - 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. 50 - 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. 51* Component.common.c: Move init() to C constructor 52 - Connectors that don't use threads use runtime constructors for their initialisation. 53* Libsel4camkes: camkes_call_hardware_init_modules 54Provide this public function for starting hardware modules that have been registered. 55* Add `global_rpc_endpoint_badges` macro. 56 - This macro assigns badges for different connectors that share the global-rpc-endpoint object for a component instance. 57* 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. 58* Add seL4DMASharedData connector and add appropriate library functionality in `libsel4camkes`. 59 - This connector sets up a dataport connector that is added to the DMA pool that the camkes runtime tracks for each component. 60* Add support for connector header files and component header templates. 61 - 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`. 62* Support creating TCB pools and assigning domains to them in camkes templates. 63 - Assign domain IDs for TCBs in the thread pool based on values provided by the config option array values. 64* Generalise jinja linter to support non-camkes use cases. The Jinja linter can now be used on any arbitrary Jinja template. 65* Add support in `libsel4camkes` for matching interrupts even if they are defined 66with different base types. 67* Add interface registration to `libsel4camkes` via `interface_registration.h` as part of the driver framework. 68* Revive graph.dot output file for each asssembly. This can be loaded with a 69program like `xdot` to view a diagram of the camkes system. 70* Virtqueues: 71 - Add virtqueue recieve. 72 - Set virtqueue size on creation to the number of rings and descriptor tables have. 73 - Add `virtqueue_get_client_id` macro for automatically assigning client IDs to distinguish different virtqueue channels within a single component instance. 74 - Link channel ID to name, this allows components to bind to channels via naming them rather than knowing their IDs. 75* Add Arm irq type support to `seL4HardwareInterrupt` template. This allows IRQs on Arm to have the trigger mode and target core configured. 76* Allow `size` to be number as well as a string in `marshal.c` template. 77* Add `global_endpoint_badges` macro used by the global-endpoints mechanism to assign badge 78values based on a full system composition. 79* Make `public allocate_badges` method which is used to standardize badge allocation across many connectors. 80* 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. 81 - This is how components can allocate objects required from a loader without having to define special connector types. 82* Add `msgqueue` mechanism which allows componets to sent messages. This is essentially another layer ontop of the virtqueue functionality. 83* Accept Red Hat ARM cross-compilers in `check_deps.py`. 84* Simplify the logic for combining the connections in the stage9 parser. This improves processing times. 85* Camkes-tool: 86 - Add priority to muslc so that its initialsation comes after camkes. This relates to recent changes in sel4runtime. 87 - Add an interface `dataport_caps` for accessing dataport caps that is used by the seL4SharedDataWithCaps template. 88* Tools: define `camkes_tool_processing` when running the C preprocessor. 89* Remove `template` keyword from camkes language. 90 - 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. 91 92--- 93camkes-3.8.0 2019-11-19 94Using seL4 version 11.0.0 95 96## Changes 97 98* Support for the new seL4 Endpoint GrantReply access right for CAmkES connector types. 99 - This allows multi-sender/single-receiver connectors such as `seL4RPCCall` that don't also provide the ability for 100 arbitrary capability transfer from sender to receiver. Previously the `seL4RPC` connector was used instead of 101 `seL4RPCCall` to create an Endpoint without a Grant right. This used a combination of `seL4_Send` and `seL4_Wait` 102 to communicate without the ability for capability transfer, however this only supports a single sender and single 103 receiver. 104* Better support for configuring components with a provided devicetree. 105 - This support includes adding a seL4DTBHardware connector that can be used instead of seL4HardwareMMIO and 106 seL4HardwareInterrupt and can be used to extract IRQs and MMIO register information out of the devicetree node rather 107 than specifying the info directly. This connector can also be used to access a devicetree within a component for 108 querying further device information. There is also a connector seL4VMDTBPassthrough that can be used for specifying 109 devices to pass through to a `camkes-arm-vm` VM component. 110* CapDL Refinement framework (cdl-refine). 111 These are generated Isabelle proof scripts to prove that the generated capDL respects the isolation properties 112 expected from its CAmkES system specification. Only the AARCH32 platform is supported. The generated capDL is a 113 specification of seL4 objects and capabilities that will implement the CAmkES system specification. This 114 specification is then given to a system initialiser to create the objects and capabilities and load the system. 115* Support for RISC-V systems. 116* Port libsel4camkes environments to the sel4runtime 117* CAmkES can be used on any seL4 platform that uses a camkes supported seL4 architecture (x86, Arm, RISC-V) 118* By default the C preprocessor will be run over CAmkES ADL files 119 - The Camkes syntax excludes lines starting with `#` due to the integration of CPP. This can sometimes cause 120 confusion where #ifdef is used but the CPP isn't configured to run. Projects are still able to disable the CPP. 121* capDL Static initialisation 122 - Using the capDL support for static allocation of objects from an Untyped list, Camkes supports generating specs 123 with all objects preallocated. This can then be loaded by a static loader. 124 - This is only supported on Arm by setting CAmkESCapDLStaticAlloc=ON. 125* Use large pages for dataports if able 126 - Instead of rounding the dataports to 4K pages all the time, try to use multiples of larger frames to back the 127 dataports if the size of the dataports are a multiple of the larger frames. 128* Fix cache flush for seL4HardwareMMIO connectors 129 - This was a feature that was available in 2.x.x but removed in 3.0.0. 130 131--- 132camkes-3.7.0 2018-11-12 133Using seL4 version 10.1.1 134 135## Changes 136 137 138## Upgrade Notes 139--- 140camkes-3.6.0 2018-11-07 141Using seL4 version 10.1.0 142 143## Changes 144 145* AARCH64 is now supported. 146* CakeML components are now supported. 147* Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. 148* Components can now make dtb queries to parse device information from dts files. 149* Component definitions for serial and timer added on exynos5422, exynos5410, pc99. 150* Preliminary support for Isabelle verification of generated capDL. 151 - See cdl-refine-tests/README for more information 152* Simplify and refactor the alignment and section linking policy for generated Camkes binaries. 153* Dataports are now required to declare their size in the ADL. 154* Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. 155 - This change is BREAKING. 156* Remove Kbuild based build system. 157* Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. 158* Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. 159 160 161## Upgrade Notes 162 163* Any dataport definitions that did not specify a size must be updated to use a size. 164* Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. 165* Projects must now use the new Cmake based build system. 166 167--- 168camkes-3.5.0 2018-05-28 169Using seL4 version 10.0.0 170 171This release is the last release with official support for Kbuild based projects. 172This release and future releases use CMake as the build system for building applications. 173 174## Changes 175* Remove `crit` and `max_crit` fields from TCB CapDL Object 176 These fields were previously added to support an earlier version of seL4-mcs that gave threads criticality fields. 177 This feature was removed from seL4-mcs. This also means that the arguments to camkes-tool, `--default-criticality` 178 and `--default-max-criticality`, have also been removed. 179 180## Upgrade Notes 181* Calls to `camkes.sh` that used the above arugments will need to be updated. 182 183--- 184camkes-3.4.0 2018-04-18 185Using seL4 version 9.0.1 186 187## Changes 188 189 190## Upgrade Notes 191--- 192camkes-3.3.0 2018-04-11 193Using seL4 version 9.0.0 194 195## Changes 196* Hardware dataport with large frame sizes issue has been fixed 197* Bug fix: Enumerating connections for hierarchical components with custom connection types is now done correctly 198* Bug fix: Data structure caching is now correctly invalidated between builds 199* Initial CMake implementation for CAmkES. See the CAmkES test apps for examples. 200 201## Upgrade notes 202* No special upgrade requirements. 203 204## Known issues 205* Hierarchical components that export dataport connectors create compilation errors as the templates cannot accurately 206 tell that the connector of the parent component is exported from the child and no code should be generated. A 207 temporary workaround involves making the dataport connection explicitly available to the parent component. 208 209--- 210camkes-3.2.0 2018-01-17 211Using seL4 version 8.0.0 212 213= Changes = 214 * New ADL Syntax: Allow struct elements to have defaults. 215 See the following ADL files for examples of Struct and Attribute behavior. 216 https://github.com/SEL4PROJ/rumprun/blob/master/platform/sel4/camkes/rumprun.camkes 217 https://github.com/seL4/camkes/tree/master/apps/structs 218 https://github.com/seL4/camkes/tree/master/apps/attributes 219 * Added experimental Rumprun support: 220 This functionality is experimental and may not work as expected. See the following examples: 221 https://github.com/seL4/camkes/tree/master/apps/rumprun_ethernet 222 https://github.com/seL4/camkes/tree/master/apps/rumprun_hello 223 https://github.com/seL4/camkes/tree/master/apps/rumprun_pthreads 224 https://github.com/seL4/camkes/tree/master/apps/rumprun_rust 225 More information about the Rumprun unikernel on seL4 can be found here: 226 https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbsd-drivers-on-sel4/ 227 * New Templates: Remote GDB debugging support 228 On ia32 platforms a GDB server can be used to debug a component using the GDB server remote serial protocol. 229 documentation: https://github.com/seL4/camkes-tool/blob/master/docs/DEBUG.md 230 * Added "hardware_cached" attribute to hardware dataports 231 This feature had been added to camkes-2.x.x but hadn't been forward ported to camkes-3.x.x. 232 documentation: https://github.com/seL4/camkes-tool/blob/master/docs/index.md#cached-hardware-dataports 233 234= Known issues = 235 * Hardware dataports that are large enough to use larger frame sizes are currently broken. There is an issue with 236large frame promotion and hardware dataports where the capDL loader is unable to map the promoted memory. This can be 237demonstrated by running the testhwdataportlrgpages app on either arm_testhwdataportlrgpages_defconfig or 238x86_testhwdataportlrgpages_defconfig configurations. If this functionality is required, hold off upgrading until this 239issue is fixed. 240 241= Upgrade notes = 242 * ADL files: ADL syntax changes in this release should not break any existing ADL files. 243 * Templates: 244 seL4HardwareMMIO template now has an option to map hardware memory as cached. The default setting is uncached 245which is the same as the old behaviour. 246 247--- 248For previous releases see https://docs.sel4.systems/camkes_release/ 249