AN EXAMPLE OF MODELING AND EVALUATION OF A CONCURRENT PROGRAM USING COLORED STOCHASTIC PETRI NETS - LAMPORT FAST MUTUAL EXCLUSION ALGORITHM

被引：22

作者：

BALBO, G ^{[1
]}

CHIOLA, G ^{[1
]}

BRUELL, SC ^{[1
]}

CHEN, PZ ^{[1
]}

机构：

[1] UNIV IOWA,DEPT COMP SCI,IOWA CITY,IA 52242

来源：

IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS | 1992年 / 3卷 / 02期

关键词：

CONCURRENT ALGORITHMS; CORRECTNESS PROOF; LIVENESS; MODELING; MUTUAL EXCLUSION; PERFORMANCE EVALUATION; STOCHASTIC PETRI NETS; WELL-FORMED COLORED NETS;

D O I：

10.1109/71.127262

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：221 / 240

页数：20

共 25 条

[11]

Dijkstra E. W., 1968, Programming languages, P43

[12]

DUTHEILLET C, 1989, 3RD P INT WORKSH PET

[13]

GOOD D, 1979, 6TH P ACM S PRINC PR

[14]

HADDAD S, 1987, THESIS U P M CURIE P

[15]

HADDAD S, 1988, 9TH P EUR WORKSH APP

[16] COLORED PETRI NETS AND THE INVARIANT-METHOD [J].

JENSEN, K .

THEORETICAL COMPUTER SCIENCE, 1981, 14 (03) :317-336

[17]

JENSEN K, 1991, IN PRESS ADV PETRI N

[18] A FAST MUTUAL EXCLUSION ALGORITHM [J].

LAMPORT, L .

ACM TRANSACTIONS ON COMPUTER SYSTEMS, 1987, 5 (01) :1-11

[19]

MARSAN MA, 1987, AUG P INT WORKSH PET, P44

[20]

MARSAN MA, 1984, ACM T COMPUT SYST, V2

← 1 2 3 →