Scheduling the execution of multiple concurrent tasks on shared resources such as CPUs and network links is essential to ensuring the reliable operation of many autonomic systems. Well known techniques such as rate-monotonic scheduling can offer rigorous timing and preemption guarantees, but only under assumptions (i.e., a fixed set of tasks with well-known execution times and invocation rates) that do not hold in many autonomic systems. New hierarchical scheduling techniques are better suited to enforce the more flexible execution constraints and enforcement mechanisms that are required for autonomic systems, but a rigorous foundation for verifying and enforcing concurrency and timing guarantees is still needed for these approaches. The primary contributions of this paper are: (1) a scheduling policy design technique that can use different decision models across a wide range of systems models, and an example of how a specific (Markov Decision Process) decision model can be applied to a basic multi-threaded system model; (2) novel model checking techniques that can evaluate the behavior of the system model when it is placed under the control of the resulting scheduling policy; and (3) an evaluation of those scheduling policy design and model checking techniques for a simple but representative example of the kinds of execution scenarios that can arise in autonomic systems.
展开▼
