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?