Model checking sequential consistency and parameterized protocols
department or school: Science, Faculty of
department or school: Computer Science, Department of
data provider: DSpace
degree campus: UBCV
creator: Bingham, Jesse
issued: 2009-12-24T00:00:21Z
issued: 2005
related degree: Doctor of Philosophy - PhD
degree grantor: University of British Columbia
description: Perhaps the most difficult aspect of designing a shared memory multiprocessor is the hardware protocol that facilitates the sharing of memory by multiple processors; these protocols are thus a natural target for formal verification. In this thesis we consider several problems relevant to model checking these protocols. The ultimate specification of a protocol is the memory model. Our more theoretical contributions relate to the problem of model checking a protocol for the well-known memory model sequential consistency (SC). We define a restricted version of SC called decisive SC (DSC), which rules out pathologies admitted by SC, and explore the complexities of its verification problems. Our key results are that DSC of a single behavior is NP-complete, DSC of a protocol is PSPACE-hard, a bounded variant DSQ is decidable in EXPSPACE, and full SC remains undecidable even when we require protocol behaviors to be prefix-closed. Also, we show that SC in conjunction with the ubiquitous property data independence imply DSC, which is strong evidence that restricting attention to DSC will never preclude any real protocol. Our second area of contribution considers parameterized model checking (PMC) of protocols. Here the goal is algorithmic proof over all of the infinite configurations of a protocol family parameterized by one or more quantities. We develop a technique to automatically abstract a family parameterized by the number of addresses and the number of data values, such that (a subset of) SC of the abstraction implies that of the family. We apply this method successfully to two nontrivial protocols, and suggest user-assisted solutions if the abstraction blows up or is too coarse for successful verification. We also contribute an approach for sound and complete processor-PMC of state assertions. The approach uses BDD-based symbolic model checking, and harnesses the theory of well-structured transition systems (WSTS). WSTS disallow conjunctive guards, which are found in…
aggregated CHO: https://circle.library.ubc.ca/rest/handle/2429/17340
note: Model Checking Sequential Consistency and Parameterized Protocols by Jesse Bingham B.Sc. University of Victoria, 1998 M.Sc . University of Victoria, 2001 A T H E S I S S U B M I T T E D IN P A R T I A L F U L F I L L M E N T O F T H E R E Q U I R E M E N T S F O R T H E D E G R E E O F Doctor of Philosophy in T H E F A C U L T Y O F G R A D U A T E S T U D I E S (Computer Science) The University of British Columbia August 2005 © Jesse Bingham, 2005 Abstract Perhaps the most difficult aspect of designing a shared memory multiprocessor is the hardware protocol that facilitates the sharing of memory by multiple processors; these protocols are thus a natural target for formal verification. In this thesis we consider several problems relevant to model checking these protocols. The ultimate specification of a protocol is the memory model. Our more theoretical contributions relate to the problem of model checking a protocol for the well-known memory model sequential consistency (SC). We define a restricted version of S C called decisive SC (DSC), which rules out pathologies admitted by S C , and explore the complexities of its verification problems. Our key results are that D S C of a single behavior is NP-complete, D S C of a protocol is PSPACE-hard, a bounded variant D S Q is decidable in E X P S P A C E , and full S C remains undecidable even when we require protocol behaviors to be prefix-closed. Also, we show that S C in conjunction with the ubiquitous property data independence imply D S C , which is strong evidence that restricting attention to D S C will never preclude any real protocol. Our second area of contribution considers parameterized model checking (PMC) of protocols. Here the goal is algorithmic proof over all of the infinite configurations of a protocol family pa-rameterized by one or more quantities. We develop a technique to automatically abstract a family parameterized by the number of addresses and the number of data values, such that (a subset of) S…
has type: Thesis/Dissertation
date issued: 2005-11
is shown at: 10.14288/1.0051397
language: eng
degree discipline: Computer Science
provider: Vancouver : University of British Columbia Library
publisher: University of British Columbia
rights: For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
scholar level: Graduate
type: Text
identifier URI: http://hdl.handle.net/2429/17340