When using dtb queries on a type that has multiple instances, when the second or additional instances are evaluated, their settings have bad values: gpio_mux_server1.gpio.dtb = dtb({}) instead of the expected: gpio_mux_server1.gpio.dtb = dtb({"path" : "/gpio@2200000"}). This is due to a parser bug that mutates the internal dictionary object instead of mutating a copy.

component GPIOMUXServer {

    emits FDT dummy_source;
    consumes FDT gpio;
    consumes FDT mux;

    composition {

        connection seL4DTBHardware gpio_conn(from dummy_source, to gpio);
        connection seL4DTBHardware mux_conn(from dummy_source, to mux);

    }

    configuration {
        gpio.dtb = dtb({"path" : "/gpio@2200000"});
        mux.dtb = dtb({"path" : "/pinmux@2430000"});

    }
}

assembly {
  composition {
        component GPIOMUXServer gpio_mux_server0;
        component GPIOMUXServer gpio_mux_server1;
  }
  configuration {}

}

Given the helloworld assembly in http://sel4.systems/CAmkES/README.pml, i.e.,

assembly {
    composition {
        component Hello h;
        component Client c;
        connection seL4RPC conn(from c.iface, to h.inf);
    }
}

if you get the from and to mixed up (like I did the first time, because I didn't just copy and paste), i.e.,

        connection seL4RPC conn(from h.inf, to c.iface);

then the resulting error message is vague and doesn't suggest that this was the mistake:

Unresolved references in input specification:
 .../seL4/apps/helloworld/helloworld.camkes:11:'inf' of type Interface
 .../seL4/apps/helloworld/helloworld.camkes:11:'iface' of type Interface

I believe 0 is a valid priority, but Camkes only lets you go down to 1 for the default priority:

https://github.com/seL4/camkes-tool/blob/master/Kconfig#L52

GitHub check fail in cmake_format/parser.py in my branch, see https://github.com/axel-h/camkes-tool/runs/1806970220?check_suite_focus=true
I can't relly make sense of this error. Seem the format checker tool is broken here:

CRITICAL:root:[
'/home/runner/work/camkes-tool/camkes-tool/Findcamkes-tool.cmake',
'/home/runner/work/camkes-tool/camkes-tool/components/components.cmake',
'/home/runner/work/camkes-tool/camkes-tool/components/plat/pc99/plat/CMakeLists.txt',
'/home/runner/work/camkes-tool/camkes-tool/libsel4camkes/CMakeLists.txt',
'/home/runner/work/camkes-tool/camkes-tool/libcamkescakeml/CMakeLists.txt',
'/home/runner/work/camkes-tool/camkes-tool/camkes/templates/camkes-gen.cmake',
'/home/runner/work/camkes-tool/camkes-tool/camkes/templates/templates.cmake',
'/home/runner/work/camkes-tool/camkes-tool/camkes.cmake',
'/home/runner/work/camkes-tool/camkes-tool/camkes-top-level.cmake',
'/home/runner/work/camkes-tool/camkes-tool/CMakeLists.txt'
] failed with error code 1

While processing /home/runner/work/camkes-tool/camkes-tool/camkes/templates/camkes-gen.cmake
Traceback (most recent call last):
  File "/home/runner/.local/bin/cmake-format", line 8, in <module>
  sys.exit(main())
  File "/home/runner/.local/lib/python3.7/site-packages/cmake_format/__main__.py", line 421, in main
  process_file(cfg, infile, outfile, args.dump)
  File "/home/runner/.local/lib/python3.7/site-packages/cmake_format/__main__.py", line 110, in process_file
  parse_tree = parser.parse(tokens, config.fn_spec)
  File "/home/runner/.local/lib/python3.7/site-packages/cmake_format/parser.py", line 608, in parse
  return consume_body(tokens, cmdspec)
  File "/home/runner/.local/lib/python3.7/site-packages/cmake_format/parser.py", line 592, in consume_body
  tokens[0].begin.line, tokens[0].begin.col))
  AssertionError: Unexpected UNQUOTED_LITERAL token at 30:0

Follow-u up from #79

Drop the best guess in the interrupt parsing and read the #interrupt-cells from the interrupt controller instead. Use the device tree parser we already use for the kernel.
See #79 (review)

The camkes-tool already gets given an import path to the capDL python library,
so it shouldn't be too hard to give it access to the kernel hardware_gen python
lib that would allow proper irq parsing.

Hello

This program is supposed called a echo with client and write "hello world". i need uses as "Single Address Space Components (Groups)".

`assembly {
composition {
group group_test{
component Echo echo;
component Client client;
}

    connection seL4DirectCall p(from group_test.client.a, to group_test.echo.a);
}

}`

This method is performed in x86_64 platform. But not on the "imx7" platform. Is this possible for the imx7 platform?

The cdl have only one ep cap in the group CNode, even if the group have multiple components. The TimeServer distinguish sender by the badge of the sender ep. So, only one component can get response from the TimeServer.
for example,
import <std_connector.camkes>;
import <global-connectors.camkes>;
import <TimeServer/TimeServer.camkes>;

component Client {
control;
uses Timer timeout;
}

assembly {
composition {
group grp {
component Client c1;
component Client c2;
}

    component TimeServer time_server;
    
    connection seL4TimeServer ts1(from grp.c1.timeout, to time_server.the_timer);
    connection seL4TimeServer ts2(from grp.c2.timeout, to time_server.the_timer);
}   

configuration {
    time_server.timers_per_client = 1;
}   

}

in https://github.com/axel-h/camkes-tool/runs/1192932657 seL4/ci-actions/style fails in template camkes/templates/camkes-gen.cmake

CRITICAL:root:['/home/runner/work/camkes-tool/camkes-tool/camkes-top-level.cmake', '/home/runner/work/camkes-tool/camkes-tool/CMakeLists.txt', '/home/runner/work/camkes-tool/camkes-tool/libsel4camkes/CMakeLists.txt', '/home/runner/work/camkes-tool/camkes-tool/components/plat/pc99/plat/CMakeLists.txt', '/home/runner/work/camkes-tool/camkes-tool/components/components.cmake', '/home/runner/work/camkes-tool/camkes-tool/libcamkescakeml/CMakeLists.txt', '/home/runner/work/camkes-tool/camkes-tool/Findcamkes-tool.cmake', '/home/runner/work/camkes-tool/camkes-tool/camkes/templates/camkes-gen.cmake', '/home/runner/work/camkes-tool/camkes-tool/camkes/templates/templates.cmake', '/home/runner/work/camkes-tool/camkes-tool/camkes.cmake'] failed with error code 1
'While processing /home/runner/work/camkes-tool/camkes-tool/camkes/templates/camkes-gen.cmake
Traceback (most recent call last):
  File "/home/runner/.local/bin/cmake-format", line 8, in <module>
    sys.exit(main())
  File "/home/runner/.local/lib/python3.6/site-packages/cmake_format/__main__.py", line 421, in main
    process_file(cfg, infile, outfile, args.dump)
  File "/home/runner/.local/lib/python3.6/site-packages/cmake_format/__main__.py", line 110, in process_file
    parse_tree = parser.parse(tokens, config.fn_spec)
  File "/home/runner/.local/lib/python3.6/site-packages/cmake_format/parser.py", line 608, in parse
    return consume_body(tokens, cmdspec)
  File "/home/runner/.local/lib/python3.6/site-packages/cmake_format/parser.py", line 592, in consume_body
    tokens[0].begin.line, tokens[0].begin.col))
AssertionError: Unexpected UNQUOTED_LITERAL token at 30:0

I assume the problem is that this is template processing code is not hidden in a a CMake comment, so it is considered CMake code for the style checker. But it is indeed invalid CMake code.

/*- set instances = composition.instances -*/
/*- set connections = composition.connections -*/

Maybe the style check must run after the a dummy run of the template processor has simply removed all template code?

Hello,

As of seL4_libs commit bdcec827602c8efb041b45f0892e0e5d958526ed, sel4bench_counter_t was replaced with ccnt_t. This has not been updated in camkes/timing.h, so the generated code fails when the enable collection of timing data for connectors menuconfig option is selected.

Here is a patch that fixed the issue for me.

--- a/libsel4camkes/include/camkes/timing.h
+++ b/libsel4camkes/include/camkes/timing.h
@@ -29,7 +29,7 @@
 
 #define TIMING_DEFS(pref, pts...) \
     static int libsel4camkes_timing_buffer_iteration = -1; \
-    static sel4bench_counter_t libsel4camkes_timing_buffer[TIMING_ENTRIES]; \
+    static ccnt_t libsel4camkes_timing_buffer[TIMING_ENTRIES]; \
     static char *libsel4camkes_timing_points[] = { \
         pts \
     }; \
@@ -49,7 +49,7 @@
     } \
     void pref##_timing_reset(void) { \
         libsel4camkes_timing_buffer_iteration = -1; \
-        memset(libsel4camkes_timing_buffer, 0, sizeof(sel4bench_counter_t) * TIMING_ENTRIES); \
+        memset(libsel4camkes_timing_buffer, 0, sizeof(ccnt_t) * TIMING_ENTRIES); \
     }

With from seL4/seL4_libs#63 (related also #109) the heap size must be a multiple of 4 KiB. We should try check this at compile time to avoid runtime errors like seL4/camkes-vm#28 happening then. Also update the CMake comment at CAMKES_DEFAULT_HEAP_SIZE to mention at least, that certain alignment might be a runtime library requirement.
If we break compilation, we also force the user to make a proper choice - might be better any trying fix the value. The memory management lib's startup code should also do a runtime check at startup. It might reduce the available heap in debug and release builds then.

The camkes-cli tool is unused and basically bit-rotted.

It should either be resurrected and brought up to date (might not be hard), or be retired/put on hold officially.

The tool is on pypi and mentioned on https://docs.sel4.systems/projects/camkes/cli

There is a test-action for it in seL4/ci-actions#87, but that is on hold until this issue is decided.

I am trying to make a connector that has an attribute.
In the CAmkES manual it says:

Components and connectors can have extra data of an arbitrary
type associated with them. These are referred to as attributes. The
description of a component/connector must describe the name of the
attribute and its type. The value of the attribute itself is unspecified.
It is assigned when the entity is instantiated, and this assignment is
referred to as a setting. Attributes are generally used to specialise or
differentiate a component at runtime.

A sample connector that I am trying to make in my top level CAmkES app for a simple case is:

connector NewSharedData {
   from Dataport user_data template "seL4SharedData-from.template.c";
   to Dataport provider_data template "seL4SharedData-to.template.c";
   attribute string attr_string; 
}

When I build the repo I get Unexpected token 'attribute'. If I comment it out, all works fine because it is the same as the standard seL4SharedData connector.

I used the attribute keyword the same as when I make a component and it is fine.

Am I using this wrong or is it not supported anymore?

Setup:

• Host: Xubuntu 16.04
• CAmkES 2.3
• seL4 4.0

(Moved from https://sel4.atlassian.net/browse/SELFOUR-2543)
A feature may be added in the future for delegating IOPort calls to a different camkes component. This is required to support sharing of devices across components such as for a PCI bus. Currently, IOPort operations for accessing PCI configuration IOPorts located in a different component need to be called through a separate API. This only affects x86

Hi. I'm working on a new camkes-based project.
This project is simulated by using Qemu, on Q35 machine for X86_64 arch and e1000e eth. I am using intel controller driver (82574 controller) for network communication. my project has built successfully and completed intel network driver initialized.

But when using network in my application in Qemu, no network packet is sent and received!

Qemu command:

sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu host, 
-netdev tap,id=netdev0,ifname=tap0,script=no,downscript=no 
-device e1000e,id=nic0,netdev=netdev0,mac=52:55:00:d1:55:01  
-nographic  -serial mon:stdio -m size=4G  -device intel-iommu  
-kernel ./target/debug/images/kernel-x86_64-pc99  
-initrd ./target/debug/images/capdl-loader-image-x86_64-pc99

.

Appendix:
Create tap0 command:

export TAP_DEV=tap0
sudo ip tuntap add dev $TAP_DEV mode tap
sudo ip addr flush dev $TAP_DEV
sudo ip addr add 10.10.100.1/24 brd 10.10.100.255 dev $TAP_DEV
sudo ip link set dev $TAP_DEV addr 02:00:ca:fe:01
sudo ip link set dev $TAP_DEV up

.

how to fix this problem?
thank you.

The Github description of this repository is "The main CAmkES tool https://wiki.sel4.systems/CAmkES". The URL in this 404s for me.

Previously in Camkes you could specify an attribute as a string:

dispatch_periodic_inst.timer_attributes = "10";

In Camkes Next, this declaration is ignored and the attribute is treated as 0. I understand I should instead use

dispatch_periodic_inst.timer_attributes = 10;

But it would be much nicer if Camkes Next would give an error message about the first version instead of silently ignoring it.

See:
https://github.com/seL4/camkes-tool/blob/next/camkes/templates/rpc-connector-common-from.c#L43
https://github.com/seL4/camkes-tool/blob/next/camkes/templates/rpc-connector-common-from.c#L67

orderedset can't be set up properly in python3.11, even though it is not referred to in the python tools. However, keeping it in camkes-deps

breaks the pip install.

Building wheel for orderedset (setup.py): finished with status 'error'
  error: subprocess-exited-with-error
  
  × python setup.py bdist_wheel did not run successfully.
  │ exit code: 1
  ╰─> [19 lines of output]
      running bdist_wheel
      The [wheel] section is deprecated. Use [bdist_wheel] instead.
      running build
      running build_py
      creating build
      creating build/lib.linux-x86_64-cpython-311
      creating build/lib.linux-x86_64-cpython-311/orderedset
      copying lib/orderedset/__init__.py -> build/lib.linux-x86_64-cpython-311/orderedset
      running build_ext
      building 'orderedset._orderedset' extension
      creating build/temp.linux-x86_64-cpython-311
      creating build/temp.linux-x86_64-cpython-311/lib
      creating build/temp.linux-x86_64-cpython-311/lib/orderedset
      x86_64-linux-gnu-gcc -Wsign-compare -DNDEBUG -g -fwrapv -O2 -Wall -g -fstack-protector-strong -Wformat -Werror=format-security -g -fwrapv -O2 -fPIC -I/usr/include/python3.11 -c lib/orderedset/_orderedset.c -o build/temp.linux-x86_64-cpython-311/lib/orderedset/_orderedset.o
      lib/orderedset/_orderedset.c:209:12: fatal error: longintrepr.h: No such file or directory
        209 |   #include "longintrepr.h"
            |            ^~~~~~~~~~~~~~~
      compilation terminated.
      error: command '/usr/bin/x86_64-linux-gnu-gcc' failed with exit code 1
      [end of output]

Rationale: Many programming languages (in which we would like to write high-assurance code) have support for sized integer types, and being able to use these in array parameters would be very helpful.

They seem to be supported fine using CType when not used in arrays, maybe the fix is as easy as adding CType to the param_type macro in camkes/templates/arch-definitions.thy?

Currently I'm using a workaround passing char instead of uint8_t, but the latter conveys much more cleanly what I want to express (plus char may or may not be unsigned, and unsigned char is not supported).

Follow-up from https://sel4.discourse.group/t/pre-rfc-exposing-cross-component-tcbs-via-camkes-template/479/4

CAmkES lacks a concept for defining “monitor” or “supervisor” relationships between component instances to deal with concerns such as fault handling or scheduling.

Hey guys,

This is a really small thing, but the link to the Visual CAmkES wiki is broken. Is it supposed to point to this page? https://wiki.sel4.systems/VisualCAmkES

Thanks!

The problem arises due to the "subtracted" line of code in the following diff snippet.
A correction for it is trivial and noted in the "added" line of code.

@@ -490,7 +490,7 @@ class Connection(ASTObject):
if len(types) > 1:
raise ASTError('multiple conflicting types for the '
'interfaces of connection '%s': %s' % (self.name,
- ', '.join(types)), self)
+ ', '.join(map(str,types))), self)
for f in self.from_ends:
if not isinstance(f.interface, Emits) and not
isinstance(f.interface, Uses) and not \

Follow up from https://lists.sel4.systems/hyperkitty/list/[email protected]/thread/XJHPCD5E5MNF2YYN4HRLQC4UEHFKVBX3

There should be a convenient way to add a dependency to a CAmkES component via DeclareCAmkESComponent(). Currently this function creates a target CAmkESComponent_${name} that can be used in add_dependencies() then. However, it would be nicer to keep the target name private and support DEPENDS as parameters. We already support a CAKEML_DEPENDS there anyway.

delete branch 'spdx', should should all be merged now?

When no camkes applications are selected, the error message is still

Multiple CAmkES applications selected. Only a single application can be built at once. Stop.

Which is misleading.

(Moved from https://sel4.atlassian.net/browse/SELFOUR-2542)
Camkes currently maps all DMA memory uncached and doesn't provide mechanisms for cache management. It should be possible to map DMA memory cached for architectures that support cache coherent DMA (x86) and also to support drivers that want to have cached software access and use cache management operations for faster data transfers.

When attempting to build an x86 VM with a SerialServer connection, I get this error when invoking the init-build.sh script:

ERROR:CAmkES:/host/projects/global-components/components/SerialServer/SerialServer.camkes:49:19:         HARDWARE_SERIAL_COMPOSITION
ERROR:CAmkES:                                                                                                      ^
ERROR:CAmkES:unknown reference to 'Serial'

The issue is due to defining a Serial.camkes file for each COM port on x86 (which was a good change). I validated that the Import paths were being handled properly. (Debug print is mine).

Serial port com1 selected.
-- path: /host/projects/camkes-tool/components/plat/pc99/plat/components/serial_com1

My fix is to rename the pc99/plat/components/serial_comX/Serial.camkes files to SerialCom.camkes and import <SerialCom.camkes>

diff --git a/components/plat/pc99/plat/serial.camkes b/components/plat/pc99/plat/serial.camkes
index 44025ff..b1b680a 100644
--- a/components/plat/pc99/plat/serial.camkes
+++ b/components/plat/pc99/plat/serial.camkes
@@ -4,4 +4,4 @@
  * SPDX-License-Identifier: BSD-2-Clause
  */
 
-import <Serial.camkes>;
+import <SerialCom.camkes>;

I'm unsure if you'll be able to replicate the issue, as it may be related to how my Macbook handles file paths, but I'm hoping the fix is simple enough that you can just pull it in

delete branch kent/rumprun-fix, looks like this has been merged.

@lsf37 I thought about your reply a few days ago, was reading the seL4 whitepaper and when I saw the diagram of gradually breaking out the system into camkes components, a lightbulb went off 🤔

If Node.js was a tightly integrated camkes component, would that not be superior to Rust because of the security guarantees seL4 provides and the vast ecosystem of JS?

If this works, it can bring contributors and enterprises in seL4's direction which can ultimately accelerate the funding of big-ticket items like the arm64 and multicore kernels.

Also, other languages jump on board and contribute their libraries to seL4.

As I understand it, Node.js has 6 dependencies: V8, libuv, llhttp, c-ares, openssl, zlib. I'm assuming openssl and zlib are already good to go, and (again, assuming) libuv isn't relevant.

Is porting these 3 to seL4 feasible?

Edit: This would also replace hacks like chroot and containers where Node.js is the only runtime.