June 2020 - Devel - lists.sel4.systems

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

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

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