July 2018 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

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

15 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 18 May '23

18 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

seL4 - getting the execution time of different threads
by Mr. Peace 10 Sep '18

10 Sep '18

Hello together, I was wondering how you do get the execution time in seL4 if you are using multiple threads. In the initial thread I can use the timer as it is shown in the tutorial about timers since I do have the bootinfo, vka, allocman and so on. But how do I use the timer to measure the execution time of the other threads without stopping their execution to "pull" the time from the initial thread? Is it possible to share the timer or create new ones in the other threads? Or is there another way to measure the execution time? Some background information: The threads have different VSpace's and CSpace's. Used tutorials: seL4-tutorial 4, seL4-tutorial timer. The other threads do not have a bootinfo in their environment. Kind regards, Chris

4 5

How to write safe C code for free?
by Wean Irdeh 04 Aug '18

04 Aug '18

Hello. I'm a poor person looking for an advice. I know this is the right place since all of you have huge expertise in formal verification. I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?

3 2

about compile error
by wong xuguo 02 Aug '18

02 Aug '18

Dear Sir/Lady, This is a student from china, I am very interested in the sel4, works on the camkes, When I first compile the project camkes, I met a problem: camkes.c:502: undefined reference to `component_control_main' I know this means it not implemented this function, but this function seems produced by a auto method, so could you tell how to solve this problem? I follow the command: https://docs.sel4.systems/CAmkES/ to compile the : repo init -u https://github.com/seL4/camkes-manifest.git

2 1

Question about wrapper files
by Holm, Elinor M 29 Jul '18

29 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are there for testing, or something else? Elinor Holm Software Engineer 781-410-5221 This message and/or attachments may include information subject to GDC4S S.P. 1.8.6 and GD Corporate Policy 07-105 and are intended to be accessed only by authorized recipients. Use, storage and transmission are governed by General Dynamics and its policies. Contractual restrictions apply to third parties. Recipients should refer to the policies or contract to determine proper handling. Unauthorized review, use, disclosure or distribution is prohibited. If you are not an intended recipient, please contact the sender and destroy all copies of the original message.

3 2

CAmkES 3.5.0 Build Error
by Amit Goyal 27 Jul '18

27 Jul '18

Hi, I am running CAmkES 3.5.0 on Ubuntu 16.04, 64 Bit, i5 machine, CMake 3.11.4. I am getting the following error on running ../init --plat pc99 --tut hello-camkes-1 --solution (although seL4 10.0.0 works perfectly fine). ------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 58, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/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=hello-camkes-1 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- The C compiler identification is GNU 5.3.1 -- The CXX compiler identification is GNU 5.3.1 -- 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 -- 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 -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FA... (295 more, please see e.stdout) STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at tools/camkes/camkes.cmake:581 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/tools/camkes/camkes/runner/__main__.py", lin... (614 more, please see e.stderr) -------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a way around? -- Thanks and Regards, Amit Goyal

2 2

Question about wrapper files
by Holm, Elinor M 26 Jul '18

26 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are they for testing, or something else? Elinor Holm

1 0

Image lies outside of usable physical memory v2
by Jeremy Fields 26 Jul '18

26 Jul '18

http://sel4.systems/pipermail/devel/2016-July/000918.html I'm running into the same issue, with likely the same cause. I wanted to see if there is any further insight that can be given on this? I'm guessing there hasn't been any updates to seL4's memory allocation in this aspect. (I'm using seL4 9.0.1) My naive attempt of commenting out that particular check in seL4 just results in the machine hard resetting when it runs (if only it were that easy). >Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner. (2016) Any chance this is on a roadmap? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1