- Devel - lists.sel4.systems

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

Re: [seL4] Understand how TLS is setup in the root server for x64
by Millar, Curtis (Data61, Kensington NSW) 26 Nov '19

26 Nov '19

Hi Alexandre, > I'm trying to understand how the TLS is setup for the root server on > x64 (to access for example the IPC buffer) > but I'm failing to connect the pieces and how the server is correctly > setting the FS register. There is detailed documentation for the TLS change on the page for RFC- 3. https://sel4.atlassian.net/browse/RFC-3 In essence, the new TLS model stores the address of the IPC buffer in a thread-local variable which must be initialised by your process or threading runtime along with general TLS intialisation. https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/functions.h#L… To assist with this there is a simple sel4runtime library which provides a minimal C-runtime and tools for initialising TLS. https://github.com/SEL4PROJ/sel4runtime On x86_64 the TLS register can be set without calling into the kernel by using the `wrfsbase` instruction or by using the `sel4runtime_set_tls_base` function from the sel4runtime library. > Now, I'm failing to find in the codebase where the ELF loader is > actually detecting the TLS segment and the according setup with the > TLS register. The ELF loader is not responsible for TLS initialisation, the C-runtime is responsible for configuring TLS of the initial thread. https://bitbucket.ts.data61.csiro.au/projects/SEL4PROJ/repos/sel4runtime/br… > Never mind, I discovered that I in order to access a TLS variable you > need to call `seL4_TCB_SetTLSBase` on seL4_CapInitThreadTCB first in > the root server, as I'm trying to work on a bare bone usage of seL4 to > better understand it, this part was not obvious from the existing more > complex samples! In general I would recommend having the initial thread in a process initialise its own TLS via the runtime and any new thread configure its own TLS in the initialisation code before the main function call of that thread with the `sel4runtime_set_tls_base`. Each new thread will also need to use `seL4_SetIPCBuffer` to initialise the IPC buffer address in its TLS before performing any invocations or any other system calls. Cheers, Curtis Millar Systems Engineer, Trustworthy Systems, CSIRO's Data61 curtis.millar(a)data61.csiro.au Data61, CSIRO Level 3, K17 Building UNSW Gate 14, Barker St Kensington NSW 2033 Australia

2 1

Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?
by Nogin, Aleksey 24 Nov '19

24 Nov '19

Unless I am looking in the wrong place, all the CMA34CR support was removed in https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a…. Is there something that remains? If not, what would be the best starting point to try to port a demo running on CMA34CR board from an old (early 2017) version of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)? Thanks. Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 4

Understand how TLS is setup in the root server for x64
by Alexandre Mutel 24 Nov '19

24 Nov '19

Hello! I'm trying to understand how the TLS is setup for the root server on x64 (to access for example the IPC buffer) but I'm failing to connect the pieces and how the server is correctly setting the FS register. For example the sel4_Send function is codegen like this (using -ftls-model=local-exec) Function: seL4_Send push r15 mov rdx,0FFFFFFFFFFFFFFFDh push rbx mov rax,[fs:0] mov r10,[rax+8] mov r8,[rax+10h] mov r9,[rax+18h] mov r15,[rax+20h] mov rbx,rsp syscall mov rsp,rbx pop rbx pop r15 ret The instruction `mov rax,[fs:0]` is accessing the seL4_IPCBuffer* and the the executable has a TLS segments of 8 bytes for the pointer. all good. Now, I'm failing to find in the codebase where the ELF loader is actually detecting the TLS segment and the according setup with the TLS register. And I'm wondering if the setup for the codegen is not wrong on my side (e.g the local-exec is not working), so that instead of having a FS register it would be a direct memory access. Does anyone have a clue about this? Thank you!

1 2

Fwd: port sel4 to RK3308(quad cortex-a35)
by Yun Zhou 22 Nov '19

22 Nov '19

---------- Forwarded message --------- 发件人： Yun Zhou <shiny725829(a)gmail.com> Date: 2019年10月25日周五下午9:52 Subject: port sel4 to RK3308(quad cortex-a35) To: <devel-owner(a)sel4.systems> Dear sel4 Experts How are you I found some information about sel4, and sel4 is great microkernel OS, i want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal processing. Form the Tutorials I found sel4 just support cortex-a53, I would like to ask does sel4 support cortex-a35 SMP mode. and because our application is real time audio processing so system delay must lower than 3ms and hard real-time determinism. Will sel4 support real-time signal processing? Looking forward to your reply Thanks &Kind regards Yun

2 1