Modeling operating systems schedulers with multi-stack-queue grammars

Abstract

This original method for specifying and checking the se- quences of events taking place in process scheduling brings the classical syntax-directed approach of compilation to this new area. The formal language of scheduling events cannot be specified by BNF grammars, but we use instead the Augmented BNF grammars, which combine breadth- first and depth-first derivations. Their recognizers feature one or more FIFO or LIFO tapes. The basic scheduling policies are covered: FCFS, time-slicing, mutex. Combined policies, such as readers/writers and back- ground/foreground, are obtainable by composition. Constraints on the minimum number of data structures (i.e. queues) for priority scheduling policies may be proved by using a pumping lemma. The construction of schedule checkers is presented in the form of augmented LL(1) parsers. For scheduling algorithms, such as shortest job first, which depend on parameters and in particular on time, a syntax-directed approach is pro- posed, which adds semantic attributes and functions to the underlying augmented BNF grammar.