Hi guys,

    I have downloaded the lastest seL4 repo and built the seL4 kernel.

    And I reuse the code in
sel4test/projects/sel4test/apps/sel4test-tests/src/tests/ipc.c.

    To test the fast, I made minor modifications: first, set caller and
callee to the same priority; second, caller uses seL4_Call while callee
uses seL4_ReplyRecv.


     However, the fastpath takes more than 2000 cycles (a round trip).


     Build: use the lastest provided docker and ../init-build.sh -
     DPLATFORM=x86_64 -DCMAKE_BUILD_TYPE=Release

     Both hardware and Qemu show similar results. (4.0GHz skylake CPU)



     BTW. The manifest is the same as
https://sel4.systems/About/Performance/home.pml (i.e.,
bf13e9f673484825a60f9950cf688ff33ac841ad).


    Any advices about the issue?


Best,
Jinyu Gu,
Institute of Parallel and Distributed Systems (IPADS),
School of Software,
Shanghai Jiao Tong University
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to