some question about seL4 performance
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? thank you very much
On 18 Nov 2021, at 02:06, yadong.li <yadong.li@horizon.ai> 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
On 18 Nov 2021, at 08:24, Gerwin Klein <kleing@unsw.edu.au> 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
On 18 Nov 2021, at 08:36, Gernot Heiser <gernot@unsw.edu.au<mailto:gernot@unsw.edu.au>> wrote: On 18 Nov 2021, at 08:24, Gerwin Klein <kleing@unsw.edu.au<mailto:kleing@unsw.edu.au>> 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
participants (3)
-
Gernot Heiser -
Gerwin Klein -
yadong.li