Multicore Schedulers with Provable Properties