- Devel - lists.sel4.systems

some question about sched_ctrl of mcs答复: some question about mcs
by yadong.li 26 Aug '20

26 Aug '20

Hi Kent： Firstly，thank you for your information. I found the test code call "simple_get_sched_ctrl(&env->simple, 0)" function to get sched_ctrl cap, but I feel confused about env->simple. I have two question about sched_ctrl when I want to add mcs call function for camkes-arm-vm project Background: I try to add get sched_ctrl cap before seL4_TCB_Configure of vm_create_vcpu_arch(projects/seL4_projects_libs/libsel4vm/src/arch/arm/boot.c) 1. I try use "simple_get_sched_ctrl(vm->simple, affinity);" or " simple_default_init_bootinfo(&simple, platsupport_get_bootinfo()) simple_get_sched_ctrl(simple, affinity);" But they all failed What "simple" should I used to get sched_ctl in this project. 2. I found camkes_simple_sched_ctrl in component.simple.c generate C code, have below code: /*- if 'sched_ctrl' in configuration[me.name].keys() -*/ But I did not found camkes configurations have "sched_ctrl" field in project or your examples in CAmkES Thank you very much -----邮件原件----- 发件人: Kent Mcleod [mailto:kent.mcleod72@gmail.com] 发送时间: 2020年8月25日 10:37 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] some question about mcs > > Hi, > 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? > 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? > > Thank you very much 11.0.0 does introduce a config option CONFIG_KERNEL_MCS (KernelIsMCS in CMake). You could start with the MCS tutorial: https://docs.sel4.systems/Tutorials/mcs.html. Alternatively, there are MCS tests in seL4test: https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/… or examples in CAmkES: - https://github.com/seL4/camkes/tree/master/apps/cms-donate - https://github.com/seL4/camkes/tree/master/apps/cs-donate - https://github.com/seL4/camkes/tree/master/apps/cs-nodonate - https://github.com/seL4/camkes/tree/master/apps/periodic - https://github.com/seL4/camkes/tree/master/apps/event-driven - https://github.com/seL4/camkes/tree/master/apps/mcs-donate - https://github.com/seL4/camkes/tree/master/apps/mcs-nodonate I'm not aware if there is any documentation about the CAmkES app examples, but I believe they are supposed to demonstrate different scheduling scenarios using MCS. > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

"Ran out of untyped memory"
by Michael Neises 26 Aug '20

26 Aug '20

Hello, I'm trying to build a camkes app, but when I attempt to run it on an Odroid-xu4, I get the following error just before the boot halts: "Ran out of untyped memory while creating objects" I've narrowed the error down to two calls to a this function: https://github.com/SEL4PROJ/camkes-vm-linux/blob/dc354df3222766b9d366725751… When I use only one call, the image boots nicely. If I use both calls, I get the above error. My understanding is that this function simply adds an executable to the filesystem, so I'm not sure how to begin debugging this. Is it possible that the filesystem is actually "too big" for sel4 to boot successfully? Please advise! Best, Michael Neises

3 4

some question about mcs
by yadong.li 25 Aug '20

25 Aug '20

Hi, 1.Did seL4-11.0.0<https://docs.sel4.systems/releases/sel4/11.0.0> support mcs, I found some CONFIG_KERNEL_MCS in this release version ? or must use seL4 10.1.1-mcs <https://docs.sel4.systems/releases/sel4/10.1.1-mcs.html> branch? 2'Where I can find some example about mcs in project? The introduction of Wiki is too simple , I can 't make the param of seL4_SchedControl_Configure is correct? Thank you very much

2 1

Trouble getting a custom kernel to boot under sel4 on a tk1 board
by Travis Wheatley 25 Aug '20

25 Aug '20

I am having difficulty getting a custom kernel to boot under sel4 on a tk1 board. I have no problems building and booting an image that uses the pre-built linux-tk1-initrd file found in the projects/vm/linux folder. Howoever, when I build a “custom” kernel using buildroot-2016.08.1 as specified in this<https://docs.sel4.systems/projects/camkes-arm-vm/> the boot process hangs shortly after it loads the dtb. <<seL4(CPU 0) [decodeUntypedInvocation/212 T0xffc2d400 "rootserver" @106f0]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: map_frame_hack install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:605 module name: plat I am using the buildroot_tk1_initrd_defconfig file, also located in the projects/vm/linux folder. I am simply replacing the linux-tk1-initrd file in projects/vm/linux with the image file that gets created in the buildroot-2016.08.1/output/build/linux-custom/arch/arm/boot folder. I then clean my build directory and do the requisite “../init-build.sh -DPLATFORM=tk1 -DCAMKES_VM_APP=vm_minimal” followed by “ninja”. I then put the capdl-loader-image-arm-tk1 file on an SD card, put it in the Tk1 and do: “fatload mmc 1 0x82000000 <filename>” followed by “bootefi 0x82000000” Assuming the guidance on buildroot and the defconfig supplied match what was used to create the working pre-built linux-tk1-initrd kernel the “custom” kernel I built should be very similar. So, what am I missing? Why would a custom kernel hang at the above mentioned point in the boot process?

1 0

Porting Sel4 with RPi 3B+
by 萧琒 21 Aug '20

21 Aug '20

Hi, Professional Devel Support of Sel4, We are porting Sel4 with RPi 3B+, but we fail to boot RPi 3B+ with Sel4 successfully. We cann't find the problem, please help us. we follow the Steps: 1. Use Raspberry Pi Imager v1.4 to burn the operation system (Raspberry Pi OS Lite 32bit) on SD card, and it works well with hardware of RPi 3B+. 2. Build Sel4test-manifest: 2.1 clone the repo of https://github.com/seL4/sel4test-manifest.git 2.2 build image with ../init-build.sh -DPLATFORM=rpi3 -DAARCH32=1 2.3 the image file (sel4test-driver-image-arm-bcm2837) is produced successfully. 3. Following the SD card setup, Copy the following files to root direcctory of SD. 3.1 sel4test-driver-image-arm-bcm2837 3.2 bootcode.bin and start.elf from https://github.com/raspberrypi/firmware/tree/master/boot 3.3 u-boot.bin downloaded from https://sel4.systems/Info/Docs/u-boot-working-rpi3-32bit-v2017.11.bin 3.4 Add enable_uart=1 and kernel=u-boot.bin to the bottom of config.txt 3.5 uboot.env, we fail to find the file, so we don't use the file. if you know the step to produce uboot.env, please lead us. 4. Re-insert SD into the RPi3B+, and power the RPi3B+ on, the RPi3B+ shows the U-Boot successfully. 4.1 sel4test-driver-image-arm-bcm2837 image file’s name printed out with the command of "fatls mmc 0" 4.2 fatload the image with command of "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2837", the result: reading sel4test-driver-image-arm-bcm2837 4791000 bytes read in 406 ms (11.3 MiB/s) 4.3 bootelf 0x10000000, the result: CACHE: Misaligned operation at range [0082a000, 0082a034] CACHE: Misaligned operation at range [0082b000, 00834fcc] CACHE: Misaligned operation at range [00834fcc, 00835b07] CACHE: Misaligned operation at range [00c9be40, 00c9be9c] CACHE: Misaligned operation at range [00c9be9c, 00c9bec8] ## Starting application at 0x0082a000 ... Then, RPi3B+ is blocked and without anything else to display ! ---- Thanks, Alen 肖月振（萧琒）阿里云事业群-IOT事业部-飞天六十四部电话：13391191786 邮箱：yuezhen.xyz(a)alibaba-inc.com

2 1

Re: [seL4] Devel Digest, Vol 75, Issue 8
by Cedric MAIRE 19 Aug '20

19 Aug '20

Hi Luke, Thanks for your help! I just tried out your solution and get back the following error: `groupmod: GID '1000' already exists`. Here is the workflow that I follow: ``` $ git clone https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git $ cd ~/sel4/seL4-CAmkES-L4v-dockerfiles/ $ git pull # Make sure to be up-to-date. $ git checkout fix_rust $ git pull # Make sure to be up-to-date. `fix_rust` is ahead of `master` so no missing commits. $ ./build.sh -p -b camkes -s rust $ make user CAMKES_IMG=camkes-rust HOST_DIR="~/sel4/" ``` I attached a more detailed log of the error I get. The command throwing this is (full command in log file): `/bin/sh -c groupadd -fg ${GID} ${GROUP} [...] && chmod -R ug+rw /home/${UNAME}` Does this look familiar to you? Best, Cedric -----Original Message----- From: Devel <devel-bounces(a)sel4.systems> On Behalf Of devel-request(a)sel4.systems Sent: samedi, 15 août 2020 04:00 To: devel(a)sel4.systems Subject: Devel Digest, Vol 75, Issue 8 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Dockerfiles - "camkes-rust" Image (Mondy, Luke (Data61, Kensington NSW)) ---------------------------------------------------------------------- Message: 1 Date: Fri, 14 Aug 2020 06:29:32 +0000 From: "Mondy, Luke (Data61, Kensington NSW)" <Luke.Mondy(a)data61.csiro.au> To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] Dockerfiles - "camkes-rust" Image Message-ID: <SYAPR01MB25284E1D39674828FDC11EBED5400(a)SYAPR01MB2528.ausprd01.prod.outlook.com> Content-Type: text/plain; charset="us-ascii" Hello Cedric, Thanks for the report. I believe the best way to use the camkes-rust image is to run this: make user CAMKES_IMG=camkes-rust However, in saying that, it unfortunately does not perform quite as hoped. Because of the way the code is built, it ends up putting the Cargo/Rust content into /root/.cargo, which is inaccessible to you as a non-root user. This is an oversight on my part, as unfortunately these interactive bits of the Dockerfile system don't get tested automatically. I've made a PR on GitHub, which shows the fixes needed: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles/pull/24 Note that the master branch has also been recently updated, so you may need to pick further commits from there (or simply pull them all down first) for things to work. Let me know if that helps. Cheers, Luke -- Dr Luke Mondy, Systems Administrator, P +61 2 9490 5773 | https://ts.data61.csiro.au/?mc_phishing_protection_id=28047-bsrk3aadu815grd… Trustworthy Systems | DATA61 | CSIRO CSIRO Staff Association Delegate Hours at CSIRO Monday: 9:00am to 5pm Tues, Wed, Fri: 1:30pm to 5pm ________________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Cedric MAIRE <cmaire(a)icrc.org> Sent: Friday, 14 August 2020 2:42 AM To: devel(a)sel4.systems Subject: [seL4] Dockerfiles - "camkes-rust" Image Dear seL4 developers, I am using the provided dockerfiles repository to build the docker images in order to compile seL4. I would like to add a rust compiler to my docker image, which I do with "./build.sh -p -b camkes -s rust". This builds an image tagged "trustworthysystems/camkes-rust". I would like to launch this image in a container using the "Makefile" as I would do for the "trustworthysystems/camkes" image (using "make user"). I tried adding targets to the "Makefile" file changing the "USER_BASE_IMG" variable to use "trustworthysystems/camkes-rust" instead of "trustworthysystems/camkes", without success. I also tried to force the image by renaming/retagging "trustworthysystems/camkes " to "trustworthysystems/camkes-old" and "trustworthysystems/camkes-rust" to "trustworthysystems/camkes ". I also forced every base image to be the one containing the Rust compiler (in "Makefile"). All without success. For some reason "trustworthysystems/camkes-rust" image is never used. If I start it manually using docker commands I am able to launch and attach to it, getting the expected Rust compiler. Through the "Makefile" it ever only uses "trustworthysystems/camkes" without the Rust compiler. Is there an easy way to get this to work? What am I missing? Best regards, Cedric =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. =============================================================================== _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel?mc_phishing_protection_id=28047-b… ------------------------------ End of Devel Digest, Vol 75, Issue 8 ************************************ =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 1

Dockerfiles - "camkes-rust" Image
by Cedric MAIRE 14 Aug '20

14 Aug '20

Dear seL4 developers, I am using the provided dockerfiles repository to build the docker images in order to compile seL4. I would like to add a rust compiler to my docker image, which I do with "./build.sh -p -b camkes -s rust". This builds an image tagged "trustworthysystems/camkes-rust". I would like to launch this image in a container using the "Makefile" as I would do for the "trustworthysystems/camkes" image (using "make user"). I tried adding targets to the "Makefile" file changing the "USER_BASE_IMG" variable to use "trustworthysystems/camkes-rust" instead of "trustworthysystems/camkes", without success. I also tried to force the image by renaming/retagging "trustworthysystems/camkes " to "trustworthysystems/camkes-old" and "trustworthysystems/camkes-rust" to "trustworthysystems/camkes ". I also forced every base image to be the one containing the Rust compiler (in "Makefile"). All without success. For some reason "trustworthysystems/camkes-rust" image is never used. If I start it manually using docker commands I am able to launch and attach to it, getting the expected Rust compiler. Through the "Makefile" it ever only uses "trustworthysystems/camkes" without the Rust compiler. Is there an easy way to get this to work? What am I missing? Best regards, Cedric =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 1

QEMU, seL4, CAmkES and Linux VM - Insufficient Memory
by Cedric MAIRE 14 Aug '20

14 Aug '20

Dear seL4 developers, I am trying to setup a stack of QEMU, seL4, CAmkES and a Linux VM. I am following the tutorial on "https://docs.sel4.systems/Tutorials/camkes-vm-linux.html" and also the example on "https://github.com/seL4/camkes-vm-examples". I am running in different errors depending on which path I follow. The machine is an old MacBook Pro (running Linux, exact specs are in the main log file). - Main log file: "intel.log", contains steps and workflows - Tests: All tests seem to pass. - CAmkES VM - Tutorial Version: doesn't start QEMU because of unsupported host flags (warnings) or some failing script - CAmkES VM - Example Version: seems to boot into seL4 or even the Linux VM, but fails because of some memory error Does this look familiar to you? Best regards, Cedric Maire =============================================================================== The ICRC - working to protect and assist people affected by armed conflict and other situations of violence. Find out more: www.icrc.org This e-mail is intended for the named recipient(s) only. Its contents are confidential and may only be retained by the named recipient (s) and may only be copied or disclosed with the consent of the International Committee of the Red Cross (ICRC). If you are not an intended recipient please delete this e-mail and notify the sender. ===============================================================================

2 2

Hins for an seL4 virtio pci driver?
by Radev, Martin 10 Aug '20

10 Aug '20

Hello seL4 community, I am currently examining the possibility of using seL4 in a VM and writing a virtio driver to communicate with a virtio pci device in the HV. I looked around the available seL4 projects, and I noticed that there is the `libvirtqueue` and `libpci` projects which should come handy. However, I haven't been able to to find any other project which uses either of the libraries and I haven't found any tests for the two projects. Can you point me to projects which use these two libraries? Kind regards, Martin

2 1

SeL4 Raspberry Pi -- QEMU support
by Brendan Morgenstern 08 Aug '20

08 Aug '20

Hello, I hope all is well. I am interested in running seL4 on the Raspberry Pi, and have been following this guide<https://research.csiro.au/tsblog/sel4-raspberry-pi-3/>. I have followed the instructions and am able to generate an seL4 image correctly, however the guide is geared towards running on hardware and in fact when I run the resulting 'simulate' script I get the following. "Unsupported platform or architecture for simulation". I can run it manually under qemu to an extent with raspi2 as a machine type (): qemu-system-arm -serial null -serial mon:stdio -nographic -M raspi2 -kernel sel4test-driver-image-arm-bcm2837 And it produces this output<https://pastebin.com/LLuum55T>. It seems the image can be *run*, but it doesn't seem to work; it gets stuck on the TIMER0001 test and the previous tests produce errors. It seems that qemu can't quite emulate the raspberry pi hardware. Is there a way to run the seL4 image on the Raspberry Pi in QEMU, or can you provide an alternative for emulation, or any help whatsoever on this matter? Thank you for your time, Brendan Morgenstern ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 2