- Devel - lists.sel4.systems

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

12 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

Reducing memory footprint - RISC-V
by porter.188＠osu.edu 19 Apr '21

19 Apr '21

I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now. In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000. 42 memory@80000000 { 43 device_type = "memory"; 44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>; 45 }; This is the smallest value that builds, lower than this I get the error: [0/1] Re-running CMake... -- Found GCC with prefix riscv64-unknown-linux-gnu- STATUS,KernelDTSList: tools/dts/spike.dts -- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml -- Detecting cached version of: musllibc -- Found valid cache entry for musllibc -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/femur_12.0/build [18/36] Generating gen_headers/image_start_addr.h FAILED: elfloader-tool/gen_headers/image_start_addr.h cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}" ninja: build stopped: subcommand failed. What do I need to modify to get to < 2 MB? Thanks!

4 8

seL4 Crowdsourcing Portal
by Gernot Heiser 14 Apr '21

14 Apr '21

Dear seL4 community, It is a pleasure to announce that seL4 now has a crowdsourcing portal, using the Linux Foundation’s LFX platform. Please help making seL4 stronger by donating, and encouraging others to do the same! https://crowdfunding.lfx.linuxfoundation.org/projects/e94c998c-bac2-4224-b0… Gernot

1 0

Choosing correct hardware platform for CAmkES-arm-vmm Cross VM connector support
by Zohra Charania 14 Apr '21

14 Apr '21

Hi everyone, I am a PhD student. For my research, I want to use sel4 and developa system based on it. The idea is to use the arm based multi VM and cross VM communication ability of sel4 and provide a secure and isolated environment for the various applications running on the system. I was reading through the sel4 tutorials and documentation to find out which hardware would be suitable for this. I started learning sel4 with Raspberry Pi 3, but as Rpi3 does not have GICv2 or GICv3, I am not sure how do I develop the CAmkES-arm-vmm, multi VM and cross VM connector on it. As I wish to develop an application i.e a system architecture using sel4, itwould be good to have a device that provides me the starting point of having a multi VM and Cross VM communication. I read in the documentation that we can use Nvidia TK1-SOM from Colorado engineering to develop CAmkES-arm-vmm. But if I see the table here: _https://docs.sel4.systems/projects/camkes-arm-vm/_ , it says that CrossVM and Multi VM support is unsupported and in notes it says untested. According to the table, this is true for TK1, TX1 and TX2. Could someone please clarify what does this mean? Does it mean that we cannot have these features for these hardware or is it that they are not tested? It will be a great help to get this information, as then I can purchase the correct hardware and advance my work. I am new to micro-kernel community, so I apologize if I have missed anything obvious and would be glad to receive guidance and advice. Hoping for a kind response. Thank you. Sincerely, Zohra

1 0

[seL4 Announce] Operating System based on seL4.
by Gernot Heiser 12 Apr '21

12 Apr '21

<comment> The below message was posted to announce(a)sel4.systems. It was inappropriate for that list, but got though due to a configuration error (now fixed). I’m reposting it here as it would be appropriate for this list. Feel free to respond here. </comment> Hello, Which operating systems are based on seL4 Microkernel? Any home usage? Thanks.

2 1

hello world difficulty
by Royce Mitchell III 08 Apr '21

08 Apr '21

I feel like an idiot for having to ask for help so early, but I'm trying to get started with the hello world tutorial and ran into a problem very quickly. First off I want to say thank you for all the work that's been put into the tutorils. The amount of information in them is quite daunting, but considering the subject matter it's actually very accessible all things considered. I have a Debian 10 linux VM that I'm using for testing. I'm okay building a VM dedicated solely to seL4 development if that's necessary, but I'm assuming it's not. FYI I had some difficulty with the prerequisites instructions regarding Debian. This may be the source of the problem I'm having but I'm not sure how to resolve it. Your setup instructions said to refer to the docker requirements but when I went there I couldn't find anything on that page that indicated what exactly I was supposed to install. All that being said, here is a capture from my terminal which I'm hoping illustrates the problem I'm having specifically: rmitchell@ou812:~/sel4-tutorials-manifest$ ./init --tut hello-world Traceback (most recent call last): File "./init", line 16, in <module> import common File "/home/rmitchell/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' rmitchell@ou812:~/sel4-tutorials-manifest$ python Python 3.9.1 (default, Mar 19 2021, 01:08:36) [GCC 8.3.0] on linux Type "help", "copyright", "credits" or "license" for more information. >>> import sh >>> sh.__version__ '1.14.1' >>> exit() As you can see from my example above, I have Python 3.9.1 installed and it is the default python interpreter on my system. The "sh" module is installed and accessible from Python's interactive interpreter, yet when the common.py file tries to import it, it complains that it can't find the 'sh' module. FYI sh is installed both at the system and user levels. I'll try digging into your source and see if I can figure out what the issue is. I'll share my findings if I figure it out before you guys point out my mistakes. Thanks! Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

3 6

seL4 service discovery question
by Royce Mitchell III 08 Apr '21

08 Apr '21

Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos. The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me. If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated. Given: * An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver. * A "tcp" service that would implement that network protocol. * A higher level service named "network" that implemented some kind of networking abstraction for us. How would: 1) the "network" service advertise its services as available via IPC? 2) an application locate this "network" service to be able to IPC with it? I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services. I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit. If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4? If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works) Thanks, Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

6 14