January 2022 - Devel - lists.sel4.systems

Virtual Machine and scheduling query
by Sidhartha 12 Jan '22

12 Jan '22

Hi, I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4 for the OS research project at I have a few independent questions: 1. Virtual Machines can be implemented with different levels of support from the hardware. If we talk about x86_64, in the most basic terms, you could have VMs without or without VT-X extensions. Looking at the resources available on the seL4 site, I think the given VMM libraries assume VT-X. Is there an example that does not use VT-X? 2. The scheduler inside seL4 is relatively simple. I have heard(Thanks Nick!) that if a complicated scheduling policy is desired, it can be done in userspace. A user-level component that has the capabilities to all the TCB's can play with the priority, resume/pause, and achieve any arbitrary scheduling. Is there an example available which I could look at? 3. I would like to implement a new functionality of memory quota, where different user-apps can be assigned memory quota and not just the physical pages. Does such a functionality belong in the kernel or the userspace component(say memory quota manager)? In the latter case, it would be just an endPoint capability to the quota manager service, so how does one split it - say split a quota of 100MB into two separate 50MB quotas. This is more a generic micro-kernel query rather than seL4 specific, but any insights would help. Thanks, Sid sid-agrawal.ca

1 0

sel4test AARCH64 on imx8mm-evk
by Zippy Manaic 07 Jan '22

07 Jan '22

Hi, I have tried running sel4test built for AARCH64 (https://docs.sel4.systems/Hardware/imx8mm.html) on my imx8mm-evk dev board. I am on the 12.1.0 branch of sel4test-manifest.git. Firstly I have to add "set(KernelAArch64SErrorIgnore ON)" to my build config in order to get the tests running and unfortunately things go awry during the test run ... Starting test 47: FRAMEEXPORTS0001 Running test FRAMEEXPORTS0001 (Test that we can access all exported frames) Pagefault from [FRAMEEXPORTS0001]: read fault at PC: 0x41c4ec vaddr: 0x11000000, FSR 0x92000210 Register of root thread in test (may not be the thread that faulted) Register dump: pc: 0x41c4ec sp: 0x100118a0 spsr: 0x80000040 x0: 0x11000000 x1: 0x11000000 x2: 0x55 x3: 0x15 x4: 0xe6 x5: 0x0 x6: 0x0 x7: 0xffffffffffffffff x8: 0x10011a48 x16: 0x0 x17: 0x0 x18: 0x0 x29: 0x100118a0 x30: 0x41c9f0 x9: 0x2b x10: 0x2b x11: 0xffffffff x12: 0x0 x13: 0x0 x14: 0x0 x15: 0x0 x19: 0xe7 x20: 0x8 x21: 0x11000000 x22: 0x0 x23: 0x0 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 tpidr_el0: 0x616f60 tpidrro_el0: 0x0 Failure: result == SUCCESS at line 291 of file /host/projects/sel4test/apps/sel4test-driver/src/testtypes.c Error: result == SUCCESS at line 217 of file /host/projects/sel4test/apps/sel4test-driver/src/main.c ... Starting test 55: IPC1001 Running test IPC1001 (Test SMP inter-AS seL4_Send + seL4_Recv) KERNEL DATA ABORT! Faulting instruction: 0xffffff804001e2ac FAR: 0xffffff80bf800020 ESR (DFSR): 0x96000210 halting... Kernel entry via Syscall, number: 1, Call Cap type: 10, Invocation tag: 20 Is this something that should just work? Or am I missing something. Cheers, Zippy

3 9

答复: Devel Digest, Vol 130, Issue 2
by yadong.li 03 Jan '22

03 Jan '22

Hi Matthew: Firstly, thank you for your information. form your answer, we understand the design intention of group, we Iook at compilation proces and may be find the probelm of compiler, we the assume the following scenario: The client A and client B are in the same group, they all have the same global variable like "global_buf", when use objcopy with "--keep-global-symbol" param, it will change the "global_buf" symbol form "gloabl" to "local", this change make the same name global variable of different client in same space can work well, they can access their own global variable as local variable. But In out test, we find if the "global_buf" not be initialized, in the group, there is only one "global_buf", if client A change the value of "global_buf", client B also can see the change, this is may be wrong, we find the gcc objcopy with "--keep-global-symbol" can only affect ".data" and ".bss" section, but "global_buf" which not be initialized, will place in ".common" section, "--keep-global-symbol" will not change the symbol of ".common" form global to local, this may be solved by add "-fno-common" when linker in camkes project related to "group" scenario ________________________________ 发件人: devel-request(a)sel4.systems <devel-request(a)sel4.systems> 发送时间: 2021年12月28日 9:00:05 收件人: devel(a)sel4.systems 主题: Devel Digest, Vol 130, Issue 2 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Some questions about group of camkes (adjust the format) (Matthew Fernandez) ---------------------------------------------------------------------- Message: 1 Date: Mon, 27 Dec 2021 16:26:26 -0800 From: Matthew Fernandez <matthew.fernandez(a)gmail.com> Subject: [seL4] Re: Some questions about group of camkes (adjust the format) To: "yadong.li" <yadong.li(a)horizon.ai> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems>, "xiaonan.wang" <xiaonan.wang(a)horizon.ai>, "lei.mao" <lei.mao(a)horizon.ai> Message-ID: <DA97FC78-B670-4CF7-88AC-9810B31D1015(a)gmail.com> Content-Type: text/plain; charset=utf-8 > On Dec 23, 2021, at 08:50, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi > > * We learn the group of camkes from the https://github.com/seL4/camkes-tool/blob/master/docs/index.md > * group can colocate two component instances in a single address space, we want to use the share var by this way, like directcall transfer string virtual address, But we feel confused about the global symbols who have the same symbol name include function and variable in a single address space, Their behavior seems undefined 。 My information on how this works is out of date and I can’t answer all your questions, but I can tell you how this feature was originally implemented. Single address space components were originally implemented using post-compilation symbol mangling. As you’ve noticed, naive linking of two component instances together presents two problems: 1. Unrelated homonyms between the instances now conflict. A symbol called `foo` in component instance A and a symbol called `foo` in component instance B now refer to the same thing when linked together. 2. References to glue code have the opposite problem: their names may differ in component instance A and component instance B, but need to refer to the same functions when the two are linked together. Both problems were solved with the same mechanism: GNU objcopy. The invocations to objcopy were template-generated so they could take advantage of knowledge about the system begin compiled. A generated objcopy invocation would do the following: 1. Adjust all non-generated symbols to have internal visibility. Component instance A and component instance B have already been (partially) linked, so at this point the only unresolved symbols that need to remain externally visible are those related to the connection(s) between them. This solves problem 1 above. 2. Name-mangle all remaining symbols to something prefixed with the relevant connection instance’s name. IIRC the name mangling scheme was something like ‘<connection instance name><space><original symbol name>’. This guaranteed uniqueness because <space> is not a character that existed in C or assembly symbols. Whether using a space in a symbol name is legal or not, I don’t know, but all the binutils seemed fine with this. 3. Rename the second component in the name mangling above to a common name. I don’t recall exactly how this name was chosen, but this solves problem 2 above. This sounds pretty unorthodox and brittle, but it actually worked surprisingly well. All combinations of single address space component systems seemed to Just Work, with a few notable sharp edges: * Anything involving MMIO was tricky. These symbols frequently needed to remain externally visible and the two component instances would often have differing names but the same addresses for them. * GNU ld was more or less required. The multiple steps involving partial linking was only supported by GNU ld and Gold at the time. LLVM’s lld may have caught up in the interim years. * The objcopy name mangling broke cross-section references used by GCC’s implementation of Link-Time Optimization. As a result, any LTO compilation degraded to LTO being disabled. This wouldn’t have been a big deal except that one of the primary reasons to put two components in a single address space is to enable cross-component inlining, usually facilitated by LTO. AFAICT this (playing objcopy tricks and expecting LTO to still work) was simply not a supported use case. We explored how to work around this and got some one-off efforts working for benchmarking, but proper support would have involved altering the way binutils work. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to devel-leave(a)sel4.systems ------------------------------ End of Devel Digest, Vol 130, Issue 2 *************************************

2 1

Question about the Real-time of the SEL4.
by 刘跃 Jeff Liu 01 Jan '22

01 Jan '22

Hi; As we know, seL4 is a non preemptive kernel. Is it because the kernel of seL4 is an event based model? Then why not use the thread based kernel? As far as I know, VxWorks and QNX are thread based. SeL4's view is that for non preemptive kernel, real-time performance focuses on WCET, and the faster kernel does not guarantee the real-time performance of the system. I partially agree with this view. I want to know if there are real-time comparison data?, The comparison test with VxWorks or QNX is about the real-time performance of the system. the worst case interrupt latency is the sum of both the longest region with interrupts disabled, and the time to dispatch an interrupt to a user thread. How are these two parts of time calculated? Is it the method of WCET static analysis? And Then how to improve the interrupt response time, What is the specific method to reduce interrupt latency? I think most users of seL4 are more concerned about this. I look forward to communicating and discussing with you, experts. Thanks;

2 1