Devel December 2016

devel@sel4.systems

18 participants
15 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

Exposing ticks to the rt API
by Corey Richardson 30 Jan '17

30 Jan '17

Hi Anna, While analyzing some time related APIs, I've noticed that the x86 rt kernel assumes that the tsc frequency is constant and well represented by the measurement made at init by comparing against the PIT. It also exposes only microseconds and uses the internal calibration to convert that to/from ticks. I'm concerned about this behavior. The tsc can have up to 200ppm error if uncalibrated and not temperature controlled, from what I'm able to determine. I'd rather have all the public APIs take ticks and allow user space to determine how their timing requirements best correspond to ticks. This came up when wanting to measure how much running time a process/thread has used. Ideally, it's kept as a running count of ticks. In the current API, one can only observe microseconds consumed, converted by a potentially lossy ticksToUs (lossy when the rate isn't exactly known or tick->us conversion isn't an exact integer multiplication). It'd be more useful for me to have tick count directly. I'm also somewhat concerned with using the PIT to estimate the TSC rate, as I can't find anything about expected error of the PIT, and any slop there will influence all future kernel behaviors until reboot. One potential alternative is the ACPI PM timer or the HPET. Those run at higher frequencies, which would help reduce the error bounds on the rate estimation. Let me know what you think! If it's useful at all, I've written up some stuff about the work that inspired these thoughts: https://gitlab.com/robigalia/meta/blob/master/blog/_drafts/2016-12-23-what-… Merry Christmas, -- cmr http://octayn.net/

4 4

Workshop debrief?
by Jeff Waugh 10 Jan '17

10 Jan '17

Hey there, I might be hoping a little too much for video, but will there be slides and notes from the Workshop? (Particularly interested in the gaps discussion.) Would be handy content on the wiki. :-) Thanks, Jeff

3 4

pic/no-pic and some other questions
by Vasily A. Sartakov 06 Jan '17

06 Jan '17

Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains: 1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together. 2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: > 43b610: 27bdffe8 addiu sp,sp,-24 <— start of the function > 43b614: afbf0014 sw ra,20(sp) > 43b618: afbe0010 sw s8,16(sp) > 43b61c: afb0000c sw s0,12(sp) > 43b620: 03a0f021 move s8,sp <— frame stack > 43b624: afc40018 sw a0,24(s8) <— save 1st arg for a subroutine call > 43b628: afc5001c sw a1,28(s8) <— save 2nd arg for the subroutine > 43b62c: afc60020 sw a2,32(s8) <— save 3rd arg for the subroutine So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect? 4. Could you please tell me what was the C equivalent of this asm code: .global __syscall .type __syscall,%function __syscall: sub sp, sp, #4 push {r5,r6} adr r5, 1f ldr r6, 1f ldr r5, [r5,r6] str r5, [sp, #8] pop {r5, r6} pop {pc} .hidden __sysinfo 1: .word __sysinfo-1b something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? Thank you. P/s Happy new year/merry xmass/happy holidays! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

seL4test on Odroid-XU4
by Yevgeny Lavrov 05 Jan '17

05 Jan '17

Hello I ran into the following issue while running seL4test suite on Odroid-XU4: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 there are pending interrupts 0x00000001 reading sel4test-driver-image-arm-exynos5 3149364 bytes read Exynos5422 # bootelf 0x48000000 ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4130441f] ELF-loading image 'kernel' paddr=[60000000..60037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[60038000..60411fff] vaddr=[10000..3e9fff] virt_entry=1e74c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info .... 1 untypeds of size 10 1 untypeds of size 11 126 untypeds of size 12 2 untypeds of size 13 3 untypeds of size 14 3 untypeds of size 15 5 untypeds of size 16 3 untypeds of size 17 3 untypeds of size 18 3 untypeds of size 19 3 untypeds of size 20 2 untypeds of size 21 2 untypeds of size 22 1 untypeds of size 23 2 untypeds of size 24 2 untypeds of size 25 2 untypeds of size 26 2 untypeds of size 27 1 untypeds of size 29 Switching to a safer, bigger stack... seL4 Test ========= _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 31 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 2147483648, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 30 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 1073741824, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 29 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 536870912, error 1 ..... _utspace_split_alloc@split.c:247 Failed to find any untyped capable of creating an object at address 0x12dd0000 vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at paddr 0x12dd0000, error 1 init_timer_caps@main.c:348 [Cond failed: error] Failed to get untyped at paddr 0x12dd0000 for timer Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to running seL4test, I ran code from seL4 tutorials and those ran w/o any problems. Any suggestions on what I might have done wrong? Thanks

3 4

Exposing TSD on x86
by Corey Richardson 03 Jan '17

03 Jan '17

How do people feel about exposing the TSD (time-stamp disable) bit as a piece of state on the TCB? Ideally it'd be lazily switched. I vaguely want this in Robigalia for disabling access to real time in non-sufficiently-privileged processes. Best, -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Workshop debrief?
by Corey Richardson 20 Dec '16

20 Dec '16

I really ought to stop using my phone for email. Sent back to list. On Mon, Dec 19, 2016, at 05:25, Jeff Waugh wrote: > On Mon, Dec 19, 2016 at 8:19 PM, Corey Richardson > <corey(a)octayn.net> wrote: > > > I'm writing up my notes and will be publishing them on the > > Robigalia blog. > > Will send a link here when it's up. Ihor said he'd be collecting > > slides, > > not sure what the availability of those will be. > > > > Cool -- maybe let the list know too? -- cmr http://octayn.net/

1 0

RELEASE: Announcing CAmkES 2.3.0
by Stephen.Sherratt＠data61.csiro.au 15 Dec '16

15 Dec '16

Announcing the release of CAmkES 2.3.0 Changes in this release: * support for seL4 4.0.0 * new dependency: Haskell Stack (http://haskellstack.org) + Haskell Stack is a haskell version and package manager. It takes care of installing an appropriate version of ghc and cabal for building the capDL translator - part of CAmkES' build system. Check out an example CAmkES system with: repo init -u https://github.com/seL4/camkes-manifest.git -m default-2.3.x.xml repo sync For more information about CAmkES, see: https://wiki.sel4.systems/CAmkES Cheers, Stephen

1 0

ARM bootloaders that matter
by Jeff Waugh 14 Dec '16

14 Dec '16

Hi all, Out of interest, are there any ARM targets the seL4 development team / community care about that do not boot via u-boot or UEFI (whatever the implementation, be it u-boot, vendor-supplied, etc)? Thanks, Jeff

4 5

RELEASE: Announcing seL4 4.0.0
by Parthasarathi.Susarlaajay＠data61.csiro.au 13 Dec '16

13 Dec '16

We are pleased to announce the release of 4.0.0 of seL4. Listed below are a few of the key changes in this release: * Reorder bootinfo structure. * Add missing seL4_AllRights macro in libsel4. * Disallow kernel from using a device frame as an IPC buffer. * Syscall docs in manual now generated by doxygen. * Changes to make verification easier. * Various documentation fixes. * Benchmarks refactoring. * Coding style fixes. * Support for TLB and Cache management. * Preemptible backwards memzero for Retype. * Support for TCB operations in X86 multicore. * Support for raspberry-pi 3. ARM specific changes: * ARM Hyp refactoring. * Update VCPU fault definitions. * Add userspace invocations for hardware debugging. * Enable PMU export for V8. * Support ARM MPCore registers * Fix config dependency for 'IPC Buffer location'. * Use new cap rights structures in iospace. * Move initial setting of TPIDRURW register. * Add seL4_BenchmarkFlushCaches() for arm and ia32. * Support for prefetcher on Cortex-A9. * Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C. * am335x: Prevent out of bounds array access. * TK1 + Remove temporary SMMU memory mapping support. + Correct SMMU PD and PT indexing. + Split the mux controller from the misc region. * OMAP: + Fix issues with OMAP IRQ Code. X86 specific changes: * Add userspace invocations for hardware debugging. * Avoid writing the fs/gs base unless necessary. * Explicitly declare adress of .phys.bss. * Add BSS regions for BOOT and PHYS code. * Write FS and GS base when restoring user context. * Initialize store area when using XSAVE variant instructions. * Efficiently pack objects for fastpath. * Increase IPI words to 3. * Support for x2APIC. * Support larger XSAVE region sizes. * Change ia32 to use fs register for IPC buffer. * Update the bootinfo for number of cores. * Initial support for SMP vt-x. * Split CPU ID management into mode and general. * Fix cpuid family/model composition. * Add X86_64 support. Please note that this release is not source compatible with earlier releases of seL4, please read https://research.csiro.au/tsblog/introduc ing-device-untyped-memory-sel4/ for more information regarding the changes. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/4.0.0.tar.gz [259d9eadaddef579c2b98b91cf40d13a 4.0.0.tar.gz] The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf Contributors: * Adrian Danis * Alexander Boettcher * Amirreza Zarrabi * Anna Lyons * Christian Helmuth * Corey Richardson * Donny Yang * Hesham Almatary * Jeff Waugh * Joel Beeren * Kent McLeod * Kofi Doku Atuah * Matthew Brecknell * Matthew Fernandez * Matt Rice * Rafal Kolanski * Stephen Sherratt * Thomas Sewell * Xin,Gao Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla Kernel engineer DATA61 | CSIRO E parthasarathi.susarla(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2016