Categorial Semantics of a Solution to Distributed Dining Philosophers Problem

摘要

Distributed dining philosophers is regarded as one of the most representative resource allocation problems. Many strategies are employed for avoiding deadlock and starvation, the two well-known problems in Distributed Dining Philosophers Problem(DDPP). In this paper, the formal semantics of DDPP are originally proposed by using category theory based on the Chandy-Mirsa's acyclic directed graph strategy. The goal is to demonstrate how category theory is used in precisely defining categorical semantics and diagrammatically describing philosophers' priority, states-transition, and composition of processes, rather than to design a new algorithm to solve the DDPP. Compared with other formal techniques, category theory not only provides a good mathematical structure for formalizing different relationships and interactions at different abstract levels, but also its diagrammatical representation strengthens the traceability and understandability of philosophers' priority and states-transformation; additionally, its universal constructions (like colimit) offer the ability to manipulate and reason about system configuration.