scholarly journals Computer Aided Verification of Lamport's Fast Mutual Exclusion Algorithm - Using Coloured Petri Nets and Occurrence Graphs with Symmetries

1997 ◽  
Vol 26 (512) ◽  
Author(s):  
Jens Bæk Jørgensen ◽  
Lars Michael Kristensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Mutual Exclusion ◽  
Condensed State ◽  
Coloured Petri Nets ◽  
Computer Tool ◽  
State Spaces ◽  
Index Terms ◽  
High Level ◽  
Mutual Exclusion Algorithm

<p>In this paper, we present a new computer tool for verification of distributed systems. As an example, we establish the correctness of Lamport's Fast Mutual Exclusion Algorithm. The tool implements the method of occurrence graphs with symmetries (OS-graphs) for Coloured Petri Nets(CP-nets). The basic idea in the approach is to exploit the symmetries inherent in many distributed systems to construct a condensed state space. We demonstrate a signigicant increase in the number of states which can be analysed. The paper is to a large extent self-contained and does not assume any prior knowledge of CP-nets (or any other kinds of Petri Nets) or OS-graphs. CP-nets and OS-graphs are not our invention. Our contribution is development of the tool and verification of the example.</p><p><strong>Index Terms:</strong> Modelling and Analysis of Distributed Systems, Formal Verification, Coloured Petri Nets, High-Level Petri Nets, Occurrence Graphs, State Spaces, Symmetries, Mutual Exclusion.</p>

scholarly journals Analysing Coloured Petri Nets by the Occurrence Graph Method

1997 ◽  
Vol 26 (517) ◽  
Author(s):  
Jens Bæk Jørgensen
Keyword(s):  
Distributed Systems ◽  
Petri Nets ◽  
Research Area ◽  
Coloured Petri Nets ◽  
Main Subject ◽  
Graph Method ◽  
Research Areas ◽  
High Level ◽  
Phd Thesis ◽  
Work Done

<p>This paper provides an overview og the work done for the author's PhD thesis. The research area of Coloured Petri Nets is introduced, and the available analysis methods are presented. The occurrence graph method, which is the main subject of this thesis, is described in more detail. Summaries of the six papers which, together with this overview, comprise the thesis are given, and the contributions are discussed.</p><p>A large portion of this overview is dedicated to a description of related work. The aim is twofold: First, to survey pertinent results within the research areas of -- in increasing generality -- Coloured Petri Nets, High-level Petri Nets, and formalisms for modelling and analysis of parallel and distributed systems. Second, to put the results obtained in this thesis in a wider perspective by comparing them with important related work.</p>

JDM: BUILDING DISTRIBUTED SYNCHRONIZATION SUPPORT INTO JAVA

2001 ◽  
Vol 02 (03) ◽  
pp. 269-282
Author(s):  
JIANNONG CAO ◽  
NICK K. C. CHEUNG ◽  
ALVIN CHAN
Keyword(s):  
System Architecture ◽  
Large Scale ◽  
Mutual Exclusion ◽  
Distributed Programming ◽  
Shared Resources ◽  
Object Oriented Design ◽  
Distributed Synchronization ◽  
High Level ◽  
Distributed Mutual Exclusion ◽  
Mutual Exclusion Algorithm

The monitor concept has been widely used in a concurrent programming environment for implicitly ensuring mutual exclusion and explicitly achieving process synchronization. It has also been extended to support high-level distributed programming. In this paper, we present JDM, a distributed monitor construct in Java for programming large-scale distributed systems. The distributed monitor construct is based on a well-know tree-based distributed mutual exclusion algorithm proposed by K. Raymond. To increase scalability of the construct, a two-level system architecture is developed, where the node level controls the access to the system-wide shared resources using Raymond's algorithm and the process level synchronizes local processes based on the local monitor concept. An object-oriented design of the system architecture is presented. Implementation and results of performance evaluation are reported and factors that influence the performance of the construct are discussed.

Condensed State Spaces for Timed Petri Nets

2001 ◽  
pp. 101-120 ◽  
Author(s):  
Søren Christensen ◽  
Lars Michael Kristensen ◽  
Thomas Mailund
Keyword(s):  
Petri Nets ◽  
Condensed State ◽  
Timed Petri Nets ◽  
State Spaces

scholarly journals Model Checking Coloured Petri Nets - Exploiting Strongly Connected Components

1997 ◽  
Vol 26 (519) ◽  
Author(s):  
Allan Cheng ◽  
Søren Christensen ◽  
Kjeld Høyer Mortensen
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
The State ◽  
Connected Components ◽  
Coloured Petri Nets ◽  
Transition Systems ◽  
Strongly Connected Components ◽  
State Spaces ◽  
Labelled Transition Systems ◽  
Strongly Connected

In this paper we present a CTL-like logic which is interpreted over the state spaces of Coloured Petri Nets. The logic has been designed to express properties of both state and transition information. This is possible because the state spaces are labelled transition systems. We compare the expressiveness of our logic with CTL's. Then, we present a model checking algorithm which for efficiency reasons utilises strongly connected components and formula reduction rules. We present empirical results for non-trivial examples and compare the performance of our algorithm with that of Clarke, Emerson, and Sistla.

Token Based Mutual Exclusion in Peer-to-Peer Systems

2012 ◽  
pp. 214-228 ◽  
Author(s):  
Mayank Singh ◽  
Shashikala Tapaswi
Keyword(s):  
Distributed Systems ◽  
Message Passing ◽  
Mutual Exclusion ◽  
Hash Table ◽  
Peer To Peer ◽  
Distributed Hash Table ◽  
Shared Resources ◽  
Peer To Peer Systems ◽  
Mutual Exclusion Algorithm ◽  
Message Overhead

Mutual exclusion is one of the well-studied fundamental primitives in distributed systems, and a number of vital solutions have been proposed to achieve the same. However, the emerging Peer to Peer systems bring forward several challenges to protect consistent and concurrent access to shared resources, as classical peer-to-peer systems, like Napster, Gnutella, et cetera, have been mainly used for sharing files with read only permission. In this chapter, the authors propose a quorum based mutual exclusion algorithm that can be used over any Peer to Peer Distributed Hash Table (DHT). The proposed approach can be seen as extension to traditional Sigma protocol for mutual exclusion in Peer to Peer systems. The basic idea is to reduce message overhead with use of smart nodes present in each quorum set and message passing between the current owners of resource with next resource requester nodes.

Sign in / Sign up

Export Citation Format

Share Document