• Publication
  • 1992
  • Issue No. 2 - March
  • Abstract - An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm
March 1992 (vol. 3 no. 2)
pp. 221-240
ASCII Text
x 
 
G. Balbo, G. Chiola, S.C. Bruell, P. Chen, "An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm," IEEE Transactions on Parallel and Distributed Systems, vol. 3, no. 2, pp. 221-240, March, 1992.
 
 
BibTex
x
 
@article{ 10.1109/71.127262,
author = {G. Balbo and G. Chiola and S.C. Bruell and P. Chen},
title = {An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm},
journal ={IEEE Transactions on Parallel and Distributed Systems},
volume = {3},
number = {2},
issn = {1045-9219},
year = {1992},
pages = {221-240},
doi = {http://doi.ieeecomputersociety.org/10.1109/71.127262},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Parallel and Distributed Systems
TI - An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm
IS - 2
SN - 1045-9219
SP221
EP240
EPD - 221-240
A1 - G. Balbo,
A1 - G. Chiola,
A1 - S.C. Bruell,
A1 - P. Chen,
PY - 1992
KW - 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
VL - 3
JA - IEEE Transactions on Parallel and Distributed Systems
ER -
 
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.

[1] M. Ajmone Marsan, G. Balbo, and G. Conte, "A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems,"ACM Trans. Comput. Syst., vol. 2, pp. 93-122, May 1984.
[2] M. Ajmone Marsan, G. Balbo, G. Chiola, and G. Conte, "Generalized stochastic Petri nets revisited: Random switches and priorities," inProc. Int. Workshop Petri Nets and Performance Models, Madison, WI, IEEE Computer Society Press, Aug. 1987, pp. 44-53.
[3] C. Dutheillet and S. Haddad, "Aggregation of states in colored stochastic Petri nets: application to a multiprocessor architecture," inProc. 3rd Int. Workshop on Petri Nets and Performance Models(Kyoto, Japan), Dec. 1989, pp. 40-49.
[4] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad, "Stochastic well-formed colored nets and multiprocessor modeling applications," Tech. Rep. 90/41, UniversitéParis 6, 4 Place Jussieu, 75 252 Paris Cedex 05, France, Oct, 1990. IBP Tech. Rep., submitted for publication.
[5] L. Lamport, "A fast mutual exclusion algorithm,"ACM Trans. Computer Syst., vol. 5, no. 1, pp. 1- 11, Feb. 1987.
[6] G. Balbo and G. Chiola, "Stochastic Petri net simulation," inProc. 1989 Winter Simulation Conf., Washington DC, Dec. 1989.
[7] S. Owicki and D. Gries, "An axiomatic proof technique for parallel programs,"Acta Informatica, vol. 6, no. 4; pp. 319-346, 1976.
[8] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[9] D. I. Good, R. M. Cohen, and J. Keeton-Williams, "Principles of proving concurrent programs in Gypsy," inProc. 6th Symp. Principles of Programming Languages, ACM, Jan. 1979.
[10] J. Nagle and S. Johnson, "Practical program verification: Automatic program proving for real-time embedded software," inProc. ACM 10th Symp. Principles Programming Languages, Jan. 1983, pp. 48-58.
[11] M. Abrams and A.K. Agrawala, "Exact performance analysis of two distributed processes with-one synchronization point," Tech.Rep., Univ. of Maryland, 1988.
[12] C. Chou, "Performance evaluation of concurrent programs modeled by timed pq-net," inProc. IEEE COMPSAC'87, Oct. 1987, pp. 465-473.
[13] D. Peng and K. G. Shin, "Modeling of concurrent task execution in a distributed system for real-time control,"IEEE Trans. Comput., vol. C-36, no. 4, Apr. 1987.
[14] G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad, "On wellformed colored nets and their symbolic reachability graph," inProc. 11th Int. Conf. Appl. and Theory Petri Nets, Paris, France, June 1990.
[15] E. W. Dijkstra, "Cooperating sequential processes," inProgramming Languages and Systems, F. Genvys, Ed. New York: Academic, 1968, pp. 43-112.
[16] K. Jensen, "Colored Petri nets: A high level language for system design and analysis," inAdvances on Petri Nets '90, G. Rozenberg, Ed. New York: Springer-Verlag, 1991, to be published.
[17] S. Haddad, "Une categorie regulier de reseau de Petri de haut niveau: Definition, proprietes et reductions," Ph.D. dissertation, Lab. MASI, Universite P. et M. Curie (Paris 6), Paris, France, Oct 1987. These de Doctorat, RR87/197 (in French).
[18] S. Haddad and J. M. Couvreur, "Toward a general and powerful computation of flows for parametrized colored nets," inProc. 9th Euro. Workshop Appl. and Theory of Petri Nets, Venezia, Italy, June 1988.
[19] J. M. Couvreur, "The general computation of flows for colored nets," inProc. 11th Int. Conf. Appl. and Theory Petri Nets, Paris, France, June 1990.
[20] K. Jensen, "Colored Petri nets and the invariant method,"Theoret. Comput. Sci., vol. 14, pp. 317-336, 1981.
[21] M. Silva, J. Martinez, P. Ladet, and H. Alla, "Generalized inverses and the calculation of symbolic invariants for colored Petri nets,"Technique et Science Informatiques, vol. 4, pp. 113-126, 1985.
[22] S. Haddad, "Generalization of reduction theory to coloured nets," inProc. 9th Europ. Workshop Application and Theory of Petri Nets, Venezia, Italy, June 1988.
[23] J. M. Colom, J. Martinez, and M. Silva, "Packages for validating discrete production systems modeled with Petri nets," inApplied Modeling and Simulation of Technological Systems, P. Borne and S. Tzafestas, Eds. New York: Elsevier Science (North Holland), 1987, pp. 529-536.
[24] G. Chiola, "A graphical Petri net tool for performance analysis," inProc. 3rd Int. Workshop Modeling Techniques and Perform. Eval., AFCET, Paris, France, Mar. 1987.
[25] G. Chiola, "GreatSPN1.5 software architecture," inProc. 5th Int. Conf. Modeling Techniques and Tools for Comput. Perform. Eval., Torino, Italy, Feb. 1991.
[26] G. Chiola and G. Franceschinis, "Colored GSPN models and automatic symmetry detection," inProc. 3rd Int. Workshop Petri Nets and Perform. Models, Kyoto, Japan, IEEE Computer Society Press, Dec. 1989.

Index Terms:
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
Citation:
G. Balbo, G. Chiola, S.C. Bruell, P. Chen, "An Example of Modeling and Evaluation of a Concurrent Program Using Colored Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm," IEEE Transactions on Parallel and Distributed Systems, vol. 3, no. 2, pp. 221-240, March 1992, doi:10.1109/71.127262
Usage of this product signifies your acceptance of the Terms of Use.