@inproceedings{4484,
  abstract     = {In shared-memory multiprocessors sequential consistency offers a natural tradeoff between the flexibility afforded to the implementor and the complexity of the programmer’s view of the memory. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at different processors be a trace of serial memory. We develop a systematic methodology for proving sequential consistency for memory systems with three parameters —number of processors, number of memory locations, and number of data values. From the definition of sequential consistency it suffices to construct a non-interfering observer that watches and reorders read/write events so that a trace of serial memory is obtained. While in general such an observer must be unbounded even for fixed values of the parameters —checking sequential consistency is undecidable!— we show that for two paradigmatic protocol classes—lazy caching and snoopy cache coherence—there exist finite-state observers. In these cases, sequential consistency for fixed parameter values can thus be checked by language inclusion between finite automata.
In order to reduce the arbitrary-parameter problem to the fixed-parameter problem, we develop a novel framework for induction over the number of processors. Classical induction schemas, which are based on process invariants that are inductive with respect to an implementation preorder that preserves the temporal sequence of events, are inadequate for our purposes, because proving sequential consistency requires the reordering of events. Hence we introduce merge invariants, which permit certain reorderings of read/write events. We show that under certain reasonable assumptions about the memory system, it is possible to conclude sequential consistency for any number of processors, memory locations, and data values by model checking two finite-state lemmas about process and merge invariants: they involve two processors each accessing a maximum of three locations, where each location stores at most two data values. For both lazy caching and snoopy cache coherence we are able to discharge the two lemmas using the model checker MOCHA.},
  author       = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  booktitle    = {Proceedings of the 11th International Conference on Computer Aided Verification},
  isbn         = {9783540662020},
  location     = {Trento, Italy},
  pages        = {301 -- 315},
  publisher    = {Springer},
  title        = {{Verifying sequential consistency on shared-memory multiprocessor systems}},
  doi          = {10.1007/3-540-48683-6_27},
  volume       = {1633},
  year         = {1999},
}

@inproceedings{4487,
  abstract     = {Refinement checking is used to verify implementations against more abstract specifications. Assume-guarantee reasoning is used to decompose refinement proofs in order to avoid state-space explosion. In previous approaches, specifications are forced to operate on the same time scale as the implementation. This may lead to unnatural specifications and inefficiencies in verification. We introduce a novel methodology for decomposing refinement proofs of temporally abstract specifications, which specify implementation requirements only at certain sampling instances in time. Our new assume-guarantee rule allows separate refinement maps for specifying functionality and timing.We present the theory for the correctness of our methodology, and illustrate it using a simple example. Support for sampling and the generalized assume-guarantee rule have been implemented in the model checker Mocha and successfully applied to verify the VGI multiprocessor dataflow chip with 6 million transistors.},
  author       = {Henzinger, Thomas A and Qadeer, Shaz and Rajamani, Sriram},
  booktitle    = {Proceedings of the 11th International Conference on Computer Aided Verification},
  isbn         = {9783540662020},
  location     = {Trento, Italy},
  pages        = {208 -- 221},
  publisher    = {Springer},
  title        = {{Assume-guarantee refinement between different time scales}},
  doi          = {10.1007/3-540-48683-6_20},
  volume       = {1633},
  year         = {1999},
}