Hello all,
I am running camkes-vm on x86 architecture, following the example on wiki
https://wiki.sel4.systems/CAmkESVM#Cross_VM_Connectors with the exception
that I want to invoke the stringReverse component
<https://github.com/podhrmic/camkes-vm/tree/master/components/StringReverse>
.
I am running the optiplex9020_defconfig example with only one VM, and when
I start booting the guest linux system, I see the following error:
*[ 1.282326] dataport: loading out-of-tree module taints kernel.*
*[ 1.290615] dataport: module license 'unspecified' taints kernel.*
*[ 1.306854] Disabling lock debugging due to kernel taint*
*[ 1.319664] dataport initialized with major number 247*
*vmm_vmcall_handler:55 | Failed to find handler for token:2*
*[ 1.325411] incorrect event context magic number (expected 42, got
-677408512)insmod: can't insert
'/lib/modules/4.8.16/kernel/drivers/vmm/consumes_event.ko': Operation not
ermitted*
*[ 1.337441] emits_event initialized with major number 245*
*[ 1.356391] k_vmm_manager: failed on sel4 hypervisor connection |-1|*
Then when I log into linux and call `string_reverse
<https://github.com/podhrmic/camkes-vm/tree/master/linux/pkg/string_reverse>`
program, I get the following error:
*# string_reverse *
*[ 8.360164] BUG: unable to handle kernel paging request at d881f2c0*
*[ 8.360164] IP: [<d00a69f0>] chrdev_open+0xab/0x100*
*[ 8.360164] *pde = 17867067 *pte = 00000000 *
*[ 8.360164] Oops: 0000 [#1]*
*[ 8.360164] Modules linked in: emits_event(PO) dataport(PO)*
*[ 8.360164] CPU: 0 PID: 691 Comm: string_reverse Tainted: P O
4.8.16 #1*
*[ 8.360164] task: d79c9740 task.stack: d6ae0000*
*[ 8.360164] EIP: 0060:[<d00a69f0>] EFLAGS: 00010286 CPU: 0*
*[ 8.360164] EIP is at chrdev_open+0xab/0x100*
*[ 8.360164] EAX: d881f2c0 EBX: 00000000 ECX: d79b0d00 EDX: 00000000*
*[ 8.360164] ESI: d79b0d00 EDI: d6add808 EBP: d6ae1e10 ESP: d6ae1df8*
*[ 8.360164] DS: 007b ES: 007b FS: 0000 GS: 0033 SS: 0068*
*[ 8.360164] CR0: 80050033 CR2: d881f2c0 CR3: 16ad9000 CR4: 00102690*
*[ 8.360164] DR0: 00000000 DR1: 00000000 DR2: 00000000 DR3: 00000000*
*[ 8.360164] DR6: fffe0ff0 DR7: 00000400*
*[ 8.360164] Stack:*
*[ 8.360164] d7ac9be0 d7ac9be0 00000001 d7ac9be0 d6add808 00000000
d6ae1e30 d00a2370*
*[ 8.360164] d6ae1e28 d7ac9be8 d00a6945 d7ac9be0 d69db010 d7462d80
d6ae1e4c d00a2cf8*
*[ 8.360164] d79c2b80 d79c2b80 00000000 d6ae1ebc d7462d80 d6ae1eb0
d00ae159 d6ae1e64*
*[ 8.360164] Call Trace:*
*[ 8.360164] [<d00a2370>] do_dentry_open+0x197/0x216*
*[ 8.360164] [<d00a6945>] ? cdev_put+0x1a/0x1a*
*[ 8.360164] [<d00a2cf8>] vfs_open+0x45/0x4e*
*[ 8.360164] [<d00ae159>] path_openat+0x822/0x970*
*[ 8.360164] [<d007a468>] ? __alloc_pages_nodemask+0x11c/0x770*
*[ 8.360164] [<d00ae2d8>] do_filp_open+0x31/0x77*
*[ 8.360164] [<d00b6293>] ? __alloc_fd+0xbb/0xfe*
*[ 8.360164] [<d00a2e56>] do_sys_open+0x54/0xc7*
*[ 8.360164] [<d00a2ee1>] SyS_open+0x18/0x1a*
*[ 8.360164] [<d0000ee1>] do_fast_syscall_32+0x7a/0xb8*
*[ 8.360164] [<d047831f>] sysenter_past_esp+0x40/0x6a*
*[ 8.360164] Code: 11 89 f0 e8 e1 fa ff ff 83 f8 01 19 db 31 d2 83 e3 fa
89 d0 e8 4d ff ff ff 85 db 75 59 8b 46 28 85 c0 75 0c*
*[ 8.360164] EIP: [<d00a69f0>] chrdev_open+0xab/0x100 SS:ESP
0068:d6ae1df8*
*[ 8.360164] CR2: 00000000d881f2c0*
*[ 8.360164] ---[ end trace 46873a57a343e435 ]---*
*[ 8.376285] string_reverse (691) used greatest stack depth: 6496 bytes
left*
*Killed*
which seems like the program is trying to access memory that it is not
supposed to.
If I follow the example from wiki (here https://wiki.sel4.
systems/CAmkESVM#Cross_VM_Connectors ) I get the same error, but triggered
by `print_client` program.
Have you seen a problem like this before? How do I correctly load the
kernel module?
Regards
Michal
I have seL4 running on a TK1 using linux-tk1-initrd. I'd like to get
the linux-tk1-debian version running to load the userspace off of the
emmc drive of the TK1. FWIW, I did flash the TK1 to the latest
verison, R21.5.
The default DTS has root=/dev/mmcblk0p2 in the bootargs. When booting
with this, I get a kernel panic. I also tried changing that to
root=/dev/mmcblk0p1 (since that partition was the larger one on the
emmc). It also gives a kernel panic, albeit a different message.
With mmcblk0p1, the message I get is:
[ 10.092841] EXT2-fs (mmcblk0p1): error: couldn't mount because of
unsupported optional features (240)
[ 10.102749] EXT4-fs (mmcblk0p1): couldn't mount as ext3 due to
feature incompatibilities
[ 10.137427] EXT4-fs (mmcblk0p1): mounted filesystem with ordered
data mode. Opts: (null)
[ 10.145696] VFS: Mounted root (ext4 filesystem) on device 179:1.
[ 10.162679] devtmpfs: mounted
[ 10.165845] Freeing unused kernel memory: 252K (c0aa9000 - c0ae8000)
[ 10.224352] Kernel panic - not syncing: Attempted to kill init!
exitcode=0x00000004
[ 10.224352]
[ 10.233480] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5 #1
[ 10.240429] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree)
[ 10.246713] [<c0015d30>] (unwind_backtrace) from [<c0012b74>]
(show_stack+0x10/0x14)
[ 10.254457] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214)
[ 10.261330] [<c009247c>] (panic) from [<c002566c>]
(complete_and_exit+0x0/0x1c)
[ 10.268627] [<c002566c>] (complete_and_exit) from [<00000000>] ( (null))
[ 10.275408] ---[ end Kernel panic - not syncing: Attempted to kill
init! exitcode=0x00000004
With mmcblk0p2, the message I get is:
[ 10.095124] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0x1000000)
[ 10.102907] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 1th superblock
[ 10.111127] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0xfb000000)
[ 10.118994] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 2th superblock
[ 10.126711] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0x1000000)
[ 10.134472] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 1th superblock
[ 10.142167] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0xfb000000)
[ 10.149983] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 2th superblock
[ 10.159891] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0x1000000)
[ 10.167669] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 1th superblock
[ 10.175842] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0xfb000000)
[ 10.183743] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 2th superblock
[ 10.191391] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0x1000000)
[ 10.199146] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 1th superblock
[ 10.206813] F2FS-fs (mmcblk0p2): Magic Mismatch, valid(0xf2f52010)
- read(0xfb000000)
[ 10.214653] F2FS-fs (mmcblk0p2): Can't find valid F2FS filesystem
in 2th superblock
[ 10.222551] Kernel panic - not syncing: VFS: Unable to mount root
fs on unknown-block(179,2)
[ 10.230976] CPU: 0 PID: 1 Comm: swapper Tainted: G W
4.3.0-rc5 #1
[ 10.238184] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree)
[ 10.244462] [<c0015d30>] (unwind_backtrace) from [<c0012b74>]
(show_stack+0x10/0x14)
[ 10.252205] [<c0012b74>] (show_stack) from [<c009247c>] (panic+0xa0/0x214)
[ 10.259079] [<c009247c>] (panic) from [<c0aaa238>]
(mount_block_root+0x21c/0x230)
[ 10.266554] [<c0aaa238>] (mount_block_root) from [<c0aaa368>]
(mount_root+0x11c/0x124)
[ 10.274459] [<c0aaa368>] (mount_root) from [<c0aaa4bc>]
(prepare_namespace+0x14c/0x194)
[ 10.282451] [<c0aaa4bc>] (prepare_namespace) from [<c0aa9dec>]
(kernel_init_freeable+0x1c0/0x1d0)
[ 10.291315] [<c0aa9dec>] (kernel_init_freeable) from [<c07c4b20>]
(kernel_init+0x8/0xe8)
[ 10.299397] [<c07c4b20>] (kernel_init) from [<c000f4d8>]
(ret_from_fork+0x14/0x3c)
[ 10.306959] ---[ end Kernel panic - not syncing: VFS: Unable to
mount root fs on unknown-block(179,2)
Is there a guide for how to setup the emmc on the TK1 to boot using
linux-tk1-debian?
Will an older version of the TK1 image from Nvidia work or do I need
to do a custom debian install (like this
https://wiki.debian.org/InstallingDebianOn/NVIDIA/Jetson-TK1)?
Hi,
I’m tracing the path where sel4 kernel jumps to an application, such as
hello-1.
>From the Makefile for apps I know that the entry of the hello-1.bin is
*_sel4_start* which is defined in the sel4_crt0.S (the directory is
sel4_tutorials/projects/sel4_libs_libsel4platsupport/src/arch/arm). The
*_sel4_start* function first calls a C function called *sel4_InitBootInfo*,
and finally jumps to the *_start* function which is defined in the crt0.S.
However the *_start* in crt0.S calls the sel4_InitBootInfo again. What
confuses me is that the sel4_InitBootInfo function requires an input
argument passed by R0, however the R0 has been set to zero in the
_sel4_start function, so I think the calling of sel4_InitBootInfo in the
_start will not run correctly.
Or is the path where the kernel jumps to the app
(_sel4_start->_start->main) wrong?
I paste referred codes below:
*/******sel4_crt0.S********************/*
_sel4_start:
/* Setup a stack for ourselves. */
ldr sp, =_stack_top
/* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'. */
bl seL4_InitBootInfo
............
mov r0, #0 // *The R0 is modified, so it doesn't store the bootinfo
structure anymore!*
............
/* Now go to actual _start */
ldr pc, =_start
*/*********crt0.S********************/*
_start:
/* Setup a stack for ourselves. */
ldr sp, =_stack_top
*/* Setup bootinfo. The pointer to the bootinfo struct starts in 'r0'.
*/*
* bl seL4_InitBootInfo //Since R0 has been modified by _sel4_start,
sel4_InitBootInfo will not run correctly.*
/* Call constructors and other initialisation functions. */
bl _init
/* Call main. */
bl main
b exit
Best Regards,
Shijun Zhao
I expect this might be (or even probably is) a bad place to ask this but at
the same time I didn't find any better coming from the Contact Information
page (http://sel4.systems/contact/).
I'm working on a conference paper (not sure if I will make it but still
trying to - code::dive <http://codedive.pl/> if anyone would be interested)
about proving program correctness. Considering my own knowledge in the field
and expected knowledge of the audience there would be nothing new in that
paper - more like an update on what is the current state of the field. Yet I
wanted to supply also some examples.
As main example I would like to show proof (or at least parts of it) of
correctness (adherence to specification) of C++ code, possibly reduced to C
code if need be. After research in this topic and finding this project some
time ago it felt natural to reuse its tools. But I fail to do so. Could you
possibly guide me? Using your tools and techniques what should I do to prove
correctness of some piece of code. I think source code level would be more
than enough - for this task no need to verify binary in any form.
As a side example I would like to show how your proves look like. I'm not
sure what you are generating / writing as a proof (that gets later verified
automatically). I imagine a sequence of something. Some formulas in natural
deduction perhaps? Or something else? Whatever that would be I guess it must
be pretty long so it is not like I would show and analyze it all but instead
would like to somehow let the audience "feel the size".
If - as I expect - this is not the right place to ask and you cannot help me
with above questions, could you at least point me to where to ask them?
Adam Badura
Hi All,
I am playing around with the capabilities of the camkes-arm-vm project
pn the Tegra TK1 and and wondering if someone else has come across this
issue. It looks like GPIO functionality is not available in the buildroot.
I can confirm the GPIO source is present and is being built:
camkes-arm-vm/libs/libplatsupport/rc/plat/tk1/gpio.c
camkes-arm-vm/libs/libplatsupport/plat_include/tk1/platsupport/plat/gpio.h
[CC] src/plat/tk1/gpio.o
The expected sysfs support is not present and looking and the relevant
dmesg:
# dmesg | grep gpio
[ 0.057543] gpiochip_add: GPIOs 0..255 (tegra-gpio) failed to register
[ 1.485061] input: gpio-keys as /devices/soc0/gpio-keys/input/input0
Any thoughts on what could be causing GPIO to the failing to register?
Steven
Hi seL4-hackers,
I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core.
The porting work is based on NVidia TK1 Cortex-A15 platform.
In current stage, the seL4 kernel has booted up and the test benches can be tested.
I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER).
In my target, only ARM generic timer is used.
My questions are:
1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer?
If I only use ARM generic timer, should these timer tests be passed?
2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific.
If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer?
If yes, is there any example for me to reference?
BRs,
Jesse
Hello All,
Has anyone come across this error before?
[GEN] imx6_net.cdl
While forming CapDL spec: failed to find dataport symbol 'camkes router router_send_buf data' in ELF router_group_bin
make[1]: *** [imx6_net.cdl] Error 255
make[1]: *** Deleting file `imx6_net.cdl'
make: *** [imx6_net] Error 2
Thanks,
Chris Guikema
Hello all,
We have published a blog post about how we manage software dependencies
within Trustworthy Systems, and how it has been adapted to produce a
relatively user-friendly interface.
It is relevant for people both new and old to the seL4 ecosystem, as it
simplifies and compartmentalises the elaborate software dependencies
sometimes required to get things to build.
You can read the blog post here:
https://research.csiro.au/tsblog/getting-started-sel4-camkes-l4v-dependenci…
If you have any feedback or changes you would like made, please let us
know on the GitHub repo.
Cheers,
Luke
--
Luke Mondy, Systems Administrator, Trustworthy Systems
DATA61 | CSIRO
M +61 0415 281 991 | https://ts.data61.csiro.au
Hi Everyone,
Is there has any seL4 project support ARM Cortex-A7 ?
I found seL4 official projects in below link.
https://github.com/seL4https://github.com/SEL4PROJ
I use sel4test project that repo from https://github.com/seL4/sel4test-manifest.git
And I found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like below.
File: sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconfig
#
# seL4 System
#
# CONFIG_ARCH_X86 is not set
CONFIG_ARCH_ARM=y
CONFIG_ARCH_AARCH32=y
# CONFIG_ARM1136JF_S is not set
# CONFIG_ARM_CORTEX_A8 is not set
CONFIG_ARM_CORTEX_A9=y
# CONFIG_ARM_CORTEX_A15 is not set
# CONFIG_PLAT_EXYNOS54XX is not set
I can’t find seL4 project support ARM cortex-A7. Does anyone find it?
Thanks,
Joyce Peng