-----邮件原件-----
发件人: [email protected] [mailto:[email protected]] 
发送时间: 2021年11月18日 5:56
收件人: [email protected]
主题: Devel Digest, Vol 125, Issue 2

Send Devel mailing list submissions to
        [email protected]

To subscribe or unsubscribe via email, send a message with subject or body 
'help' to
        [email protected]

You can reach the person managing the list at
        [email protected]

When replying, please edit your Subject line so it is more specific than "Re: 
Contents of Devel digest..."

Today's Topics:

   1. Re: some question about seL4 performance (Gerwin Klein)
   2. Re: some question about seL4 performance (Gernot Heiser)
   3. Re: some question about seL4 performance (Gerwin Klein)


----------------------------------------------------------------------

Message: 1
Date: Wed, 17 Nov 2021 21:24:57 +0000
From: Gerwin Klein <[email protected]>
Subject: [seL4] Re: some question about seL4 performance
To: yadong.li <[email protected]>
Cc: "[email protected]" <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="utf-8"


> On 18 Nov 2021, at 02:06, yadong.li <[email protected]> wrote:
> 
> Hi:
>  I learn the sel4 performance form 
> https://sel4.systems/About/Performance/
>  I focus on the ARMv8 platform, from the website, the parameters are as 
> follows:
>     ISA    Mode  Core/SoC/Board   Clock         IRQ Invoke         IPC call  
> IPC reply
>  "Armv8a     64     A57/Tx1/Jetson   1.9 GHz         863 (18)          
> 396(15)   397(4)"
> 
>  I want to know what is the length of IPC for the record provided on the web 
> page , when test IPC call and reply?  0 or 10?

The page reports the 0-length numbers. The idea is that IPC should fit into 
registers, the 10 case is the one that make it spill into memory deliberately. 
That number is good to know for development, but should not be the main 
performance characteristic.

Cheers,
Gerwin


------------------------------

Message: 2
Date: Wed, 17 Nov 2021 21:36:39 +0000
From: Gernot Heiser <[email protected]>
Subject: [seL4] Re: some question about seL4 performance
To: "[email protected]" <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="utf-8"

On 18 Nov 2021, at 08:24, Gerwin Klein <[email protected]> wrote:
> 
> The page reports the 0-length numbers. The idea is that IPC should fit into 
> registers, the 10 case is the one that make it spill into memory 
> deliberately. That number is good to know for development, but should not be 
> the main performance characteristic.

Note that whether data is transferred solely in registers or using a memory 
buffer does not make a big difference on contemporary hardware. However, our 
present implementation reverts to the slow path as soon as the message size 
overflows the physical message registers, which will make the PIC much slower. 

This is something that could be fixed by widening the fastpath conditions 
without much complications. However, we haven’t yet come across an important 
use case where this matters, so there isn’t much motivation for investing time 
in it.

Gernot

------------------------------

Message: 3
Date: Wed, 17 Nov 2021 21:56:06 +0000
From: Gerwin Klein <[email protected]>
Subject: [seL4] Re: some question about seL4 performance
To: Gernot Heiser <[email protected]>
Cc: "[email protected]" <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="us-ascii"



On 18 Nov 2021, at 08:36, Gernot Heiser 
<[email protected]<mailto:[email protected]>> wrote:

On 18 Nov 2021, at 08:24, Gerwin Klein 
<[email protected]<mailto:[email protected]>> wrote:

The page reports the 0-length numbers. The idea is that IPC should fit into 
registers, the 10 case is the one that make it spill into memory deliberately. 
That number is good to know for development, but should not be the main 
performance characteristic.

Note that whether data is transferred solely in registers or using a memory 
buffer does not make a big difference on contemporary hardware. However, our 
present implementation reverts to the slow path as soon as the message size 
overflows the physical message registers, which will make the PIC much slower.

Yes I should have mentioned that. If you look at the raw numbers for x86, eg. 
at https://github.com/seL4/sel4bench/actions/runs/1469475721#artifacts, fast 
path/no fast path is almost equal for length 10. You get a tiny bit better 
performance for length 10 when the fast path is switched off completely, 
because it doesn't first have to test whether to take the fast path or not.

Cheers,
Gerwin


------------------------------

Subject: Digest Footer

_______________________________________________
Devel mailing list -- [email protected] To unsubscribe send an email to 
[email protected]


------------------------------

End of Devel Digest, Vol 125, Issue 2
*************************************
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]

Reply via email to