A friendly reminder that the seL4 developer hangout is on again next week:
Tue, Nov 1, 9pm (UTC), Topics: (open)
* Sydney: Wed, Nov 2, 8am
* Central Europe: Tue, Nov 1, 10pm
* US Pacific Time: Tue, Nov 1, 2pm
Zoom link: https://unsw.zoom.us/j/82640784431
Dr. Birgit Brecknell
Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:email@example.com>
seL4 Foundation, birgit(a)sel4.systems<mailto:firstname.lastname@example.org>
0433 880 571
I came across Gernot Heiser's blog post on "How to use seL4 IPC" . The
article explicitly says that doing cross-core IPC is a bad idea. This
statement led to a series of questions for me, which I hope you guys can
help me with.
We have a system with two cores. Let's say that a physical memory server is
running on core0, my application is on core1, and they are somehow pinned
to those cores. The application wants some physical memory (frame
capabilities) from the memory server.
Q1. Will the application be able to invoke the endpoint given that the TCB
which will respond to it is on a separate core? If yes, will sending a
capability back via cross-core IPC be allowed? I did not read anything in
the manual which said otherwise.
Q2. Why is a cross-core IPC a bad idea? This might be a loaded question,
but I am not able to appreciate the badness of the idea :)
Q3. What would be the right way to do it? For example, in
Barrelfish(limited experience from a course), the application(on core1)
would make an IPC to a monitor running on the same core1. This monitor did
synchronization with another monitor running on the other core(core0) via a
shared memory region (all in user space). That monitor(core0) then sent an
IPC to the memory server running on core0. And then back again via the
Hi Sel4 developers,
I am new to this forum and hoping this is the right place to bounce my
project idea off. I typically use FPGA to enforce security in my products
but there are lots of reasons why FPGAs are not suitable for all use cases.
I have also used low end microcontroller where one can review all the code
to understand the security risks.
My latest project however involves two USB processes (one for each physical
connection) with high throughput expectations. And to pass data streams at
high typical throughput between them. Due to the wide range of USB type of
devices I fear this would be too much code to review - it feels very OS
like. Note, I don't need a GUI, it's headless.
So I'm interested in sel4 as I could run the processes in Linux VMs if I
understand sel4 correctly. And whilst it's not the smallest processors I
think they need to be more powerful to support the speeds. So this is fine
. I am unsure how much of this project is already done, mainly thinking the
usb driver perspective.
Thanks in advance,
I was interested to see the Google news re. KataOS which I suspect confirms
that my sort of requirement / entry point is someway out.
I was also reading about ARM Morello / CHERI work. Although I appreciate
this is taking a different, perhaps flawed, path of some new hardware
Appreciate any feedback you can humour me with.
A friendly reminder that the seL4 developer hangout is on again this week:
Wed, Oct 19, 6am (UTC), Topics: (open)
* Sydney: Wed, Oct 19, 5pm
* Central Europe: Wed, Oct 19, 8am
* US Pacific Time: Tue, Oct 18, 11pm
Zoom link: https://unsw.zoom.us/j/82640784431
> From: Gerwin Klein <kleing(a)unsw.edu.au>
> Subject: [seL4] new RFC: seL4 Device Driver Framework
> To: sel4 <devel(a)sel4.systems>
> Cc: "tsc-members(a)sel4.systems" <tsc-members(a)sel4.systems>
> Message-ID: <55BB3266-24A1-488B-A623-5B912461AD7F(a)unsw.edu.au>
> Content-Type: text/plain; charset="us-ascii"
> A new RFC has just landed: https://sel4.atlassian.net/browse/RFC-12
> If you have any feedback, please comment there.
Ooh, exciting. I wonder if something similar to Mesa could be implemented for graphics, to ease porting existing Mesa drivers.
I remember talk in one of the developer hangouts I was in about a
proof of concept for a high-throughput asynchronous driver layer for
seL4 (presumably based on notifications). Has code for this been
released anywhere? I'm going to be starting on my own IPC transport
layer and I want to include asynchronous message passing as an option.
I am trying to do a device pass-through for a qemu-arm-virt implementation of seL4. Although there are no resources on how to do it on ARM, I followed the procedures for x86 found here . There are differences between the two architectural implementations thus can't be successful.
I tried to pass the image as an argument to Simulate,
parser.add_argument('--extra-qemu-args', dest='qemu_sim_extra_args', type=str,
help="Additional arguments to pass onto QEMU", default="-device virtio-blk-pci,drive=drive0 -drive file=/****/***/****/projects/camkes-vm-images/qemu-arm-virt/sdcard.img,format=raw,if=none,id=drive0")
The machine can start successfully, but it keeps dropping to the initramfs and there is no sda in /dev/. Is there someone who is successful in passing through a device to qemu-arm-virt? Are there any documents to do that?