Hello,
we're are in progress of extending our Genode/seL4 support, namely
adding x86_64 and ARM support.
During this work I encountered on x86_64 some sporadically crashes of
the seL4 kernel. It happened during the debugging of our roottask on
seL4 in form of a page fault in the kernel ("KERNEL EXCEPTION") or a
static assertion in the kernel (see below).
>From my understanding, this shouldn't be possible based on your
verification work. Nevertheless, it happens reliable.
(To be fair, the roottask was in this scenario already a bit confused
and did things wrong - which however should never be enough to force the
kernel in an exception or assertion - I presume.)
I saved and stripped down the scenario which causes the kernel exception
with high reliably and hope you can re-produce it and find the root
cause. I stripped down the scenario to just the Genode image binary and
the steps we did to create the seL4 kernel from the vanilla sources.
Steps to reproduce:
qemu-system-x86_64 -no-kvm -serial stdio -m 512 -kernel sel4 -initrd
bomb_image.elf
The binaries of "bomb_image.elf" can be found at [1] and the kernel
"sel4" at [2].
The kernel is based on seL4 6.0 and a patch to pc99/autoconf.h (see
[0]). Beside that it is the vanilla 6.0 kernel:
https://github.com/seL4/seL4.git
git commit 8564ace4dfb622ec69e0f7d762ebfbc8552ec918
"update VERSION file to 6.0.0"
patch -p1 <~autoconfig.patch
BOARD=x86_64 ARCH=x86 SEL4_ARCH=x86_64 PLAT=pc99 DEBUG=1 make
objcopy -O elf32-i386 kernel.elf.strip sel4
(Qemu complains otherwise about 64bit elf for boot)
The final "sel4" binary can be used with the "bomb_image.elf" and qemu
as pointed out above.
I tried Qemu 2.5.0 as shipped with Ubuntu 16.04 LTS and Qemu 2.8.0
(self-compiled). On real hardware the scenario typically leads after a
while (kernel booted, roottask booted, scenario starts to run) to a
reboot (without the messages or assertion as in the Qemu case, see below).
The tool-chain for Genode is based on GNU GCC 6.3.0 (see [3] and [4]).
The kernel was either compiled with Genode's toolchain (6.3.0) or with
the standard GCC as provided by Ubuntu 16.04 LTS (GCC 5.4.0).
On x86_32 I could not reproduce the issue. (On ARM I did not try.)
I hope the information are helpful - if you need more just ask.
Cheers,
Alex.
========== KERNEL EXCEPTION ==========
Vector: 0xe
ErrCode: 0x0
IP: 0xffffffff80720e60
SP: 0xffffffff80740e08
FLAGS: 0x6
CR0: 0x8000003b
CR2: 0x3007065 (page-fault address)
CR3: 0x1ffb000 (page-directory physical address)
CR4: 0x220
Stack Dump:
*0xffffffff80740e08 == 0xffffff8001a99b00
*0xffffffff80740e10 == 0xffffffff80729b1f
*0xffffffff80740e18 == 0x1
*0xffffffff80740e20 == 0xffffffff80721c59
*0xffffffff80740e28 == 0xffffffff
*0xffffffff80740e30 == 0x0
*0xffffffff80740e38 == 0xffffff801f02b740
*0xffffffff80740e40 == 0xffffff801f02b740
*0xffffffff80740e48 == 0x1
*0xffffffff80740e50 == 0xffffff8001a99000
*0xffffffff80740e58 == 0x7
*0xffffffff80740e60 == 0x59
*0xffffffff80740e68 == 0xffffff8001a99b00
*0xffffffff80740e70 == 0xffffffff80729cf3
*0xffffffff80740e78 == 0x9000000000000007
*0xffffffff80740e80 == 0xffffff8001a99059
*0xffffffff80740e88 == 0xffffff80ffffffff
*0xffffffff80740e90 == 0xffffffff80740f18
*0xffffffff80740e98 == 0xffffff800013c200
*0xffffffff80740ea0 == 0x10000
Halting...
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 10, Invocation tag: 16
or
seL4 failed assertion
'(cte_t*)mdb_node_get_mdbNext(destSlot->cteMDBNode) == NULL &&
(cte_t*)mdb_node_get_mdbPrev(destSlot->cteMDBNode) == NULL' at
src/object/cnode.c:457 in function cteInsert
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 10, Invocation tag: 18
or a fault by the roottask (and not in the kernel). So - this is no
issue for the kernel:
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x18 with status 0x4
in thread 0xffffff800013c200 "child of: 'rootserver'" at address 0x20419cf
[0]
https://github.com/alex-ab/genode/blob/crash_sel4_kernel_vanilla/autoconfig…
[1]
https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.…
[2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4
[3] https://genode.org/download/tool-chain
[4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.05/
--
Alexander Boettcher
Genode Labs
http://www.genode-labs.com - http://www.genode.org
Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
Hello to All,
I am trying to do some message passing between a vm component and a camkes
component.
I have tried by enabling the Vchan option on the build system and compiling
the helloworld linux user level program on a tk1. I received an error about
the /dev/vmm_manager not being able to open. What is the proper method of
setting up the Vchan communication for camkes-arm-vmm on a tk1?
Thank You
Dear,
I used "qemu-system-i386 -m 1024 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99"
It showed "Booting from ROM"
Thanks, Sincerely
------------------ Original ------------------
From: "devel-request";<devel-request(a)sel4.systems>;
Date: Thu, Aug 24, 2017 10:00 AM
To: "devel"<devel(a)sel4.systems>;
Subject: Devel Digest, Vol 39, Issue 26
Send Devel mailing list submissions to
devel(a)sel4.systems
To subscribe or unsubscribe via the World Wide Web, visit
https://sel4.systems/lists/listinfo/devel
or, via email, send a message with subject or body 'help' to
devel-request(a)sel4.systems
You can reach the person managing the list at
devel-owner(a)sel4.systems
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Devel digest..."
Today's Topics:
1. Re: about camkesvm (Kofidoku.Atuah(a)data61.csiro.au)
----------------------------------------------------------------------
Message: 1
Date: Thu, 24 Aug 2017 00:00:19 +0000
From: <Kofidoku.Atuah(a)data61.csiro.au>
To: <devel(a)sel4.systems>
Subject: Re: [seL4] about camkesvm
Message-ID: <1503532819201.94096(a)data61.csiro.au>
Content-Type: text/plain; charset="iso-8859-1"
Hey Talos,
Sorry we didn't make this clearer on that page: those defconfigs build an x86-pc image; not an ARM image. Could you try running Qemu again, but with something similar to,
qemu-system-i386 -m <WHATEVER_RAM_SIZE_YOU_WANT> -kernel <SEL4_KERNEL_IMAGE> -initrd <CAPDL_INITRD_IMAGE>
And tell me what happens? Sorry for the inconvenience.
--
Kofi Doku Atuah
Kernel engineer
DATA61 | CSIRO
________________________________
From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com>
Sent: 22 August 2017 15:39
To: devel
Subject: [seL4] about camkesvm
Hi
I started the tutorial following the link:
https://wiki.sel4.systems/CAmkESVM
I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig
then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99
but the error is
Segmentation fault (core dumped)
what's wrong? Thanks
Sincerely
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://sel4.systems/pipermail/devel/attachments/20170824/cd4992b3/attachmen…>
------------------------------
Subject: Digest Footer
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
------------------------------
End of Devel Digest, Vol 39, Issue 26
*************************************
Hi
I started the tutorial following the link:
https://wiki.sel4.systems/CAmkESVM
I used "make minimal_defconfig" substituting "make cma34cr_minimal_defconfig" for int the directory config there is minimal_defconfig
then make and qemu-system-arm -M kzm -nographic -kernel images/capdl-loader-experimental-image-ia32-pc99
but the error is
Segmentation fault (core dumped)
what's wrong? Thanks
Sincerely
Has anyone had issues with serial when running the test suite on a
Raspberry Pi 3b?
Currently I am following the blog post:
https://research.csiro.au/tsblog/sel4-raspberry-pi-3/
In the seL4test project I have successfully compiled
sel4test-driver-image-arm-bcm2837 from rpi3_debug_xml_defconfig. Along
with this I have the following files: bootcode.bin, start.elf,
u-boot.bin, and config.txt.
Bootcode.bin and start.elf are from the current Raspian firmware.
Config.txt just contains a line to enable UART ("enable_uart=1") and one
to point and u-boot.bin ("kernel=u-boot.bin"). And per the comment
section of the seL4 post I downgraded the version of u-boot to before
March 2017 (currently using Jan 2017).
I am not deviating from the blog posting but I am experiencing an issue
not mentioned. I have no serial output (I do have a u-boot terminal
prompt through HDMI, so I can load/boot the binary). When I boot seL4 I
receive the misaligned cache messages (through HDMI) and then it hangs.
Without serial I have no eyes to see if the seL4 tests are running.
Other than wiring into the RPI3 UART (GND/TX/RX on pins 6/8/10) and
enabling UART in config.txt is there another step I'm missing?
Thanks for any direction you can point me in,
Steve
Hi seL4,
I see below link to know VMM support SMP at Q3’17.
I want to know does it ready and has any restriction? Thank you.
https://sel4.systems/Info/Roadmap/
Low-level Userland
Status
Date
Feature
Location
deferred to
Q3’17
SMP-capable virtual-machine monitor (VMM)
master
Joyce.Peng (彭美僑)
Thanks for the information. Looking at eChronos now.
>
> ---------- Forwarded message ----------
> From: <Ihor.Kuz(a)data61.csiro.au>
> To: <devel(a)sel4.systems>
> Cc:
> Bcc:
> Date: Sun, 20 Aug 2017 23:57:34 +0000
> Subject: Re: [seL4] mpu vs mmu
>
> > On 21 Aug 2017, at 8:05 am, Gernot.Heiser(a)data61.csiro.au wrote:
> >
> > On 21 Aug 2017, at 03:00, Thomas Dundon <dundon.thomas(a)gmail.com> wrote:
> >>
> >> Does an MPU, e.g. on a Cortex M3, provide enough functionality to
> support seL4?
> >
> > No, it doesn’t. The seL4 model is fundamentally based on the ability to
> virtualise hardware resources.
> >
> > If you don’t have that, then you can’t dod much more than a
> memory-protected RTOS. If you’re after an RTOS with a (not yet complete)
> verification story, look at eChronos: https://ts.data61.csiro.au/
> projects/TS/echronos/
> >
>
> In particular we have some work in the pipeline that adds (ARM
> Cortex-M3/4) MPU support to eChronos (it’s currently in the process of
> being code-reviewed and will be released after that).
>
> Ihor.
>
>
>
> _______________________________________________
> Devel mailing list
> Devel(a)sel4.systems
> https://sel4.systems/lists/listinfo/devel
>
>
Has anyone had luck running the seL4test suite with an i.MX7 processor?
I acquired a Toradex Colibri board
(https://www.toradex.com/computer-on-modules/colibri-arm-family/nxp-freescal…)
and am testing it out.
Using the docker environment when I brew a seL4test config file either
by hand or through menuconfig results in a 'libplatsupport' failure.
There is platform support for the i.MX7 in the kernel source and
imx7/armv7-a/cortex-a7 options in the seL4 git Makefile. Using the
following make options results in another failure on multiple #error
defines:
"TOOLPREFIX=arm-none-eabi- ARCH=arm PLAT=imx7 ARMV=armv7-a CPU=cortex-a7
make"
Thanks for any help or direction you can point me in,
Steve
