- Devel - lists.sel4.systems

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

20 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 13 Aug '20

13 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 07 Aug '20

07 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

Re: [seL4] [seL4 Announce] UNSW seL4 teaching videos available
by Heiser, Gernot (Data61, Kensington NSW) 02 Aug '20

02 Aug '20

I’ve (almost) finished teaching and all seL4-related videos from my Advanced OS course are now up on YouTube, details below. Gernot > On 2 Jun 2020, at 10:50, Announcements about seL4 -- low volume list <announce(a)sel4.systems> wrote: > > Dear seL4 community, > > I’m pleased to announce yet another contribution of UNSW Sydney to the seL4 community: This year I’m making the seL4-related videos from my UNSW Advanced Operating Systems class freely available. You’ll find them at the UNSW CSeLearning COMP9242 YouTube channel: https://www.youtube.com/playlist?list=PLbSaCpDlfd6qLbEsKquVo3--0gwYBmrUV > > At present there are the first two modules, which provide some background on microkernels and seL4, and discuss the seL4 API. More material will show up over the next two months. > > The complete course material, including all lecture slides, the project spec and code, are available, as always, from the COMP9042 web site: https://www.cse.unsw.edu.au/~cs9242/current/ > > Enjoy, > Gernot

1 0

help with tutorial
by Sachin More 02 Jul '20

02 Jul '20

Hi: I am new to L4 and have been working through the tutorials. However, I am having a problem doing the hello-camkes-0 tutorial. When I try to install the tutorial, I get the output below. Looks like a file hello-camkes-0_build/camkes_gen/deps_1 is not there. Any help would be greatly appreciated! thanks, Sachin $ ./init --tut hello-camkes-0 loading initial cache file ../projects/sel4-tutorials/settings.cmake -- Found capdl: /compile/sel4-tutorials-manifest/projects/capdl CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) This warning is for project developers. Use -Wno-dev to suppress it. -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/sel4-tutorials CMake Warning (dev) at /usr/share/cmake3/Modules/FindPackageHandleStandardArgs.cmake:272 (message): The package name passed to `find_package_handle_standard_args` (camkes-tool) does not match the name of the calling package (sel4-tutorials). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:67 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/settings.cmake:96 (find_package) CMakeLists.txt:3 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- The C compiler identification is GNU 7.3.1 -- The ASM compiler identification is GNU -- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc - works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Found camkes-tool: /compile/sel4-tutorials-manifest/projects/camkes-tool -- Found seL4: /compile/sel4-tutorials-manifest/kernel -- Found elfloader-tool: /compile/sel4-tutorials-manifest/tools/seL4/elfloader-tool -- Found musllibc: /compile/sel4-tutorials-manifest/projects/musllibc -- Found util_libs: /compile/sel4-tutorials-manifest/projects/util_libs -- Found seL4_libs: /compile/sel4-tutorials-manifest/projects/seL4_libs -- Found projects_libs: /compile/sel4-tutorials-manifest/projects/projects_libs -- Detecting cached version of: capDL-tool -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- Found sel4runtime: /compile/sel4-tutorials-manifest/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- Detecting cached version of: musllibc -- No cache path given. Set SEL4_CACHE_DIR to a path to enable caching binary artifacts. -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/ast.pickle is out of date. Regenerating... -- /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes-gen.cmake is out of date. Regenerating... CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable. CMake Error at /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:13 (file): file failed to open for reading (No such file or directory): /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes_gen/deps_1 Call Stack (most recent call first): /compile/sel4-tutorials-manifest/tools/seL4/cmake-tool/helpers/make.cmake:71 (MakefileDepsToList) /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:503 (execute_process_with_stale_check) CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) CMake Error at /compile/sel4-tutorials-manifest/projects/camkes-tool/camkes.cmake:523 (message): Failed to generate /compile/sel4-tutorials-manifest/hello-camkes-0_build/camkes-gen.cmake Call Stack (most recent call first): CMakeLists.txt:17 (GenerateCAmkESRootserver) /compile/sel4-tutorials-manifest/projects/sel4-tutorials/Findsel4-tutorials.cmake:29 (include) CMakeLists.txt:4 (sel4_tutorials_regenerate_tutorial) -- Configuring incomplete, errors occurred! See also "/compile/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 106, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/compile/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 74, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 1549, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 793, in __init__ self.wait() File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 849, in wait self.handle_command_exit_code(exit_code) File "/net/freenas/mnt/freenas-4TB/smore/.local/lib/python3.6/site-packages/sh.py", line 877, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../projects/sel4-tutorials/settings.cmake /compile/sel4-tutorials-manifest/hello-camkes-0 STDOUT: STDERR:

2 2

Confirming correct syntax of items in devices.camkes.
by Travis Wheatley 01 Jul '20

01 Jul '20

I have been attempting to add support for both USB and SD persistent memory to my vm (See "Re: ramdisk vs. persistant rfs in VMs.” thread.). I seem to be having a problem with power management. In hopes of correcting this I wish to expose the power management unit to the VM. The related stanza looks like this in my device tree file. cci@fd6e0000 { compatible = "arm,cci-400"; reg = <0x0 0xfd6e0000 0x0 0x9000>; ranges = <0x0 0x0 0xfd6e0000 0x10000>; #address-cells = <0x1>; #size-cells = <0x1>; pmu@9000 { compatible = "arm,cci-400-pmu,r1"; reg = <0x9000 0x5000>; interrupt-parent = <0x4>; interrupts = <0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4 0x0 0x7b 0x4>; }; }; The PMU appears to be a child of cci. I am unsure of the proper syntax to use in my devices.camkes file. Since it is a child does one specify the path as /cci/pmu? Does the parent also have to be exposed to the vm? Here is what the related lines inmy devices.camkes look like. Is this correct? vm0.dtb = dtb([ {"path": "/cci@fd6e0000"}, {"path": "/cci/pmu@9000"},

1 0

Re: [seL4] ramdisk vs. persistant rfs in VMs.
by Zhuang, Siwei (Data61, Kensington NSW) 27 Jun '20

27 Jun '20

Hi Travis, It looks like the issue is related to the power management. You may need to read the board's manual(e.g UG1085) to find out if USB and SDHCI rely on any other devices which you also need to pass through to your Linux VM. You may also try to recompile your Linux kernel with PM disabled. If it doesn't work for you, then you'll have to debug your Linux kernel to find the root cause of the error. Good Luck. - Siwei ________________________________________ From: Travis Wheatley <travis.wheatley(a)emergentspace.com> Sent: Friday, 26 June 2020 6:25 AM To: devel(a)sel4.systems Cc: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: ramdisk vs. persistant rfs in VMs. I have made some good progress thanks to Siwei’s advice. I have modified my .dts file and have made a usb controller as well as the sdhci controller available to the VM. However, there still seems to be some issues at start up. Here is what dmesg has to say about the usb controller(s) root@xilinx-zcu102-2019_1:~# dmesg | grep usb [ 1.754678] usbcore: registered new interface driver usbfs [ 1.761934] usbcore: registered new interface driver hub [ 1.768958] usbcore: registered new device driver usb [ 3.827826] usbcore: registered new interface driver asix [ 3.834976] usbcore: registered new interface driver ax88179_178a [ 3.842998] usbcore: registered new interface driver cdc_ether [ 3.850682] usbcore: registered new interface driver net1080 [ 3.858146] usbcore: registered new interface driver cdc_subset [ 3.865948] usbcore: registered new interface driver zaurus [ 3.873301] usbcore: registered new interface driver cdc_ncm [ 3.895799] usbcore: registered new interface driver uas [ 3.902820] usbcore: registered new interface driver usb-storage [ 3.916716] usbcore: registered new interface driver uvcvideo [ 3.991358] usbcore: registered new interface driver bcm203x [ 3.998824] usbcore: registered new interface driver bpa10x [ 4.006182] usbcore: registered new interface driver bfusb [ 4.013424] usbcore: registered new interface driver btusb [ 4.028142] usbcore: registered new interface driver ath3k [ 4.201363] usbcore: registered new interface driver usbhid [ 4.208699] usbhid: USB HID core driver [ 4.224831] usbcore: registered new interface driver snd-usb-audio [ 5.181742] dwc3-of-simple ff9e0000.usb1: failed to add to PM domain domain3: -13 [ 5.191629] dwc3-of-simple: probe of ff9e0000.usb1 failed with error -13 Any clue? Regarding the SD card, it is partitioned with a boot partition where uboot and the .elf file live and the remainder is the free space I hope to use as the filesystem. Here is what dmesg has to say about the sdhc interface. root@xilinx-zcu102-2019_1:~# dmesg | grep sdhc [ 4.049894] sdhci: Secure Digital Host Controller Interface driver [ 4.058026] sdhci: Copyright(c) Pierre Ossman [ 4.063768] sdhci-pltfm: SDHCI platform and OF driver helper [ 5.209925] sdhci-arasan ff160000.mmc: failed to add to PM domain domain4: -13 [ 5.219468] sdhci-arasan: probe of ff160000.mmc failed with error -13 [ 5.351710] mmc0: sdhci: ============ SDHCI REGISTER DUMP =========== [ 5.360229] mmc0: sdhci: Sys addr: 0x00000000 | Version: 0x00000000 [ 5.368759] mmc0: sdhci: Blk size: 0x00000000 | Blk cnt: 0x00000000 [ 5.377280] mmc0: sdhci: Argument: 0x00000000 | Trn mode: 0x00000000 [ 290.055387] random: fast init done [ 5.385810] mmc0: sdhci: Present: 0x00000000 | Host ctl: 0x00000000 [ 5.394331] mmc0: sdhci: Power: 0x00000000 | Blk gap: 0x00000000 [ 5.402860] mmc0: sdhci: Wake-up: 0x00000000 | Clock: 0x00000000 [ 5.411381] mmc0: sdhci: Timeout: 0x00000000 | Int stat: 0x00000000 [ 5.419902] mmc0: sdhci: Int enab: 0x00000000 | Sig enab: 0x00000000 [ 5.428441] mmc0: sdhci: AC12 err: 0x00000000 | Slot int: 0x00000000 [ 5.436962] mmc0: sdhci: Caps: 0x00000000 | Caps_1: 0x00000000 [ 5.445491] mmc0: sdhci: Cmd: 0x00000000 | Max curr: 0x00000000 [ 5.454021] mmc0: sdhci: Resp[0]: 0x00000000 | Resp[1]: 0x00000000 [ 5.462551] mmc0: sdhci: Resp[2]: 0x00000000 | Resp[3]: 0x00000000 [ 5.471089] mmc0: sdhci: Host ctl2: 0x00000000 [ 5.477023] mmc0: sdhci: ============================================ Seems to be getting the same -13 error when setting up it’s domain. So… what do I need to do to make these devices accessible from the linux command line? On Jun 24, 2020, at 8:58 PM, Zhuang, Siwei (Data61, Kensington NSW) <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Travis, The addresses are board specific. The document for your board is UG1085, https://www.xilinx.com/support/documentation/user_guides/ug1085-zynq-ultras… If all you need is a number, you can also find it in the dts files in u-boot, Linux kernel or seL4, https://github.com/seL4/seL4/blob/master/tools/dts/zynqmp.dts#L900, #L910 - Siwei ________________________________________ From: Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> Sent: Thursday, 25 June 2020 5:49 AM To: devel(a)sel4.systems<mailto:devel@sel4.systems> Cc: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: ramdisk vs. persistant rfs in VMs. Thanks Siwei. This was very helpful. I do have a follow up question about the addresses used in the devices.camkes file. Are these board specific or standard locations for the microkernel? The board I am using is a zcu102. Not sure where/how to find the appropriate address to use for the sdhci device. — Travis On Jun 23, 2020, at 3:54 AM, Zhuang, Siwei (Data61, Kensington NSW) <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Travis, If you only need one VM to access the SD card. You could pass-through the SD card controller to Linux, recompile the Linux kernel with the proper driver. Then passing your rootfs on SD card via Linux kernel boot parameters. An example can be found in the "camkes-arm-vm" repo. Have a read about the "TK1 configuration" on this page, https://docs.sel4.systems/projects/camkes-arm-vm/ The configuration code can be found here, https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/apps/vm_minimal/tk1/d… https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/apps/vm_minimal/tk1/d… If you need to share the SD card between an native seL4 application and a VM or among multiple VMs, you'll need a virtual SD card driver. We only have a virtual USB driver at the moment. Use it as a reference to make your virtual driver. The code can be found here, https://github.com/SEL4PROJ/seL4_projects_libs/blob/master/libsel4vmmplatsu… https://github.com/SEL4PROJ/camkes-arm-vm/blob/master/components/VM/src/mod… You can of course partition the SD card, if your board supports boot from SD card. Consult the board's manual regarding how to boot from SD card. Note that, the Linux VM would have the access to your boot partition, hence the seL4 boot image could be compromised. To avoid that, you'll need to intercept the SD card access from the VM. The code here demonstrates one way of doing it, https://github.com/SEL4PROJ/seL4_projects_libs/blob/master/libsel4vmmplatsu… Hope these helps. - Siwei ________________________________________ From: Devel <devel-bounces(a)sel4.systems<mailto:devel-bounces@sel4.systems>> on behalf of Travis Wheatley <travis.wheatley(a)emergentspace.com<mailto:travis.wheatley@emergentspace.com>> Sent: Tuesday, 23 June 2020 6:47 AM To: devel(a)sel4.systems<mailto:devel@sel4.systems> Subject: [seL4] ramdisk vs. persistant rfs in VMs. I’ve been working with VMs running under SEL4 on ARM hardware. I have been able to boot to a command prompt in a VM. However, the filesystem being used is a ramdisk. I need some sort of persistent storage, preferably a regular rfs that lives on an SD card. Not exactly sure what modifications to make and where to cause the kernel to use a persistent rfs rather than the ramdisk. Barring that, wondering if the SD card can be divided into multiple partitions such that one can be the boot partition and the other mounted to provide persistent storage space. Hoping one of y’all can point me in the right direction. — Travis _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel

1 0