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-…
[View More]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
[View Less]
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 -…
[View More]- maybe let the list know too?
--
cmr
http://octayn.net/
[View Less]
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 …
[View More]information about CAmkES, see: https://wiki.sel4.systems/CAmkES
Cheers,
Stephen
[View Less]
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 …
[View More]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
[View Less]
Hello,
We are looking to add another virtio device to camkes-vm for guests to use. I have been looking through the code at how virtio_net works and I have a pretty decent understanding of how it is configured and used. I have a few design/philosophical questions though.
1. Was any of this (libethdriver, libpci, Ethdriver component, virtio_net.c, virtio_emul.c) ported from somewhere else, or was it all written from scratch?
2. Why is components/Init/src/virtio_net.c used in …
[View More]conjunction with vm0_config.init_cons instead of just using the VMNet templates?
3. Looks like pci handling was decoupled from drivers like libethdriver and it is left up to the VM Init component to configure PCI. What is the reason for that?
4. Virtio_emul.c appears to be the layer that actually provides the virtio interface to the VM. Would it make more sense to make this more generic to cover more devices, or should new emulation files be created for each device?
Thanks,
Robbie VanVossen
[View Less]
Hurrah,
I was curious about the huge kernel images, and had it on my list to poke
at. Adrian's changes merged last night sorted it:
x86: Explicitly declare adress of .phys.bss
x86: Add BSS regions for BOOT and PHYS code
Simulation debug x86_64 image is down from 7.1M to 1.1M. That's more like
it!
Nice! :-)
Thanks,
Jeff
Hi all,
I recently acquired a BD-SL-I.MX6 and will be tinkering with it to install seL4. A major use case for me is if I could run [bitcoind](https://en.bitcoin.it/wiki/Bitcoind) or at least [vanitygen](https://en.bitcoin.it/wiki/Vanitygen) on seL4. I'm very new to the system, but is there a relatively easy way of cross-compiling said software for seL4? Would love to spend some time learning.
Cheers,
Carl Dong
accounts(a)carldong.me
