Exact schedulability analysis of global multi-processor IUF scheduling using symbolic model checking

Real time scheduling spans a broad spectrum of algorithms for simple uniprocessors to highly sophisticated multiprocessors. As the world nears the end of Moore's Law, more emphasis is being laid on the use of multi-processors in embedded systems. This has lead to a rise in several new scheduling schemes for multi-processor environments. Naturally there arises a need for an accurate comparison of the schedulabilities of each of these schemes in order to prove their superiority over others. The two-fold aim of this paper is to present a technique for the exact schedulability analysis of global multi-processor schedulers and, based on this intermediary result, prove the schedulability superiority of a novel multi-processor scheduling algorithm. The exact schedulability analysis technique presented here is symbolic model checking in NuSMV, and we have used this technique to investigate the schedulability of global Instantaneous Utilization Factor (IUF) based scheduling. Our analysis shows a substantial improvement in the acceptance of task sets with heavier utilizations.