For the most recent entries see the Petri Nets Newsletter.

An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm.

Balbo, G.; Chiola, G.; Bruell, S.C.

In: IEEE Transactions on Parallel and Distributed Systems Vol.3. 2.. 1992.

Abstract: We use a colored generalized stochastic Petri net (CGSPN) model to study both the correctness and performance of Lamport's concurrent algorithm to solve the mutual exclusion problem on machines lacking an atomic ``test and set'' instruction. In particular, a parametric formal proof of liveness is developed based on the structure and initial state of the model. The performance evaluation is based on a Markovian analysis that exploits the symmetries of the model to reduce the cost of the numerical solution. Both kinds of analysis are supported by efficient algorithms. The aim of the paper is to illustrate the potential of the GSPN modeling technique on an academic but nontrivial example of an application from distributed systems.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography