Resource allocation is the problem that a process may enter a critical section CS of its code only when its resource requirements are not in conflict with those of other processes in their critical sections. A classical description is as the Drinking Philosophers, in a paper by Chandy and Misra in ACM TOPLAS (1984). There, the processes form a fixed finite graph, and the resources are bottles on the edges of the graph. We treat the general problem with unboundedly many processes, finitely many resources, and every process may apply for all resources. For each execution of CS, the resource requirements can be different. In the resource requirements, levels can be distinguished, such as e.g. read access or write access.
We allow unboundedly many processes that communicate by asynchronous messages and have extendable finite memory. We present a simple starvation-free solution. The final paper is "A distributed resource allocation algorithm for many processes", Acta Informatica 50 (2013) 297-329. It is available at link.springer.com. Processes only wait for one another when they have conflicting resource requirements. The correctness of the solution is argued with invariants and temporal logic. It has been verified with the proof assistant PVS (version 5.0); readers familiar with PVS can inspect and process the gzipped PVS dump file. The arXiv has an older version.
Comments and questions are welcome.
Back to my home page.
Wim H. Hesselink