A distributed resource allocation algorithm for many processes

TL;DR

This paper presents a distributed, starvation-free resource allocation algorithm for many processes with conflicting resource requirements, verified using formal methods.

Contribution

It introduces a simple, starvation-free algorithm for resource allocation among infinitely many processes communicating asynchronously.

Findings

Algorithm guarantees starvation-freedom.

Processes only wait when resource requirements conflict.

Verified correctness with the PVS proof assistant.

Abstract

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. For each execution of CS, these requirements are given anew. In the resource requirements, levels can be distinguished, such as e.g. read access or write access. We allow infinitely many processes that communicate by reliable asynchronous messages and have finite memory. A simple starvation-free solution is presented. 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.