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?