Monday March 23, 1998. 4:10 pm
Room 124 HRBB

Modeling and Model Checking of a Shared Memory Consistency Protocol

Claude Girault.
Department of Computer Science, Université Paris VI Pierre & Marie Curie

Abstract

Distributed Shared Memory (DSM) systems provide the abstraction of a common virtual address space across a network of processors. Such systems employ a variety of protocols to maintain a consistent view of data across all local memories. Due to the practical importance of DSM systems, verification has been applied to some of the underlying protocols. Li and Hudak (1989) proposed several of the pioneering protocols for DSM. A combination of Petri net modelling and model checking has been used to explore some of their protocols. This work has allowed to detect inefficiencies, unstated assumptions, and errors in the original protocol descriptions. The modelling and analysis of one of the protocols will be detailled. Petri net models have been designed at two layers of abstractionand allow to obtains some safety invariants. The corresponding specifications for model checking also provide liveness checks. Verification statistics show the complexity of the state space. This combination of models and specifications gives several slightly different views of the protocol. The advantage is a greater confidence in the correctness of the analysis than if only one approach had used.

Biography

Dr. Claude GIRAULT is a professor of Computer Science at the University Paris VI in France since 1974. He is actually in sabbatical at Rice University (cg@cs.rice.edu). His teaching, research and publication areas are distributed systems, load balancing, modeling and validation of distributed systems, Petri nets analysis tools, applications to communications, distributed data bases, cache coherence protocols, distributed shared memories. He was director of the C.N.R.S. Laboratory in methodology and architecture of computer systems, director of the Ph.D. program in computer science for the University Paris VI, chairman of the society of French teachers and researchers in computer science, vice chairman of IFIP TC 10 (Task Committee on Computer System Technology). He has been member or chirman of numerous program committees including Euromicro, Petri net conferences and steering committee,. IFIP WG 10.3, PACS. He was involved in several ESPRIT and EUREKA European contracts and is actually coordinator of 2 European research contracts.

Parasol Home | Research | People | General info | Seminars | Resources   Parasol Lab, 301 Harvey R. Bright Bldg, 3112 TAMU, College Station, TX 77843-3112  Contact Webmaster      Phone 979.458.0722     Fax 979.458.0718  Department of Computer Science and Engineering | Dwight Look College of Engineering | Texas A&M University     Privacy statement: Computer Science and Engineering Engineering TAMU