Selectors: High-Level Resource Schedulers

Resource sharing problems can be described in three basically independent modular components. ¿ The constraints the resource places upon sharing because of physcal limitations and consistency requirements. ¿ The desired ordering of resource requests to achieve efficiency-either efficiency of resource utilization or efficiency of processes making the requests. ¿ Modifications to the ordering to prevent starvation of processes waiting for requests which might otherwise never receive service. A high-level nonprocedural language to specify these components of resource sharing problems is described. General deadlock and starvation properties of selectors are proven. Solutions to several classic resource sharing problems are shown to illustrate the expressiveness of this language. Proof techniques for this high-level language are introduced to show how to prove particular selectors are or are not deadlock and starvation free.