Time Petri Net Models for a New Queuless and Uncentralized Resource Discovery System

TL;DR

This paper models a fully distributed resource reservation system using Time Petri Nets to verify its qualitative and quantitative properties without relying on central administration.

Contribution

It introduces a novel Petri Net model for a decentralized resource discovery system, detailing algorithms and verification methods.

Findings

Model successfully captures system behavior

Enables property verification of the distributed system

Supports analysis of resource reservation processes

Abstract

In this report, we detail the model using Petri Nets of a new fully distributed resource reservation system. The basic idea of the considered distributed system is to let a user reserve a set of resources on a local network and to use them, without any specific, central administration component such as a front-end node. Resources can be, for instance, computing resources (cores, nodes, GPUs...) or some memory on a server. In order to verify some qualitative and quantitative properties provided by this system, we need to model it. We detail the algorithms used by this system and the Petri Net models we made of it.