Hi,

2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"?

This indicates if the thread is returning from a system call (therefore the instruction pointer needs to be updated) or a preemption. See the function activateThread which does the update.

3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means.

What "Cycles" means in this benchmark?

This is an IPC throughput benchmark.

"The existing multicore benchmark measures IPC throughput of a client and server, both pinned to the same processor, sending fastpath, 0-length IPC messages via seL4_Call and seL4_ReplyRecv . One pair of client and server is set up per core. Both threads are the same priority and the messages are 0 length. Each thread spins for a random amount with an upper bound N between each subsequent IPC. As N increases so does IPC throughput, as fewer calls are made." -- (from my phd thesis which used this benchmark - https://github.com/pingerino/phd/blob/master/phd.pdf?)

Cycles corresponds to the upper bound on the number of cycles between IPC.

4. I try to measure IPC performance with SMP is on.

I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles.

I can't offer further analysis without seeing your benchmark code. Those results don't look right. If you put your code up we're happy to take a look.

Are these results are available?

Sorry, we don't have an SMP IPC benchmark currently. ?Note that our current ipc benchmarks aren't written for multicore, and our SMP IPC path is not heavily optimised for the sake of simplicity in our initial multicore verification project.

Thanks, Anna.

________________________________ From: Devel devel-bounces@sel4.systems on behalf of 송대영 scribnote5@gmail.com Sent: Wednesday, 31 October 2018 9:13 PM To: devel@sel4.systems Subject: [seL4] seL4 IPC and SMP question.

HI, I have a question about IPC and SMP.

I ran sel4bench on sabre lite(i.mx6, arm v7).

1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler?

2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"?

3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput.

4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?