Automatically assigned DDC number:

Manually assigned DDC number: 00435

Number of references: 0

Title: Boleslaw K. Szymanski and Jose M. Vidal



Subject: Boleslaw K. Szymanski,Jose M. Vidal Boleslaw K. Szymanski and Jose M. Vidal

Description: This paper presents an efficient method of verification of a class of symmetric parallel programs characterized by a limited usage of communication variables. The limitation requires that any process identifier appearing in a condition must be a logical variable bounded by the universal or existential quantifier. Hence, programs in this class are only able to test whether a set of processes in a certain state is empty or not. Our approach to automatic verification is to reduce the verified program to a directed graph. Nodes of this diagraph represent different states of the program. Each edge of the diagraph is labeled with a predicate that must be satisfied if this edge is to be selected by a state transition. We use standard reachability analysis to verify the properties of the program. The efficiency of the approach results from the limitations imposed on the form of the conditions in the verified program. Using this method, we prove that a novel mutual exclusion program enforces mutual exclusion and is deadlock-free. Keyword Codes: C.1.2; C.4; I.6 Keywords: Multiprocessors; Performance of Systems; Simulation and Modeling

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1997-06-26

Pubyear: unknown

Format: ps



Language: en

Rights: unrestricted


<?xml   version="1.0"   encoding="UTF-8"?>


      <rec   ID="SELF"   Type="SELF"   CiteSeer_Book="SELF"   CiteSeer_Volume="SELF"   Title="Boleslaw   K.   Szymanski   and   Jose   M.   Vidal"   />