Formal Automatic Verification of Cache Coherence in Multiprocessors with Relaxed Memory Models

No abstract is available for this paper.

• Publication year

  2000

• Venue

  IEEE Trans. Parallel Distributed Syst.

• Publication date

  2000-09-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/71.879780
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs

  2016cited by this paper
• Verifying Systems with Replicated Components in Murϕ

  1999influential reference
• Retrospective: weak ordering—a new definition

  1998cited by this paper
• Verification techniques for cache coherence protocols

  1997cited by this paper
• TreadMarks: shared memory computing on networks of workstations

  1996cited by this paper
• Formal verification of delayed consistency protocols

  1996cited by this paper
• Verifying Systems with Replicated Components in Murphi

  1996cited by this paper
• Symbolic state model: a new approach for the verification of cache coherence protocols

  1996influential reference
• Using Write Caches to Improve Performance of Cache Coherence Protocols in Shared-Memory Multiprocessors

  1995cited by this paper
• A New Approach for the Verification of Cache Coherence Protocols

  1995influential reference
• Verifying Distributed Directory-Based Cahce Coherence Protocols: S3.mp, a Case Study

  1995cited by this paper
• Performance optimizations, implementation, and verification of the SGI Challenge multiprocessor

  1994cited by this paper
• A Unified Formalization of Four Shared-Memory Models

  1993influential reference
• Better Verification Through Symmetry

  1993cited by this paper
• The Detection And Elimination Of Useless Misses In Multiprocessors

  1993cited by this paper
• Abstract Interpretation Frameworks

  1992cited by this paper
• Model checking and abstraction

  1992cited by this paper
• A Formal Specification and Verification Technique for Cache Coherence Protocols

  1992cited by this paper
• Delayed consistency and its effects on the miss rate of parallel programs

  1991cited by this paper
• Memory consistency and event ordering in scalable shared-memory multiprocessors

  1990cited by this paper
• Algorithms for automated protocol verification

  1990cited by this paper
• Weak ordering-a new definition

  1990cited by this paper
• Reasoning about Networks with Many Identical Finite State Processes

  1989cited by this paper
• Hierarchical correctness proofs for distributed algorithms

  1987cited by this paper
• A class of compatible cache consistency protocols and their support by the IEEE futurebus

  1986cited by this paper
• Reasoning about networks with many identical finite-state processes

  1986cited by this paper
• Cache coherence protocols: evaluation using a multiprocessor simulation model

  1986cited by this paper
• Memory access buffering in multiprocessors

  1986cited by this paper
• A New Solution to Coherence Problems in Multicache Systems

  1978cited by this paper

• An NMOS transistor-based high-gain operational amplifier designed in 0.25-micron CMOS technology

  2023cites this paper
• D-wash - A dynamic workload aware adaptive cache coherance protocol for multi-core processor system

  2022cites this paper
• Verification of a lazy cache coherence protocol against a weak memory model

  2017cites this paper
• Cache coherency controller verification IP using SystemVerilog Assertions (SVA) and Universal Verification Methodologies (UVM)

  2017cites this paper
• McVerSi: A test generation framework for fast memory consistency verification in simulation

  2016cites this paper
• Définition et utilisation de traces issues de plateformes virtuelles pour le débogage des MPSoCs

  2016cites this paper
• Memory consistency directed cache coherence protocols for scalable multiprocessors

  2016cites this paper
• Analyse de la consistance mémoire dans les MPSoCs à l'aide du prototypage virtuel

  2013cites this paper
• Formal verification of on-chip communication fabrics

  2013cites this paper
• Towards the formal verification of cache coherency at the architectural level

  2012cites this paper
• REVISIÓN SISTEMÁTICA A LA LITERATURA PARA DETERMINAR LOS ENFOQUES DE LA INVESTIGACIÓN EN VERIFICACIÓN FORMAL DEL SOFTWARE ** Artículo en estado de edición para envío a publicación (Julio 2011)

  2011cites this paper
• Specification-based Verification in a Distributed Shared Memory Simulation Model

  2010cites this paper
• Dynamic Verification of Memory Consistency in Cache-Coherent Multithreaded Computer Architectures

  2009cites this paper
• Automatic Non-Interference Lemmas for Parameterized Model Checking

  2008cites this paper
• Abstraction techniques for parameterized verification

  2006influential citation
• Simulation modelling of distributed-shared memory multiprocessors

  2006cites this paper
• Model checking sequential consistency and parameterized protocols

  2005cites this paper
• A Case Study On The Verification of Cache Coherence Protocols

  2004cites this paper
• Formal Verification of Distributed Systems

  2004cites this paper
• Speci cation-Based Parameter-Model Interaction: Towards a Correct Re ection of Memory Characteristics in a DSM Cluster Simulation

  2003cites this paper
• Model checking a cache coherence protocol for a Java DSM implementation

  2003cites this paper
• Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol

  2002cites this paper
• See Blockindiscussions, Blockinstats, Blockinand Blockinauthor Blockinprofiles Blockinfor Blockinthis Blockinpublication Dynamic Blockinverification Blockinof Blockinmemory Blockinconsistency Blockinin Cache-coherent Blockinmultithreaded Blockincomputer Architectures. Dynamic Verification of Memory

  year unknowncites this paper