Devel May 2021

devel@sel4.systems

16 participants
15 discussions

ARM64: Handle SError in user-space instead of halting the kernel
by Indan Zupancic 27 May '21

27 May '21

Hello, By default any SError interrupt will halt the kernel. SErrors may be caused by e.g. writes to read-only device registers or ECC errors. With this patch SErrors can instead be reported as a VM data fault for the currently running task. Because SError is asynchronous it is not assured that the faulting task caused the error. With ARMv8.2 there is a new RAS feature which solves the SError problem for common cases: This patch does not use that, our hardware is v8.0, we need another solution for the SError problem. We would rather log the SError and continue than halt the whole system. As SError is easily triggered by device drivers, halting the whole system would make user-space device drivers not much more reliable than in-kernel ones. I do not know if VMs can also cause SErrors in seL4. However, that seems likely, in which case guest OSes can also halt the whole system. One thing I'm not sure about: SError is edge-triggered, while handleVMFaultEvent() does a MCS_DO_IF_BUDGET check. Does this means that if the current task has no budget, the SError IRQ will be lost? Or are pending faults saved by the schedule code? For us missing the SError would be better than halting the kernel, so it doesn't really matter, but I would like to know. I have an Atlassian account, but it seems you can't attach patches there, so I'm not sure how else to send this patch, other than creating a Github account. What is the preferred way to submit patches as an outsider? Best regards, Indan

4 5

Running seL4Test for RISCV with QEMU
by basho1600＠pm.me 13 May '21

13 May '21

Working on Ubuntu, I have built the seL4Test project for RISCV64. I think. At least, there were no build errors. I have qemu-system-riscv64 installed. But when I get to the ./simulate command, all I get is an echo of "Unsupported platform or architecture for simulation". I configured this test as follows: ../init-build.sh -DPLATFORM=hifive -DRELEASE=FALSE -DSIMULATION=TRUE After the 'ninja' command completes, in the images/ directory there is a 6.6MB file named sel4test-driver-image-riscv-hifive which I am guessing is the resulting image to run, though qemu is not impressed by it, saying that the image format is not specified. Maybe I am just not finding the instructions on how to run this, or what 'simulate' WOULD have contained, had things been working as I expect. Or the complete qemu command line to run it.

2 1

Generating CAmkES glue-spec and glue-proofs
by Ben Fiedler 11 May '21

11 May '21

Hi everyone, I'm having troubles generating the CAmkES glue component specification and proofs from our source. I can and have successfully generated the ADL/CDL spec and implementations using the documented CMake parameters. Grepping around the docs I've found references to a 'camkes.sh' script, but neither the project tree nor the files generated during build contain it. One candidate reason could be that we set up our build environment strangely: We currently check out seL4/camkes-manifest and then symlink our component into the 'projects/global-components' subtree of the seL4. This works for generating bootable images, but I haven't found out how to generate the glue spec yet. Why we have set it up this way I don't know, and I suspect that there is a right way TM that we have overlooked/not found in the documentation. I appreciate any help in this regard. Thanks and have a nice day! Cheers, Ben

4 6

Multiple ARM VMs with different CAmkES component configurations
by Olof Holmberg 11 May '21

11 May '21

Hi, I am currently performing research for my master thesis which involves seL4 and ideally retrofitting a SDN controller application for it. As a part of retrofitting applications for seL4 the suggested way is the incremental cyber retrofit approach wich involves dividing subsystems of the application onto several VMs that each runs in a VMM. Therefore I was wondering if it is currently possible to run several VMs on the ARM architecture that has different component configurations in CAmkES? (ARM is mostly preferable for the simple simulation in QEMU when building for qemu-arm-virt, so switching architecture is an option if this is not achievable) I noted that the macros for VMs on x86 and ARM were different when defining components: x86: /* VM and per VM componenents */ #define VM_PER_VM_COMPONENTS(num) \ component Init##num vm##num; \ /**/ ARM: #define VM_COMPONENT_DEF(num) \ component VM vm##num; \ And to clarify using the vm-examples where in the optiplex9020.camkes there are two VMs that are configured differently: component Init0 { dataport Buf(STRING_REVERSE_BUFSIZE) dp1; dataport Buf(STRING_REVERSE_BUFSIZE) dp2; emits Ready ready; consumes Done done; has mutex cross_vm_event_mutex; VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } But in the ARM vm_multi.camkes there is only one VM component that is used for all three VMs: component VM { VM_INIT_DEF() maybe uses VirtQueueDev recv1; maybe uses VirtQueueDrv send1; maybe uses VirtQueueDev recv2; maybe uses VirtQueueDrv send2; attribute vswitch_mapping vswitch_layout[] = []; attribute string vswitch_mac_address = ""; } So it is at least it is not as simple as defining Init##num components for ARM since currently only one VM component is allowed in the macros. Do you have a recommended way that could achieve a CAmkES structure that allows for multiple differently configured VMs for ARM without altering the macros? If it is not possible at the time I assume that switching to x86 is the easiest alternative to achive this? Best regards, Olof

2 2

CAmkES Access to TCBs
by John Shackleton 06 May '21

06 May '21

I am attempting to develop a userland scheduler to manage the release times and deadlines of other threads executing in the system. I would like to use CAmkES as much as possible, since it abstracts away many messy and error-prone details. Question: How do we specify in CAmkES that a scheduler component has access to TCBs of other CAmkES components? Thanks, -John

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel May 2021