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 …
[View More]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
[View Less]
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:
> >>
> >> …
[View More]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
>
>
[View Less]
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 …
[View More]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
[View Less]
Hello Kent,
I extended the rumprun+rust example (available in this PR
<https://github.com/seL4/camkes/pull/4>) with a simple camkes connection
between the rumprum camkes component and a serial server component, as
shown below (full code here
<https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/r…>
):
* composition {*
* component rumprun_platform_layer rrpl;*
* component rumprun_rust hello1;*
* RUMPRUN_META_CONNECTION(hello1, rrpl)*
* …
[View More]component rumprun hello2;*
* RUMPRUN_META_CONNECTION(hello2, rrpl)*
* component Server server;*
* connection seL4SharedData conn(from hello1.camkes_buffer, to
server.buffer);*
* connection seL4Notification simpleEvent1(from hello1.camkes_ev, to
server.ev);*
* connection seL4Notification simpleEvent2(from server.ev1, to
hello1.camkes_ev1);*
* }*
I added a simple rust program
<https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…>
(running on rumprun_rust):
*fn main() {*
* println!("Hello rust!");*
* unsafe {*
* camkes_ev_emit();*
* }*
* println!("Waiting for event!");*
* unsafe {*
* camkes_ev1_wait();*
* }*
* println!("Got event!");*
*}*
*#[no_mangle]*
*extern {*
* fn camkes_ev_emit();*
* fn camkes_ev1_wait(); *
*}*
In order to compile the cargo project, I added a build.rs script
<https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_rust/c…>
to package the generated camkes object file (camkes.o) into an archite that
cargo can link against.
The problem is, that the generated camkes.c file contains its own main
function:
*int USED main(int argc UNUSED, char *argv[]) {*
* assert(argc == 2);*
* assert(strcmp(argv[0], "camkes") == 0);*
* int thread_id = (int)(uintptr_t)(argv[1]);*
* return post_main(thread_id);*
*}*
which collides with the *fn main()* defined in rust. (I get *multiple
definition of `main'* error).
How is this handled in rumprun_ethernet
<https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…>
example? There is also a main function for the rumpkernel component
<https://github.com/GaloisInc/camkes/blob/devel_rust_app/apps/rumprun_ethern…>,
and the main() from camkes, but the compilation process handles this
correctly.
Could you point me in the right direction?
Regards
Michal
[View Less]
Hi,
Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel?
I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below:
[ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000)
[ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004
[ 10.761443]
[ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.…
[View More]0-rc5-00024-gec4c02c-dirty #122
[ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree)
[ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14)
[ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220)
[ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4)
[ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0)
[ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754)
[ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c)
[ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4)
[ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20)
[ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004
Is this a problem that current VMM does not support FPU? or other reasons caused the problem？
[View Less]
Hello all, mostly Kent,
I read your blog post about rumpkernels on sel4:
https://research.csiro.au/tsblog/using-rump-kernels-to-run-unmodified-netbs…
and after experimenting with the rumprun apps (such as the ethernet one
<https://github.com/seL4/camkes/tree/master/apps/rumprun_ethernet>) I think
it is a great addition to sel4.
So I have few questions. I need to run two different rumpkernels, each with
its own address space, connected only through dataports/events.
1- does the current …
[View More]rumpkernel backend support having this separation?
According to your thesis
<http://www.disy.cse.unsw.edu.au/theses_public/16/kentm.pdf>, all
rumpkernel threads run in a single sel4 thread - is that correct?
2- Right now, I can combine multiple rumprun components in one application
(lets say *runmprun_hello* and *rumprun_pthreads*). butI can have only one
rumprun_platform_layer per application, correct? An example below:
*assembly {*
* composition {*
* component rumprun_platform_layer rrpl;*
* component rumprun hello;*
* RUMPRUN_META_CONNECTION(hello, rrpl)*
* component rumprun_pthreads pthreads;*
* RUMPRUN_META_CONNECTION(pthreads, rrpl)*
* }*
* configuration {*
* hello.rump_config = {"cmdline": "hello World!" };*
* RUMPRUN_COMPONENT_CONFIGURATION(hello, 0)*
* pthreads.rump_config = {"cmdline": "./pthreads_test 4" };*
* RUMPRUN_COMPONENT_CONFIGURATION(pthreads, 1)*
* }*
*}*
If I instantiate another *rumprun_platform* component, it wont compile.
3 - how can I go around defining/adding my own rumpkernels? Lets say I want
to build a rumpkernel with rust support
<https://github.com/rumpkernel/rumprun-packages/tree/master/rust> (you have
an sel4 example here
<https://github.com/SEL4PROJ/rumprun-sel4-demoapps/tree/master/userapps/rust>)
and integrate it with the rumprun_hello
<https://github.com/seL4/camkes/blob/master/apps/rumprun_hello/rumprun_hello…>
app.
Regards
Michal
[View Less]
