Modeling operating systems schedulers with multi-stack-queue grammars