The Community for Technology Leaders
Green Image
A colored generalized stochastic Petri net (CGSPN) model was used to study the correctness and performance of the Lamport 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 potential of the GSPN modeling technique is illustrated on an academic but nontrivial example of an application from distributed systems.
Index Termsconcurrent program; colored stochastic Petri nets; correctness; Lamport concurrentalgorithm; mutual exclusion problem; parametric formal proof of liveness; performanceevaluation; Markovian analysis; distributed systems; concurrency control; distributedprocessing; Markov processes; performance evaluation; Petri nets; stochastic processes

G. Chiola, P. Chen, G. Balbo and S. Bruell, "An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm," in IEEE Transactions on Parallel & Distributed Systems, vol. 3, no. , pp. 221-240, 1992.
80 ms
(Ver 3.3 (11022016))