CINECA IRIS Institutional Research Information System
IRIS è il sistema di gestione integrata dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall'Università degli Studi di Torino.
AperTO è l'archivio istituzionale Open Access destinato a raccogliere, rendere visibile e conservare la produzione scientifica dell'Università degli Studi di Torino.
EnglishA 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.
| Titolo: | An Example of Modelling and Evaluation of a Concurrent Program using Coloured Stochastic Petri Nets: Lamport's Fast Mutual Exclusion Algorithm | |
| Autori Riconosciuti: | ||
| Autori: | G. BALBO; G. CHIOLA; S.C. BRUELL; P. CHEN | |
| Data di pubblicazione: | 1992 | |
| Abstract: | 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. | |
| Volume: | 3 (2) | |
| Pagina iniziale: | 221 | |
| Pagina finale: | 240 | |
| Anno del convegno: | 1992-March | |
| Digital Object Identifier (DOI): | 10.1109/71.127262 | |
| Parole Chiave: | Stochastic Petri nets; Well formed coloured nets; Concurrent algorithms; Mutual exclusion; Correctness proof; Modelling; Performance evaluation | |
| Rivista: | IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS | |
| Appare nelle tipologie: | 03A-Articolo su Rivista |
File in questo prodotto:
Copyright © 2022