Devel

devel@sel4.systems

20 participants
1384 discussions

syscall.c
by Vasily A. Sartakov 11 Oct '16

11 Oct '16

Greetings. I have moved forward to tests in my our MIPS port. Some of them work fine, but not all. Now I have a question about syscall.c test. What exactly we test here? In ARM-based part I see initialisation of 12 registers, performing syscall with further checking that our initialised registers have original values. So, as far I understand, these registers should be modified in a syscall’s inline, thus, they should be allocated on the stack and reloaded after the end of syscall. Right? My issue here is that I have much many than 12 registers and my compiler chooses them randomly (for me). For example, sometimes it uses only S0-S7 with some T0-T9 registers, sometimes all T0-T9 with some S0-S7 registers. Moreover, I cannot put more than 30 asm instructions in one inline (gcc error), thus, maybe I should specify proper register name here. But for that, I should be sure that I understand this test correct. Can we help me? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

Spawn new process
by Andrew Mine 11 Oct '16

11 Oct '16

Hi I am working with sel4-tutorials and wanted to spawn a new process using int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka, vspace_t *spawner_vspace, sel4utils_process_config_t config); However, I am not able to understand some of the details required to initialize the parameter config used in the function. Can someone give me link to an example of sorts where this is used. Regards Andrew Mine

1 0

adding new code to VMM on TK1
by PX 11 Oct '16

11 Oct '16

Hi, Please forgive my ignorance. I want to add new code to the seL4-based VM for TK1. However, I find it is hard to add new directories. The newly added directories are always ignored or can not be found by compiler. What's the correct way to add new directories? which scripts we should look into? thanks Peng

3 4

questions about the device driver in virtual machine on ARM seL4 (TK1 board)
by PX 06 Oct '16

06 Oct '16

Hi, I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio. 2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. Do I miss something? Thanks Peng

2 4

Post-mutikernel approach to multiprocessor support?
by Jeff Waugh 04 Oct '16

04 Oct '16

Hi all, Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support? (I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.) Thanks, Jeff

2 5

Possible seL4 developer day Dec 15–16 in Malibu
by Gernot.Heiser＠data61.csiro.au 04 Oct '16

04 Oct '16

Dear seL4 Community, Part of the Data61 seL4 Team will be in Malibu in mid December and we are considering running another Developer Day. As in the past, this would actually run over 1.5 days, from the morning of the 15th to about mid-day on the 16th and be a combination of lectures and hands-on sessions. As usually we’ll try to make this a free event, provided that our friends at HRL Labs can host us. We have been discussing the possibility of providing an advanced stream besides the “newbie” version we had been running in the past. Right now, we are gauging interest in this. So, if you are interested in participating on those two days, would you please let Ihor know 1) how many participants you expect from your organisation 2) whether you are interested in the newbie or an advanced version, 3) if advanced, what topics you would like covered Examples of advanced materials - advanced driver writing/porting, eg how to port a real Linux driver - advanced real-time topics: eg building stuff from scratch rather than filling in templates - locking and synchronisation - architecting seL4-based systems - process for building real systems: throw everything into a VM, and then extract bits into native components - anything specific you are interested in We’d imagine the advanced stream to be less structured, emphasising largely independent work on a specific problem, with people around to help. It could even be solving a particular problem you have (but we’d need to understand what you’re trying to build beforehand). Gernot & Ihor

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Gernot.Heiser＠data61.csiro.au 29 Sep '16

29 Sep '16

We have just received this comment on github, which I think merits some explanation: > There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. Summary: I accept that this is a valid use case, but the suggested solution is not the right one. There are two reasons why I’m saying this: 1) the current behaviour of send-only IPC is correct and cannot be changed, 2) send-only IPC is the wrong way to address this use case. Re (1): Anyone who tried to use seL4_Send() or seL4_NBSend() will likely have noticed that they are of very little use, because you don’t know whether the message was transferred. So, why can't we return at least a boolean value, indicating whether a message has been delivered or it was dropped on the floor? It’s simple: this would violate the dataflow guarantees provided by seL4. Send-only IPC is there to enable one-way information flow, and consequently can be invoked using a send-only cap. But a send-only cap must not allow any information flow from the receiver to the sender (or else all our isolation proofs would break down). Basically, a return status that can be influenced by the receiver constitutes a back channel that is not authorised by a cap, and as such is verboten. This means that send-only IPC is of very little practical use, except where you really want one-way information transfer, or you have a higher-level protocol that lets you get away with not knowing whether the message was lost. (Eg if the receiver being not ready is a protocol violation by the receiver, and it has only itself to blame for losing the message.) So, could we make send-only IPC a bit more useful by changing the semantics slightly? For example, we could have a return value that indicates successful message delivery if the send was invoked with a send+receive cap, but will always return false if the invocation used a send-only cap? In principle that would be doable without violating security requirements. The cost would be extra checking. It would also be somewhat unsystematic if the semantics of a send-only operation would depend on whether your cap has receive rights as well. It’d be arguably misleading, as you’re doing more than sending. This gets me to (2): send-only IPC is the wrong way to solve the problem. The above use case is clearly one where info flow is inherently two-way: you send something and need an acknowledgment of receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. The problem, of course, is that seL4_Call() is always blocking, there is no polling variant of this syscall. Should there be an seL4_NBCall()? Arguably yes, just as the RT branch already provides a seL4 SignalRecv() syscall, which is the non-blocking equivalent of seL4_ReplyRecv(). Will it happen? Possibly, but not in mainline the near future. The reason is that to add this (fairly simple) feature to the mainline kernel will require verifying it, and our verification engineers are presently very busy delivering on contracted milestones. We’ll discuss this internally. In the meantime I’ve added some explanation of the semantics of seL4_Send()/seL4NBSend() to the FAQ on the seL4 wiki. Gernot

4 6

quesion about TK1 Linux irq
by PX 27 Sep '16

27 Sep '16

Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng

2 1

Fwd: [Fwd: quesion about TK1 Linux irq]
by Jason.Butler＠data61.csiro.au 27 Sep '16

27 Sep '16

The irq numbers are remapped in: kernel/include/plat/tk1/plat/machine.h Jason ? -------- Forwarded Message -------- From: PX <seawolf.peng(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] quesion about TK1 Linux irq Date: Mon, 26 Sep 2016 17:38:47 -0400 Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Matt Rice 26 Sep '16

26 Sep '16

Gernot.Heiser wrote: > We have just received this comment on github, which I think merits some explanation: >> There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. ... >This gets me to (2): send-only IPC is the wrong way to solve the problem. > >The above use case is clearly one where info flow is inherently two-way: you send >something and need an acknowledgment of > receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than > separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. New to sel4 and the list (so sorry for stuffing up the threading) Couldn't at the expense of an extra notification send, use a notification where the receiver of the notification then should call the then do a non-blocking reply. I didn't see reply being non-blocking described in the manual so please correct me if i am wrong. This only works one party is willing to block correct, and there is no way to short circuit the call if an incoming message could be delivered to the call'ing process before the call can be completed? Although it would seem to take some amount of gymnastics to balance sending and receiving... so if really neither are willing to wait there is always notifications+shared memory?

3 4

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel