Dear seL4 developers,
I am running the CAmkES VM examples from `https://github.com/seL4/camkes-vm-examples` and am able to boot the `minimal` example with:
```
$ ../init-build.sh -DSIMULATION=TRUE -DCAMKES_VM_APP=minimal
$ ninja
$ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic
```
However this example does not provide networking capabilities due to missing drivers (is that correct?). Is there a simple way I may add networking? Simply put I would like the Linux guest to be able to connect to the internet. I tried passing the QEMU parameters to setup a tap interface, which didn't help.
I also tried to use the example `cma34cr_centos` which should already provide networking but when I try to boot this example using
`qemu-system-x86_64 -m 2048 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic`
I get the following error: `create_objects@main.c:794 Ran out of untyped memory while creating objects.`. Full log output in the `.log` file.
Thanks in advance,
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.
===============================================================================
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
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
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?
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
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.
===============================================================================
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.
===============================================================================
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.
===============================================================================
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