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
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)*
* 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
