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?
