Unified Categorical Models for Three Typical Resource Allocation Problems

摘要

This paper concerns formalization of resource allocation using category theory, rather than a new algorithm to solve these problems. The unified and efficient categorical models for three specific resource allocation problems-including dinning philosophers problem, drinking philosophers problem and committee coordination problem - is originally presented based on Chandy-Misra's acyclic precedence graph strategy and our previous experience in defining the categorical semantics for distributed dinning philosophers problem. Four categories (including Dinners Category, Drinkers Category, Committees Category and Functors Category) defined in our paper not only facilitate to formalize usual concepts (such as task, resource, precedence) of resource allocation problems, but also give good directions to reason the relationships between these three typical problems. Finally, we formally proof some properties of symmetry, safety (non-deadlock), liveness (non-starvation) and concurrency, which all satisfied in our models.