On 4/19/24 02:45, Gernot Heiser via Devel wrote:
> On 19 Apr 2024, at 14:00, Andrew Warkentin wrote:
>>
>> Somehow I said Send()/Recv()/Reply() when I meant Call()/Recv()/Send()
>> (MCS of course doesn't even have a distinct Reply() function).
>
> the correct syscall to use is ReplyWait():
>
> R
On 19 Apr 2024, at 14:00, Andrew Warkentin wrote:
>
> Somehow I said Send()/Recv()/Reply() when I meant Call()/Recv()/Send()
> (MCS of course doesn't even have a distinct Reply() function).
the correct syscall to use is ReplyWait():
Recv(…);
while (1) {
ReplyWait(…);
}
Es per my blog:
On Thu, Apr 18, 2024 at 8:31 PM Gernot Heiser via Devel
wrote:
>
> I’m not completely sure what you’re actually measuring here (actually I’m
> totally unsure
> what your setup really is, I can’t make sense of the above description in
> terms of
> what the seL4 system is doing).
> But measuring p
On 18 Apr 2024, at 23:55, Andrew Warkentin wrote:
>
> Somebody in the Zoom call the other day (IIRC it was Gernot) said that
> seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is
> somehow faster in a simple benchmarking experiment in which a client
> repeatedly sends messages
On 4/18/24 05:34, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 19:18, Hugo V.C. wrote:
>>
>> "A web browser is a good example of this. The number of security
>> domains is at least the number of origins in use, which can be
>> extremely large. Furthermore, some origins might be CPU-
On 4/18/24 07:12, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
>
> The challenge that I probably didn't expressed correctly, is to integrate
> seL4 on top of other dynamic systems (in example to virtualize a browser), as
> seL4 needs to know in advance how much me
"Running seL4 in any way other than on bare metal makes no sense
whatsoever."
There are scenarios where it makes sense. The power of seL4 is isolation
guarantee. That is, software running virtualized on top of seL4 can't
escape from seL4. This means it can be used to safely run a web browser
(virt
Somebody in the Zoom call the other day (IIRC it was Gernot) said that
seL4 IPC is considerably faster than QNX IPC, but it seems that QNX is
somehow faster in a simple benchmarking experiment in which a client
repeatedly sends messages to a bit-bucket server, using the TSC to
determine timing.
I'
On 18/04/24 12:12, Gernot Heiser via Devel wrote:
> On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
>
> The challenge that I probably didn't expressed correctly, is to integrate
> seL4 on top of other dynamic systems (in example to virtualize a browser), as
> seL4 needs to know in advance how much m
On 18 Apr 2024, at 20:38, Hugo V.C. wrote:
The challenge that I probably didn't expressed correctly, is to integrate seL4
on top of other dynamic systems (in example to virtualize a browser), as seL4
needs to know in advance how much memory will have available... Running seL4 on
bare metal is
"All this is a matter for user mode. "
Well... in seL4. In standard OSs (Windows, Linux...) this is a matter of
kernel mode. And here is the party. Of course if you use seL4 as TCB then
you can partition whatever you want on top.
The challenge that I probably didn't expressed correctly, is to in
On 18 Apr 2024, at 19:18, Hugo V.C. wrote:
>
> "A web browser is a good example of this. The number of security
> domains is at least the number of origins in use, which can be
> extremely large. Furthermore, some origins might be CPU-intensive."
>
> Yes. That's the challenge when you tr
"A web browser is a good example of this. The number of security
domains is at least the number of origins in use, which can be
extremely large. Furthermore, some origins might be CPU-intensive."
Yes. That's the challenge when you try to use a solution aimed to static
systems for dynami
13 matches
Mail list logo
