-
Notifications
You must be signed in to change notification settings - Fork 65
/
CHANGES
286 lines (245 loc) · 17.1 KB
/
CHANGES
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
Revision history for CAmkES
For more information see the release notes at https://docs.sel4.systems/camkes_release/
This file should be word wrapped to 120 characters
---
Upcoming release
## Changes
* Added RISC-V in `is_64_bit_arch()`
* Added helpers `is_arch_arm()` and `is_arch_riscv()`
* Added an additional parameter with the current architectures for the macros
`parse_dtb_node_interrupts()` and `global_endpoint_badges()`.
* 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
---
camkes-3.10.0 2021-06-10
Using seL4 version 12.1.0
## Changes
* Fixed new line generation in `show_attribute_value`.
* Added const expression attributes to help convert CAmkES attributes to literals.
* Fixed broken Python nosetests that weren't updated when moving to Python3 from Python2.
* Added caching when querying DMA frame physical addresses to avoid unnecessary kernel context switch overheads.
* Changed templates and libraries to be DMA cache-aware and to not ignore requests for cache-able memory
allocations.
* Added a macro function for every dataport to query its size.
* Changed DMA bookkeeping to keep track of pools of frames and not individual frames.
* Added code to sanitize the names of nested components for the naming of a components' DMA pool.
* Converted the repository to use SPDX license tags.
* Fixed the passing of LD flags to the linker from CAmkES generation tools.
* Added the failing C pre-processor command to an exception in the CAmkES parser tools for easier diagnosis.
* Moved the CAmkES component interface header contents away from `camkes.h` and into separate header files that is
included by `camkes.h`.
* Simplified the `sys_uname` library function.
* Fix handling of array parameters for the CAmkES templates.
* Sped up proofs for cdl-refine.
* Fixed a CMake argument marshalling bug in the `execute_process_with_stale_check` function.
### 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 `<component name>.dma_pool_cached = True;` in the 'configuration' block to make a component's
DMA pool to be cached. Additionally, use `camkes_dma_alloc` in libsel4camkes with the correct arguments to allocate
cached DMA memory from that pool.
---
camkes-3.9.0 2020-10-27
Using seL4 version 12.0.0
## Changes
* Enforce system-V stack ordering for libc.
- 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.
* 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.
* 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.
* 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.
* 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.
* 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.
* 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.
* `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.
* 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.
* Component.common.c: Move init() to C constructor
- 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.
* 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.
* 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.
* 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`.
* 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.
* 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.
* 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.
* 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.
* 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.
* 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.
* 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.
---
camkes-3.8.0 2019-11-19
Using seL4 version 11.0.0
## 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
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 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 (cdl-refine).
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.
* Port libsel4camkes environments to the sel4runtime
* CAmkES can be used on any seL4 platform that uses a camkes supported seL4 architecture (x86, Arm, RISC-V)
* By default the C preprocessor will be run over CAmkES ADL files
- The Camkes syntax excludes lines starting with `#` due to the integration of CPP. This can sometimes cause
confusion where #ifdef is used but the CPP isn't configured to run. Projects are still able to disable the CPP.
* capDL Static initialisation
- Using the capDL support for static allocation of objects from an Untyped list, Camkes supports generating specs
with all objects preallocated. This can then be loaded by a static loader.
- This is only supported on Arm by setting CAmkESCapDLStaticAlloc=ON.
* Use large pages for dataports if able
- Instead of rounding the dataports to 4K pages all the time, try to use multiples of larger frames to back the
dataports if the size of the dataports are a multiple of the larger frames.
* Fix cache flush for seL4HardwareMMIO connectors
- 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
## Upgrade Notes
---
camkes-3.6.0 2018-11-07
Using seL4 version 10.1.0
## Changes
* AARCH64 is now supported.
* CakeML components are now supported.
* Added `query` type to Camkes ADL to allow for querying plugins for component configuration values.
* 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
* 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.
* 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
* 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
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
* 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
* 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
## Upgrade Notes
---
camkes-3.3.0 2018-04-11
Using seL4 version 9.0.0
## 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
* No special upgrade requirements.
## 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
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.
---
For previous releases see https://docs.sel4.systems/camkes_release/