- Devel - lists.sel4.systems

Pass Ethernet device to CAmkES ARM VM when using QEMU
by Olof Holmberg 02 Jun '21

02 Jun '21

Hi, I am currently trying to pass a device for ethernet access through qemu to the vm. However there seems to be some issue since the device is not passed through correctly. I have looked at some resources for guidance on how to solve it: https://github.com/seL4/sel4webserver (webserver example) https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/message/X34TX… (old devel thread) And the important parts for this to work seems to be untyped_mmios for the vm (in devices.camkes for qemu-arm-virt): vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* TODO: QEMU PCI addresses could change - ideally need to decode from pcie node */ "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; And passing the device to QEMU in the simulation script: $ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01" However when listing the devices with "ip a" on the VM it does not show an eth0 device: # ip a 1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue qlen 1 link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00 inet 127.0.0.1/8 scope host lo valid_lft forever preferred_lft forever inet6 ::1/128 scope host valid_lft forever preferred_lft forever 2: tunl0@NONE: <NOARP> mtu 1480 qdisc noop qlen 1 link/ipip 0.0.0.0 brd 0.0.0.0 3: ip6tnl0@NONE: <NOARP> mtu 1452 qdisc noop qlen 1 link/tunnel6 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 brd 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 But on the host the device that is passed to qemu can be seen: $ ip link show tap0 6: tap0: <BROADCAST,MULTICAST> mtu 1500 qdisc noop state DOWN mode DEFAULT group default qlen 1000 link/ether 62:43:43:54:2d:e6 brd ff:ff:ff:ff:ff:ff I am not sure if I missed something or if it is the QEMU addresses for the pci region that are not correct. Is there any output during boot or build that could give insight in what went wrong when it tries to passthrough the device? Also are there are any resources or guidelines on how to decode the pcie node? (Since I assume this has to be done inside the vm with the limited selection of commands available). Best regards, Olof

1 1

Blocking and unblocking under the MCS kernel
by Robert Kaiser 02 Jun '21

02 Jun '21

Hi all, I'm working on the SOS example of the AOS course, trying to adapt code that used to work under the non-MCS kernel to the now used MCS kernel. So far, this mostly works. However, I'm having problems in resuming a thread that is blocked in an IPC Call operation. In simple cases where the server can reply immediately, the thread is successfully unblocked, simply by replying to the reply object as with the reply capability in the non-MCS kernel. However, if the server does not respond immediately, (i.e. it leaves the calling thread in blocked state, serves some other requests and/or notifications in the meantime, then comes back to reply), replying to the reply object silently fails to unblock the thread for some reason. In the non-MCS kernel, it was necessary in these cases to save the reply capability in a cspace. Therefore I tried to similarly copy/move the reply object to a thread-specific cspace slot, but that doesn't help. I'm sure I'm missing something very basic here. Can anybody point me to the right direction? Best, Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

Easy way to edit VM guest file system
by skydivebcn＠gmail.com 02 Jun '21

02 Jun '21

Hi, I'm learning about this project: https://github.com/seL4/sel4webserver and would like to edit the guest filesystem. Digging around I found some cpio files that looks to me like may be the right place (output_overlay_rootfs.cpio, rootfs.cpio) but I'm not sure. So, as far I understand in theory I can just edit them and the execute "ninja" again. Before going that way, can anyone confirm this is the easiest/right way? Thanks,

3 2

CAmkES Tutorial, check_deps.py - what does good look like?
by Roderick Chapman 02 Jun '21

02 Jun '21

The first CAmkES tutorial points me at the "Usage" section of the CAmkES manual, which tells me to run "./tools/check_deps.py" to see if I have "the appropriate dependencies installed" but I have no idea what that means... What does good look like? I assume I'm supposed to run that from within the Docker container? If I do that, I get the output below, but I have no idea if that's right. I would expect the Docker container to "Pass" this test with flying colours... so I think I might have screwed up somewhere... Can anyone advise please? Thanks, Rod --- rchapman@in-container:/host/sel4-tutorials-manifest/projects/camkes-tool$ tools/check_deps.py Dependencies of CAmkES runner jinja2 (Python templating module)... Not found plyplus (Python parsing module)... Not found ply (Python parsing module)... Not found elftools (Python ELF parsing module)... Not found orderedset (Python OrderedSet module (orderedset))... Not found six (Python 2/3 compatibility layer)... Found sqlite3 (Python SQLite module)... Found pyfdt (Python flattened device tree parser)... Not found You will not be able to build/run this component Dependencies of CAmkES test suite expect (automation utility)... Found pylint (Python linter)... Found qemu-system-arm (ARM emulator)... Found qemu-system-i386 (IA32 emulator)... Found pycparser (Python C parsing module)... Not found gcc (C compiler)... Found spin (model checker)... Found sha256sum (file hashing utility)... Found You will not be able to build/run this component Dependencies of CapDL translator stack (Haskell version manager)... Found Dependencies of seL4 gcc (C compiler)... Found tempita (Python templating module)... Not found xmllint (XML validator)... Found bash (shell)... Found make (GNU Make build tool)... Found cpio (CPIO file system tool)... Found You will not be able to build/run this component Suggestions: c-parser (NICTA C-to-Simpl parser): you will need this installed if you want to validate code for verification clang-format (Clang code reformatter): installing this will reflow generated C code to make it more readable VBoxManage (VirtualBox administration tool): you will need this installed if you want to build VMWare images mformat (formatting tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 figleaf (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES python-coverage (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES syslinux (Linux bootloader tool): you will need this installed if you want to build QEMU images for IA32 mpartition (partitioning tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 pandoc (document format translator): you will need this if you want to build the CAmkES documentation mcopy (copying tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 sponge (input coalescer from moreutils): installing this will give a marginal improvement in compilation times

2 1

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 01 Jun '21

01 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

1 0

sel4webserver on qemu
by Hugo V.C. 31 May '21

31 May '21

Hi, I just did a commit: https://github.com/hugusmaximus/sel4webserver/blob/master/README.md so people can test this project without having to use a Odroid-XU4 (myself I had this problem...). Notice that I worked on this repository because in the below tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html I was failing all the time at running in qemu the x86_64 image. Not sure what was happening there, I fixed many things but still not working, maybe because my laptop is somewhat old (Latitude E6410), and even if VT-x is supported for some reason I was unable to make it work (fixed BIOS disabling trusted execution, had OS nested guests supported, etc). As I think having "easy things to play" is key for people to test seL4 stuff, I think it would be nice to make extra effort to have things working on user available equipment (x86_64, qemu, etc). Having said that, I excuse myself in advance for any mistakes in the pull request process as this is the first time in my life doing this, so any suggestion and corrections will be welcome. Last but not least important I'm very happy to have a working Linux guest on a seL4 running on my laptop as this opens to me a big door for tests so I can build prototypes and test many things hoping that as soon as possible I will have some developer doing this job and building native apps for seL4 to interact with an (isolated) guest. Cheers,

2 2

Troubles with hello-world tutorial
by Roderick Chapman 30 May '21

30 May '21

Hello everyone, I am a newbie with seL4, and trying to get the first hello-world tutorial to build and run. I am a bit stuck on a few issues. 1. I had to add the Python "sh" module before the "init" script would run. 2. It is not clear if the "init" script should be run on my main Linux VM, or within the Docker container. 3. The instructions here https://docs.sel4.systems/Tutorials/hello-world.html and https://docs.sel4.systems/Tutorials/ appear to be contradictory, and neither actually works. It appears that the correct sequence of commands is: 3.1. Start the docker container in the directory above sel4-tutorials-manifest 3.2. In the container: cd sel4-tutorials-manifest mkdir hello-world cd hello-world ../init --plat pc99 --tut hello-world cd ../hello-world_build ninja ./simulate Does that look right? The build finishes with "[181/181] objcopy kernel into bootable elf" although https://docs.sel4.systems/Tutorials/hello-world.html says it should be "[150/150] objcopy kernel into bootable elf" Is that still OK? Should I raise an Issue in GitHub to get the documentation pages updated? All the best, Rod Chapman, Director, Protean Code Limited

8 19

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 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