Data-Intensive Distributed Systems LaboratoryProject -- Theory of Priority Scheduling Systems (Stefan Muller)
Many high-performance computing systems contain tasks of varying priority. Consider a file storage system that is constantly indexing and analyzing metadata in order to optimize search time as well as storage usage, but must also handle store and load requests: the analytics and optimization processes are low-priority background tasks but the requests must be handled quickly to keep the system responsive. In prior work, we have developed priority scheduling algorithms for such systems that provably respect bounds on how much a high-priority computation can be delayed by a lower-priority computation. The proof models a parallel computation as a dependency graph in which each graph node is assigned a priority, and a scheduler as a scheme for assigning graph nodes to processors respecting the dependencies. The result holds as long as the program is free of priority inversions, that is, no high-priority graph node can be caused to be unavailable by a low-priority node. We also developed a type system for a parallel language model that ensures that programs are free of this type of priority inversion.
The above work makes many assumptions, for example that priorities are known at compile time and do not change during execution. In this project, students will work toward relaxing these assumptions and extending the models and languages to be more interesting and expressive. These changes will require extending the type system of the language to make sure that the new features do not allow for priority inversions, as well as extending all of the models and proofs to account for the new features. For example, allowing "first-class" priorities that are not known at compile time will require extending the graph-based scheduling model and the proof of the time bound above to account for all possible assignments of priorities at runtime. In a language, "first-class" priorities will correspond to variables that hold priority levels; in order to continue to prevent priority inversions, the type system will need to be extended with refinement types indicating any known restrictions on the priority level contained in a variable (e.g. "x has priority at least MEDIUM").
Not all students will need to work on all facets of a particular language feature, which allows students of many varying backgrounds to participate and collaborate. For example, the language and type systems extensions are suitable for students who have taken an upper-level programming languages course, while students who have had introductory algorithms and data structures coursework will likely be able to work on the time bound models and corresponding proofs.