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?