- Devel - lists.sel4.systems

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 03 Jul '20

03 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 02 Jul '20

02 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

Re: [seL4] ramdisk vs. persistant rfs in VMs.
by Travis Wheatley 27 Jun '20

27 Jun '20

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?

1 0

ramdisk vs. persistant rfs in VMs.
by Travis Wheatley 25 Jun '20

25 Jun '20

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

2 3

CAmkES VM rootfs.cpio with Python3 Causes Error
by Turner, Ben 12 Jun '20

12 Jun '20

Hi, I have been attempting to create a VM to run as a CAmkES component, and it is a requirement that it has Python3. I have been using the vm_minimal app as a template to get started, and was successful at getting my own buildroot filesystem image running, however when I attempted to add the Python3 package, the resulting image resulted in the following error when it booted: ... <<seL4(CPU 0) [decodeInvocation/631 T0xfec34400 "rootserver" @106f0]: Attempted to invoke a null cap> create_objects@main.c:805 [Err seL4_InvalidCapability]: Untyped retype failed with unexpected error seL4 root server abort()ed Debug halt syscall from user thread 0xfec34400 "rootserver" halting... Kernel entry via Unknown syscall, word: 1 The only change I made to the image was to add the Python3 package, and that has caused this error. Is there something the vm_minimal app is missing that is required in order to get Python3 working? Kind regards, Ben Turner ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

2 5

camkes-vm-linux tutorial issue
by Nanfang Hu 11 Jun '20

11 Jun '20

When I try to build the tutorial and run ninja I got the following error. [1/31] Performing build step for 'hello-app' ninja: no work to do. [3/31] Performing configure step for 'poke-module' FAILED: poke-module-stamp/poke-module-configure cd /home/weiqi/test/camkes-vm-linux_build/poke-module && /usr/local/bin/cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_TOOLCHAIN_FILE=/home/w eiqi/test/tools/seL4/cmake-tool/polly_toolchains/linux-gcc-32bit-pic.cmake -DLINUX_KERNEL_DIR=/home/weiqi/test/camkes-vm-linux_build/out/linux-4.8.16 -DMODULE_HELPERS_FILE=/home/weiqi/test/projects/camkes-vm-linux/linux-module-helpers.cmake -GNinja /home/weiqi/test/camkes-vm-linux/modules && /usr/local/bin/cmake -E touch /home/weiqi/test/camkes-vm-linux_build/poke-module-stamp/pok e-module-configure CMake Warning (dev) in CMakeLists.txt: No project() command is present. The top-level CMakeLists.txt file must contain a literal, direct call to the project() command. Add a line of code such as project(ProjectName) near the top of the file, but after cmake_minimum_required(). CMake is pretending there is a "project(Project)" command on the first line. This warning is for project developers. Use -Wno-dev to suppress it. -- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit CMake Error at CMakeLists.txt:11 (DefineLinuxModule): DefineLinuxModule Function invoked with incorrect arguments for function named: DefineLinuxModule -- Configuring incomplete, errors occurred! See also "/home/weiqi/test/camkes-vm-linux_build/poke-module/CMakeFil es/CMakeOutput.log". See also "/home/weiqi/test/camkes-vm-linux_build/poke-module/CMakeFil es/CMakeError.log". [4/31] Completed 'hello-app' ninja: build stopped: subcommand failed. >

2 2

question about creating threads in sel4 based system
by sergey volkovich 10 Jun '20

10 Jun '20

Cabulertion. I trying to create my own sel4 based system, and currently i cannot understand next thing after calling seL4_Untyped_Retype i will be must somehow put execution data in memory. It can be implemented by using seL4_TCB_WriteRegisters. -- sever99

2 1

RISC-V (RV64) is the third ISA with verified seL4
by Heiser, Gernot (Data61, Kensington NSW) 09 Jun '20

09 Jun '20

Dear seL4 community, I’m extremely pleased to announce that we have completed the functional correctness proof of seL4 on the RV64 ISA. Congratulations to our awesome Proof Engineering Team on achieving this major milestone for seL4! And many thanks to HENSOLDT Cyber for making it possible. My blog discusses provides a bit more context for this announcement: https://microkerneldude.wordpress.com/2020/06/09/sel4-is-verified-on-risc-v/ What we have now is the refinement proof from the seL4 formal spec to the C implementation, putting RV64 on the same level as x64 in terms of seL4 verification. The binary verification, which extends this refinement to the binary code of the kernel is progressing, stay tuned for more news on that in the foreseeable future. Gernot for the Trustworthy Systems team and the seL4 Foundation

1 0