---
_id: '4484'
abstract:
- lang: eng
  text: "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.\r\nIn 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."
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Henzinger TA, Qadeer S, Rajamani S. Verifying sequential consistency on shared-memory
    multiprocessor systems. In: <i>Proceedings of the 11th International Conference
    on Computer Aided Verification</i>. Vol 1633. Springer; 1999:301-315. doi:<a href="https://doi.org/10.1007/3-540-48683-6_27">10.1007/3-540-48683-6_27</a>'
  apa: 'Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1999). Verifying sequential
    consistency on shared-memory multiprocessor systems. In <i>Proceedings of the
    11th International Conference on Computer Aided Verification</i> (Vol. 1633, pp.
    301–315). Trento, Italy: Springer. <a href="https://doi.org/10.1007/3-540-48683-6_27">https://doi.org/10.1007/3-540-48683-6_27</a>'
  chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Verifying Sequential
    Consistency on Shared-Memory Multiprocessor Systems.” In <i>Proceedings of the
    11th International Conference on Computer Aided Verification</i>, 1633:301–15.
    Springer, 1999. <a href="https://doi.org/10.1007/3-540-48683-6_27">https://doi.org/10.1007/3-540-48683-6_27</a>.
  ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Verifying sequential consistency
    on shared-memory multiprocessor systems,” in <i>Proceedings of the 11th International
    Conference on Computer Aided Verification</i>, Trento, Italy, 1999, vol. 1633,
    pp. 301–315.
  ista: 'Henzinger TA, Qadeer S, Rajamani S. 1999. Verifying sequential consistency
    on shared-memory multiprocessor systems. Proceedings of the 11th International
    Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS,
    vol. 1633, 301–315.'
  mla: Henzinger, Thomas A., et al. “Verifying Sequential Consistency on Shared-Memory
    Multiprocessor Systems.” <i>Proceedings of the 11th International Conference on
    Computer Aided Verification</i>, vol. 1633, Springer, 1999, pp. 301–15, doi:<a
    href="https://doi.org/10.1007/3-540-48683-6_27">10.1007/3-540-48683-6_27</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International
    Conference on Computer Aided Verification, Springer, 1999, pp. 301–315.
conference:
  end_date: 1999-07-10
  location: Trento, Italy
  name: 'CAV: Computer Aided Verification'
  start_date: 1999-07-06
date_created: 2018-12-11T12:09:05Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:21:11Z
day: '01'
doi: 10.1007/3-540-48683-6_27
extern: '1'
intvolume: '      1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 301 - 315
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540662020'
publication_status: published
publisher: Springer
publist_id: '244'
quality_controlled: '1'
status: public
title: Verifying sequential consistency on shared-memory multiprocessor systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...
---
_id: '4487'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Henzinger TA, Qadeer S, Rajamani S. Assume-guarantee refinement between different
    time scales. In: <i>Proceedings of the 11th International Conference on Computer
    Aided Verification</i>. Vol 1633. Springer; 1999:208-221. doi:<a href="https://doi.org/10.1007/3-540-48683-6_20">10.1007/3-540-48683-6_20</a>'
  apa: 'Henzinger, T. A., Qadeer, S., &#38; Rajamani, S. (1999). Assume-guarantee
    refinement between different time scales. In <i>Proceedings of the 11th International
    Conference on Computer Aided Verification</i> (Vol. 1633, pp. 208–221). Trento,
    Italy: Springer. <a href="https://doi.org/10.1007/3-540-48683-6_20">https://doi.org/10.1007/3-540-48683-6_20</a>'
  chicago: Henzinger, Thomas A, Shaz Qadeer, and Sriram Rajamani. “Assume-Guarantee
    Refinement between Different Time Scales.” In <i>Proceedings of the 11th International
    Conference on Computer Aided Verification</i>, 1633:208–21. Springer, 1999. <a
    href="https://doi.org/10.1007/3-540-48683-6_20">https://doi.org/10.1007/3-540-48683-6_20</a>.
  ieee: T. A. Henzinger, S. Qadeer, and S. Rajamani, “Assume-guarantee refinement
    between different time scales,” in <i>Proceedings of the 11th International Conference
    on Computer Aided Verification</i>, Trento, Italy, 1999, vol. 1633, pp. 208–221.
  ista: 'Henzinger TA, Qadeer S, Rajamani S. 1999. Assume-guarantee refinement between
    different time scales. Proceedings of the 11th International Conference on Computer
    Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 1633, 208–221.'
  mla: Henzinger, Thomas A., et al. “Assume-Guarantee Refinement between Different
    Time Scales.” <i>Proceedings of the 11th International Conference on Computer
    Aided Verification</i>, vol. 1633, Springer, 1999, pp. 208–21, doi:<a href="https://doi.org/10.1007/3-540-48683-6_20">10.1007/3-540-48683-6_20</a>.
  short: T.A. Henzinger, S. Qadeer, S. Rajamani, in:, Proceedings of the 11th International
    Conference on Computer Aided Verification, Springer, 1999, pp. 208–221.
conference:
  end_date: 1999-07-10
  location: Trento, Italy
  name: 'CAV: Computer Aided Verification'
  start_date: 1999-07-06
date_created: 2018-12-11T12:09:06Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T09:04:26Z
day: '01'
doi: 10.1007/3-540-48683-6_20
extern: '1'
intvolume: '      1633'
language:
- iso: eng
month: '01'
oa_version: None
page: 208 - 221
publication: Proceedings of the 11th International Conference on Computer Aided Verification
publication_identifier:
  isbn:
  - '9783540662020'
publication_status: published
publisher: Springer
publist_id: '243'
quality_controlled: '1'
status: public
title: Assume-guarantee refinement between different time scales
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 1633
year: '1999'
...