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.