bench_sched_messaging
int bench_sched_messaging(int argc, const char **argv);
{ "messaging", "Benchmark for scheduling and IPC", bench_sched_messaging },