- Devel - lists.sel4.systems

Error while building in docker
by Edward Sandberg 09 Jan '20

09 Jan '20

This morning I saw this error when building sel4: /bin/sh: 1: PROTOBUF_PROTOC_EXECUTABLE-NOTFOUND: not found I noticed a warning when starting the docker container about trustworthysystems/camkes:latest being over 30 days old. I thought that using an up to date pull of: https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles.git would keep the build env up to date but that apparently is either not the case or there is a problem with the repo. I ran: docker pull trustworthysystems/camkes and the warning was resolved and I could build seL4. Is pulling that docker image supposed to be necessary? Thanks! -- Edward Sandberg Adventium Labs 111 3rd Avenue S. Suite #100 Minneapolis, MN 55401 ed.sandberg(a)adventiumlabs.com

2 1

fastpath performance test
by Dd Nirvana 05 Jan '20

05 Jan '20

Hi guys, I have downloaded the lastest seL4 repo and built the seL4 kernel. And I reuse the code in sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c. To test the fast, I made minor modifications: first, set caller and callee to the same priority; second, caller uses seL4_Call while callee uses seL4_ReplyRecv. However, the fastpath takes more than 2000 cycles (a round trip). Build: use the lastest provided docker and ../init-build.sh - DPLATFORM=x86_64 -DCMAKE_BUILD_TYPE=Release Both hardware and Qemu show similar results. (4.0GHz skylake CPU) BTW. The manifest is the same as https://sel4.systems/About/Performance/home.pml (i.e., bf13e9f673484825a60f9950cf688ff33ac841ad). Any advices about the issue? Best, Jinyu Gu, Institute of Parallel and Distributed Systems (IPADS), School of Software, Shanghai Jiao Tong University

2 1

Understand seL4 x86_64 Kernel ABI calling convention
by Alexandre Mutel 03 Jan '20

03 Jan '20

Hello! While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall: SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9 SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9 SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15 So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9. (Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)

1 1

Hardware-aided Trusted Computing devroom at FOSDEM
by Vasily A. Sartakov 01 Jan '20

01 Jan '20

Hello I would like to invite your to participate in a new devroom: Hardware-aided Trusted Computing. The devroom is devoted to open source projects on top of modern TEEs like Intel SGX, AMD SEV/SVE, Arm TrustZone. You can find the schedule here: https://fosdem.org/2020/schedule/track/hardware_aided_trusted_computing/ I hope this will be interesting for the community. See you at FOSDEM. -- Dr.-Eng. V. A. Sartakov

2 1

some question about the compile of global-components in camkes_arm_vm project
by yadong.li 28 Dec '19

28 Dec '19

hi， I have some question about the compile of global-components in camkes_arm_vm project. 1、In projects/global-components/components, there are some directory include FileServer, SerialServer, TimeServer and the others. I found FileServer had been compiled to project， but the other directory have not been compiled Is there some on-off switch control the compile ？ But I did not find it. 2、The CAmkES of FileServer component did not have a "int run(void) {}, If I want to add an new component with run entry， but it is not rootserver（I think one project only have one rootserver），it run with vm rootserver parallelly？ what should I do ？ Is there some example. Thank you very much

1 0

Camkes Project on Sabre Lite i.mx6 board
by Parvaneh Ahgajani 19 Dec '19

19 Dec '19

Hello all, I am trying to have my own seL4 demo on Sabre Lite board. I am using this command to create the image file: ../init-build.sh -DPLATFORM=sabre -DCROSS_COMPILER_PREFIX=arm-linux-gnueabi- -DCAMKES_APP=adder After that I run this commands to boot the image: fatload mmc 1 0x41000000 adder(image file) The bootm command gives this error: Wrong Image Format for bootm command ERROR: can't get kernel image! I tried bootelf but it stuck and does not show the correct answer: bootelf 0x41000000 CACHE: Misaligned operation at range [10598000, 105980a4] CACHE: Misaligned operation at range [10599000, 105a3434] CACHE: Misaligned operation at range [105a3434, 105a3c23] CACHE: Misaligned operation at range [107fc000, 1080a038] ## Starting application at 0x10598000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[10598000..1080a037] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 1069c064. Loaded DTB from 1069c064. paddr=[10038000..10042fff] ELF-loading image 'kernel' paddr=[10000000..10037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'capdl-loader' paddr=[10043000..1019bfff] vaddr=[10000..168fff] virt_entry=188dc ELF loader relocated, continuing boot... Enabling MMU and paging It seems It does not go to kernel-image entry point and bootstrap the kernel! Is there any thing that I need to perform on board? Thank you, Parvaneh Aghajani.

2 1

Blog on seL4 licensing
by Heiser, Gernot (Data61, Kensington NSW) 10 Dec '19

10 Dec '19

The question of what the seL4 license actually means, in particular, to which degree it may force deployer’s IP to be open-sourced (*), has come up repeatedly, and from informal discussions I realised that misconceptions abound. I tried to clear up such confusion in a blog that I just posted: https://microkerneldude.wordpress.com/2019/12/09/what-does-sel4s-license-im… Enjoy, Gernot (*) short answer: normally not at all!

1 0

try to add vm in zynqmp, but when run rootserve crash.
by yadong.li 03 Dec '19

03 Dec '19

hi： I try add vm in zynqmp, but when run rootserve crash. print See appendix for the log Function call stack create_objects for (int ut_index = 0; ut_index < spec->num_untyped; ut_index++) { .... CDL_Object *obj = &spec->objects[obj_id]; CDL_ObjectType capdl_obj_type = CDL_Obj_Type(obj); ----case crash } I fount when it access 0x440010 (the 42th of capdl_spec.objs, 0~41 objs access is OK) which is (CDL_Object)obj->type will case the crash, but I access the 42th obj->name ("frame_vm0_group_bin_0132" can be printed) is OK. [42] = { #ifdef CONFIG_DEBUG_BUILD .name = "frame_vm0_group_bin_0132", #endif .type = CDL_Frame, .size_bits = 21, .frame_extra = { .paddr = 0, }, }, what may be the problem ? mmu? Thank you very much. log: ## Starting application at 0x02793000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[2793000..481106f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 2878d08. Loaded DTB from 2878d08. paddr=[239000..23afff] ELF-loading image 'kernel' paddr=[0..238fff] vaddr=[ff8000000000..ff8000238fff] virt_entry=ff8000000000 ELF-loading image 'capdl-loader' paddr=[23b000..2393fff] vaddr=[400000..2558fff] virt_entry=408af8 ELF loader relocated, continuing boot... Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 33333000, expected 100000000 Bootstrapping kernel Booting all finished, dropped to user space Caught cap fault in send phase at address (nil) while trying to handle: vm fault on data at address 0x440010 with status 0x93800007 in thread 0xff887f81b400 "rootserver" at address 0x4026e4 With stack: 0x2553d50: 0x424a9a 0x2553d58: 0x43ffb8 0x2553d60: 0x2553de0 0x2553d68: 0x408a4c 0x2553d70: 0x255a000 0x2553d78: 0x453588 0x2553d80: 0x0 0x2553d88: 0x25 0x2553d90: 0x900000000 0x2553d98: 0x100000000000009 0x2553da0: 0x800000000 0x2553da8: 0x43ffb8 0x2553db0: 0x2186 0x2553db8: 0x21dd 0x2553dc0: 0x2a 0x2553dc8: 0x408a40

1 0

Userspace debugging with QEMU/gdb
by Jiusheng Liu 02 Dec '19

02 Dec '19

Hi, >From the page https://docs.sel4.systems/DebuggingGuide.html (section Userspace debugging), I know we can debug userspace process by command below: ---------------------------- cmd example start ---------------------------------------- gdb ./dynamic-2 Reading symbols from ./dynamic-2...done. (gdb) target remote :1234 Remote debugging using :1234 0x000000000000fff0 in ?? () (gdb) break main Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161. (gdb) c Continuing. Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161 161 (gdb) ---------------------------- cmd example end ---------------------------------------- It works for normal userspace process (such as the example code in tutorials: https://docs.sel4.systems/Tutorials/dynamic-2.html ). But when I want to debug the userspace process for the code in the tutorials page https://docs.sel4.systems/Tutorials/camkes-vm-linux.html (one virtual machine in seL4), I cannot catch the breakpoints. So can you help me to explain why I cannot catch the breakpoint? and can we debug the vmm create process with qemu/gdb? Thanks.

2 2

Re: [seL4] Devel Digest, Vol 66, Issue 26
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

> As I'm playing with a prototype language and OS while building it on > top of seL4, > I'm not using any intermediate C layers to connect to the seL4 API (so > custom build and > integration and no C runtime), while most of the samples out there are > heavily relying on > some foundations, which is completely understandable, considering how > it can be involving > to build anything relevant on top of the seL4 API. > So as I'm just really getting started to integrate with seL4 (and > I love?? it!) I have to go through > all these details, but I hope that I won't be spamming unnecessarily > here! ? If you are looking to avoid any C interop or runtime that should be completely possible. The only requirement the kernel makes is that user- level code needs to keep track of the IPC buffer address on its own (unlike previous versions which ensure that a particular register contains the IPC buffer address). If you want a minimal runtime without TLS you could store the IPC buffer address in a global variable and ensure that your system call wrappers use that global variable to load and store data into the IPC buffer.

1 0