December 2016 - Devel - lists.sel4.systems

seL4 test on x86
by Yevgeny Lavrov 29 Jan '25

29 Jan '25

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

4 3

Questions about Memory Management in seL4
by Daniel Wang 18 May '23

18 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 29 Jan '17

29 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 05 Jan '17

05 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 04 Jan '17

04 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 02 Jan '17

02 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 19 Dec '16

19 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 14 Dec '16

14 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 13 Dec '16

13 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