Devel July 2019

devel@sel4.systems

13 participants
13 discussions

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

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Initialising Camkes App before another dependent Camkes app
by yogidk . 03 Oct '19

03 Oct '19

Hi, I have a Camkes app (app1) which depends on another Camkes app (app2), which means my app1 must start only after app2 is completely initialized. For this currently I use a signal RPC wait in app1 and the corresponding RPC emit from app2 after app2 is completely initialized. Is there any other way in CamkES which will ensure that app1 starts only after app2 is completely initialized without using RPC signalling (emit and wait) ? How can this dependency be built ? Regards yk

3 2

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

seL4_FailedLookup in vmware
by KAP Benjamin 03 Oct '19

03 Oct '19

Hello I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine. However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file. For the ethernet configuration I used linux in the same VM to figure out the details: 1) ip addr: 2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000 link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff 2) lspci -vvv: 02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10) Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971 Physical Slot: 32 Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx- Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx- Latency: 64 (1500ns min, 63750ns max) Interrupt: pin A routed to IRQ 18 Region 0: I/O ports at 2000 [size=128] [virtual] Expansion ROM at fd500000 [disabled] [size=64K] Kernel driver in use: pcnet32 Kernel modules: pcnet32 3) dmesg | grep "02:00.0": ... [ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref] ... 4) lspci -nn: 02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10) And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified): picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a]; .... hwethdriver.mmio_paddr = 0xfd500000 hwethdriver.mmio_size = 0x10000 hwethdriver.irq_irq_type = "pci"; hwethdriver.irq_irq_ioapic = 0; hwethdriver.irq_irq_ioapic_pin = 18; hwethdriver.irq_irq_vector = 18; ethdriver.iospaces = "0x0:0x02:0x00:0"; ethdriver.iospace_id = 0x0200; ethdriver.pci_bdf = "0x02:0x00.0"; I am sorry to bother you with this; I am fairly new to low level stuff. Any help would be very much appreciated. Best regards, Benjamin

2 1

Shared memory in CapDL
by Norrathep Rattanavipanon 12 Aug '19

12 Aug '19

Hi, I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed? Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

SeL4 on 32 bit RISC-V
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu-toolchain (is there a specific release I should try?). I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output: > ./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 > /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike > bbl loader > /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) > Power off Are there any tricks for getting this working right now? Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

3 5

CAmkES Tutorial Generation Issues
by Austin Owens 23 Jul '19

23 Jul '19

Hello, I am able to generate, build, and execute the majority of tutorials using init, ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues generating the tutorials specifically for the CamkES tutorials. I have installed all of the system requirements and I am running on Ubuntu 18. The output I get is the following: # ./init --tut hello-camkes-0 loading initial cache file ../settings.cmake -- The C compiler identification is GNU 7.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 7.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- CPIO test cpio_reproducible_flag FAILED -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle is out of date. Regenerating... -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/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 tools/seL4/cmake-tool/helpers/make.cmake:19 (file): file failed to open for reading (No such file or directory): /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1 Call Stack (most recent call first): tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList) tools/camkes/camkes.cmake:460 (execute_process_with_stale_check) hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) CMake Error at tools/camkes/camkes.cmake:480 (message): Failed to generate /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake Call Stack (most recent call first): hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/root/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 "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../settings.cmake .. STDOUT: STDERR: I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything to do with deps_1 file not being present. It's not possible to copy the deps_0 file to deps_1 since calling the './init --tut hello-camkes-0' command again creates a new project directory. Is there something obvious that I am missing? Thanks, Austin

3 4

Autocorres tutorial for Isabelle/HOL beginner
by Norrathep Rattanavipanon 22 Jul '19

22 Jul '19

Hello, I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL. I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output: ``` Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Statespace Session HOL/HOL-Word (main timing) Session Lib/Word_Lib (lib) Session Lib/Lib (lib) Session C-Parser/Simpl-VCG Session C-Parser/CParser Session Lib/CLib (lib) Session Unsorted/AutoCorres Session Unsorted/AutoCorresTest Building AutoCorresTest ... AutoCorresTest: theory AutoCorresTest.CustomWordAbs AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation ... Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23) ``` But I couldnt find any Isabelle definitions as output except "thy" files that contain: ``` theory somefile imports "AutoCorres.AutoCorres" begin external_file "somefile.c" install_C_file "somefile.c" autocorres "somefile.c" end ``` I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated. Best Regards, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 on the Xilinx Zynq US+ ZCU104 Evaluation Kit
by derek65 22 Jul '19

22 Jul '19

Hi, I'm interested in running sel4 on a Xilinx Zynq UltraScale+ MPSoC evaluation board. I read the great blog post about the port from DornerWorks [1] and checked the sel4 hardware support page here [2]. Since the Zynq ZCU102 Evaluation Kit listed is quite expensive, I wanted to ask if anyone tried the procedure described in the blog post on the much cheaper Xilinx US+ ZCU104 Evaluation Kit. Might this work as well? Thanks! Kind regards, - derek [1] - https://dornerworks.com/blog/hardware-security-growing-concern-sel4-ecosyst… [2] - https://docs.sel4.systems/Hardware/

4 3

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel July 2019