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/
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
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
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
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
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/
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
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
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
