Devel December 2016

devel@sel4.systems

18 participants
14 discussions

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

seL4 on Zinq7000 on QEMU
by Andrew Gacek 09 Dec '16

09 Dec '16

I'm trying to build and emulate a version of seL4 for the zinq7000 platform, but it crashes immediately. I've started by taking the camkes tutorial and building it for zinq7000: repo init -u https://github.com/seL4/camkes-manifest.git repo sync make arm_simple_defconfig make menuconfig # change seL4 platform to zinq7000 make When I try to emulate it, it crashes right away: qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel images/capdl-loader-experimental-image-arm-zynq7000 qemu: fatal: Trying to execute code outside RAM or ROM at 0x10000000 R00=00000000 R01=00000000 R02=00000000 R03=00000000 R04=00000000 R05=00000000 R06=00000000 R07=00000000 R08=00000000 R09=00000000 R10=00000000 R11=00000000 R12=00000000 R13=00000000 R14=00000000 R15=10000000 PSR=400001d3 -Z-- A svc32 s00=00000000 s01=00000000 d00=0000000000000000 s02=00000000 s03=00000000 d01=0000000000000000 s04=00000000 s05=00000000 d02=0000000000000000 s06=00000000 s07=00000000 d03=0000000000000000 s08=00000000 s09=00000000 d04=0000000000000000 s10=00000000 s11=00000000 d05=0000000000000000 s12=00000000 s13=00000000 d06=0000000000000000 s14=00000000 s15=00000000 d07=0000000000000000 s16=00000000 s17=00000000 d08=0000000000000000 s18=00000000 s19=00000000 d09=0000000000000000 s20=00000000 s21=00000000 d10=0000000000000000 s22=00000000 s23=00000000 d11=0000000000000000 s24=00000000 s25=00000000 d12=0000000000000000 s26=00000000 s27=00000000 d13=0000000000000000 s28=00000000 s29=00000000 d14=0000000000000000 s30=00000000 s31=00000000 d15=0000000000000000 s32=00000000 s33=00000000 d16=0000000000000000 s34=00000000 s35=00000000 d17=0000000000000000 s36=00000000 s37=00000000 d18=0000000000000000 s38=00000000 s39=00000000 d19=0000000000000000 s40=00000000 s41=00000000 d20=0000000000000000 s42=00000000 s43=00000000 d21=0000000000000000 s44=00000000 s45=00000000 d22=0000000000000000 s46=00000000 s47=00000000 d23=0000000000000000 s48=00000000 s49=00000000 d24=0000000000000000 s50=00000000 s51=00000000 d25=0000000000000000 s52=00000000 s53=00000000 d26=0000000000000000 s54=00000000 s55=00000000 d27=0000000000000000 s56=00000000 s57=00000000 d28=0000000000000000 s58=00000000 s59=00000000 d29=0000000000000000 s60=00000000 s61=00000000 d30=0000000000000000 s62=00000000 s63=00000000 d31=0000000000000000 FPSCR: 00000000 Aborted Is there something I'm doing wrong? Thanks, Andrew

2 9

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2016