Queue-less, Uncentralized Resource Discovery: Formal Specification and Verification.
Camille Coti, Sami Évangelista, Kaïs Klai · Espace ÉTS (ETS) · 2015
A New Fully Distributed Resource Management System In this paper, we present a formal approach for the specification and the verification of a fully distributed resource reservation system. Our system is made of two parts: the launcher, which is executed by the user who wants to run a job on a set of computing nodes, and the agent, which is a daemon running on all the resources that exist in the system. Clients must have an exclusive access to the resources that are allocated for them. Under the requirement that clients have reasonable requirements, all the clients’ requests are answered positively in a finite time and all the jobs are executed completely. In order to ensure the correctness of our system regarding such