An example of modeling and evaluation of a concurrent program using colored stochastic Petri nets: Lamport's fast mutual exclusion algorithm

淡江大學機構典藏 > 工學院 > 資訊工程學系暨研究所 > 期刊論文 > Item 987654321/45364

jsp.display-item.identifier=請使用永久網址來引用或連結此文件: https://tkuir.lib.tku.edu.tw/dspace/handle/987654321/45364

题名:	An example of modeling and evaluation of a concurrent program using colored stochastic Petri nets: Lamport's fast mutual exclusion algorithm
作者:	Balbo, Giafranco;Chiola, Giovanni;Bruell, Steven C.;陳伯榮;Chen, Po-zung
贡献者:	淡江大學資訊工程學系
日期:	1992-03
上传时间:	2010-03-26 19:07:17 (UTC+8)
出版者:	Piscataway: Institute of Electrical and Electronics Engineers (IEEE)
摘要:	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
關聯:	IEEE Transactions on Parallel and Distributed Systems 3(2), pp.221-240
DOI:	10.1109/71.127262
显示于类别:	[資訊工程學系暨研究所] 期刊論文

文件中的档案:

档案	描述	大小	格式	浏览次数
1045-9219_3(2)p221-240.pdf		1969Kb	Adobe PDF	1278	检视/开启

在機構典藏中所有的数据项都受到原著作权保护.

TAIR相关文章