Pith. sign in

REVIEW 3 major objections 4 minor 39 references

Automated Synthesis of Heterogeneous, Hierarchical, Scoped Coherence Protocols

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read ShimGen automatically synthesizes shim logic that lets heterogeneous, hierarchical cache-coherence protocols—including non-SWMR and scoped ones—interoperate through a global protocol, and verifies that the resulting system enforces…

desk verdict ShimGen's shim API and the APU consistency bug are real advances, but the 'verified correct' claim rests on unpublished abstractions; send it to review on the condition that the artifacts and abstraction definitions ship. read the letter →

arxiv 2608.05965 v1 pith:OCVFEGS7 submitted 2026-08-06 cs.AR

Fletch Rydell , An Qi Zhang , Nicolai Oswald , Andres Goens , Vijay Nagarajan , Daniel Sorin This is my paper · ORCID
classification cs.AR
keywords cachecoherenceprotocolsynthesisheterogeneoussystemshierarchicalprotocolsshimgenerationscopedmemoryconsistencycompoundnon-SWMR
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

ShimGen is an automated synthesis engine that takes state-machine descriptions of per-cluster cache-coherence protocols and a global interconnect protocol and produces the 'shim' logic that fuses them into one hierarchical protocol. The paper's central claim is that this generation can be made correct for systems that mix single-writer/multiple-reader (SWMR) protocols, non-SWMR GPU-style protocols, scoped accesses, and global protocols such as CXL, CHI, and Spandex, which no prior synthesis tool handled. The payoff is that architects can compose heterogeneous CPU/GPU systems without hand-writing subtle interface logic, and can exploit non-SWMR global transactions such as one-off writes that earlier tools ignored. The paper supports this claim with two case studies: a comparison with a manually designed APU protocol in which the manual shim is shown to violate release consistency while ShimGen's does not, and a streaming-write study in which using one-off global writes improves effective memory bandwidth.

What carries the argument

The load-bearing mechanism is the shim API, a semantic classification of protocol transactions into three categories—obtains, one-offs, and revokes—with parameters for permission level, data requirements, and scope, plus a 'stronger-than' partial order that tells ShimGen which global transactions can legally implement which cluster transactions. This classification decouples coherence semantics from protocol-specific messages, so ShimGen can map between protocols whose message sets share no common vocabulary. The third step, dependency-respecting parallel composition, splits transitions with dependency guards so the two controllers run concurrently while preserving the ordering needed for compound consistency; for example, a cluster operation is only performed once it is known to be necessary on all subsequent global traces, and cluster-scoped operations can be acknowledged locally while later global-scoped transactions wait for them to complete.

What would settle it

Run the synthesized GPU shim in its write-back L2 variant on the message-passing pattern from the first case study: GPU writes Data, then Flag, while the CPU holds Data in the shared state; if the CPU can observe Flag=1, Data=0, the shim has failed to enforce release consistency, contradicting the paper's correctness claim.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes that coherence-shim synthesis can be made fully general: a small semantic vocabulary—obtains (permission plus optional data), one-offs (reads, writes, or read-modify-writes done at the directory without obtaining permission), and revokes (permission recalls), each tagged with scope and data requirements—is enough to classify the transactions of both cluster and global protocols and to derive correct mappings between them. Given a cluster directory transaction, ShimGen finds every global transaction that offers at least the required coherence guarantee, picks the weakest such mapping as the default, and composes the two transactions in parallel while inserting dependency guards so that a cache never receives permission before the global protocol has granted it, data is only used when available, and a global-scoped acknowledgment waits for the global transaction to complete. The paper reports that all litmus-test variations it generated respect the protocol's compound memory consistency, and its first case study exposes a release-consistency violation in a manually designed GPU shim that the ShimGen-generated shim avoids.

Load-bearing premise

The safety guarantee depends on the unstated assumption that every hand-built simplified model of a protocol faithfully reproduces everything the real protocol can do; if a simplified model misses a possible interleaving, the verification can report success while the actual shim misbehaves.

Editorial extensions

If this is right

  • Architects can automatically turn a new global interconnect standard into a drop-in coherence layer for a heterogeneous CPU/GPU system without hand-writing or hand-verifying shims.
  • Non-SWMR and scoped features become usable in practice: mapping non-temporal stores to one-off global writes yields higher effective memory bandwidth than forcing every access through read-for-ownership, as shown in the streaming case study.
  • Synthesis can act as a correctness oracle for manual designs: the comparison with the manually designed APU GPU shim finds a release-consistency violation that the manual logic allows and ShimGen's logic prevents.
  • Scoped cluster operations can be acknowledged locally without global propagation, and correctness is preserved by making later global-scoped transactions wait for outstanding cluster-scoped ones, so scoped optimizations do not silently break consistency.
  • Because compound consistency is compositional, a system built from ShimGen-shimmed clusters inherits each cluster's memory consistency model, so existing compiler mappings to those models remain valid in the composed system.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The three-category API is stated in terms of coherence functionality rather than protocol messages, so in principle it could be extended to future protocol families, though ShimGen currently excludes timestamp-ordered and update-based protocols.
  • The strength ordering defines a space of correct shims; a natural extension is to have ShimGen search that space automatically for a performance objective such as latency or invalidation traffic instead of defaulting to the weakest mapping.
  • The verification claim currently inherits the soundness of the hand-built protocol abstractions; a stronger guarantee would come from generating those abstractions mechanically from the concrete protocols or proving the refinement relation, rather than asserting it.
  • If ShimGen sees wider adoption, the practice of writing shims by hand could shift to generating candidate shims and then optimizing the mapping choice, exposing correctness and performance trade-offs earlier in the design cycle.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. ShimGen is a synthesis tool that takes DSL state-machine descriptions of cluster coherence protocols and a global protocol and automatically generates shim logic, producing a hierarchical protocol. The key abstraction is a shim API that classifies transactions as obtains, one-offs, and revokes, parameterized by permission level, data requirements, and scope. The synthesized shims are emitted as Murphi models for model checking and as SLICC code for gem5. The paper claims two main results: (1) for the AMD APU case study, ShimGen's output is essentially equivalent to the manually designed gem5 protocol but avoids a release-consistency violation in the GPU VIPER cluster; (2) for a multi-cluster CXL system, mapping non-temporal stores to global one-off writes (WrInv) improves effective memory bandwidth on streaming workloads compared with a read-for-ownership mapping. Verification is performed by exhaustive Murphi model checking of litmus-test variants on abstracted systems, where the abstractions are said to preserve all observable behaviors of the concrete protocols.

Significance. If the verification claim can be made auditable, this is a significant advance: it is the first synthesis tool in this line of work to support non-SWMR and scoped global protocols such as CXL, CHI, and Spandex, and the shim API is a genuinely useful semantic decomposition. The APU comparison is a strong, concrete case study, and the claimed bug in the manual gem5 protocol is independently checkable. The performance study is a clean demonstration that one-off global transactions can matter, and the tool's ability to emit both Murphi and SLICC is a practical strength. However, the central correctness claim rests on Section 7's compositional abstraction verification, and the abstractions are neither specified nor shipped, so the machine-checked evidence cannot currently be audited or reproduced from the manuscript alone.

major comments (3)
  1. [Section 7, 'Compositional abstraction technique' and preceding paragraph] The load-bearing correctness claim depends on hand-crafted abstractions that are asserted to preserve all behavior of each cluster protocol, global protocol, and shim, but these abstractions are not specified anywhere in the paper and no artifact is provided. The text states that 'we verify with Murphi that each protocol in a system refines its abstraction' and that this guarantees safety for the generated protocol, but without the abstraction definitions, the refinement maps, the generated Murphi models, or the abstraction-composition scripts, the reader cannot check that every reachable transient interleaving of the concrete protocol is represented. A concrete failure mode would be an abstraction omitting a one-off write in flight concurrently with a global upgrade or revoke, or a proxy-cache downgrade interleaved with a global WritePull; in such a case the abstracted litmus checks could pass while the concrete synthesized protocol violates compound consistency. This is not a presentation nit: the paper's headline claim is that ShimGen produces verifiably correct hierarchical protocols, and the verification evidence is currently an unverifiable assertion.
  2. [Section 7, formal citation of compositional results] The paper justifies the abstraction-composition step by citing Theorem 7.4 of [32] and Corollary 7.68 of [6], which concern simulation relations over composition and preservation of safety properties. However, ShimGen's fused controllers are generated using dependency guards dep(De), cross-controller data dependencies, proxy-cache transactions, and revoke transitions inserted into transient states (Sections 4.4.3 and 4.4.4). The paper does not show that this specific generated composition is an instance of the handshaking composition for which the cited theorems hold. Without such a verification of the theorem hypotheses, the move from 'each protocol refines its abstraction' to 'the composed abstracted system covers all concrete executions' is an assertion, not an established step.
  3. [Section 7, litmus-test verification scope] The model checking verifies a finite set of litmus-test variants (7 tests, 52–444 variants per system) on the abstracted systems, but the text concludes that 'our constructed protocols respect their compound MCMs, never violating safety.' Litmus-test coverage, while standard practice, does not by itself establish that a protocol enforces the full compound memory model for all executions; it only rules out the specific forbidden outcomes encoded in those tests. The abstract and Section 7 should state this scope limitation explicitly rather than implying a full MCM correctness proof, or the paper should provide the complete set of MCM axioms and a proof that the litmus set is complete for the protocols under consideration.
minor comments (4)
  1. [Section 5.4, Figure 5] The performance comparison reports runtimes ranging from 0.90% slower to 1.04% faster than the manual protocol, with an average 0.13% improvement, but no run-to-run variance or methodology details are given. Since gem5 syscall emulation is likely deterministic, this may be acceptable, but the paper should say so explicitly and specify how many repetitions, if any, were used.
  2. [Section 3.2 and Section 7] The paper mentions outputting the generated protocol in 'the same input DSL, the Murphi model checking language, and the SLICC DSL,' and the verification depends on the Murphi models, but no artifact or repository URL is provided. Providing the generated models and refinement scripts would substantially strengthen reproducibility.
  3. [Section 4.3, Algorithm 2] In Algorithm 2, the notation in the one-off write case (line 11) uses a variable d that is bound in an existential but then appears inside the Obtain pattern; clarifying this notation would help readers understand the strength ordering.
  4. [Section 5.3, GPU VIPER discussion] The paper says the manually designed L2 controller 'transitions directly to M on a write in write-back mode without obtaining permission globally,' and then gives a litmus test. It would be useful to state whether this is the write-back mode only, since the write-through mode appears to issue WriteThrough globally, and to clarify the exact configuration in which the bug manifests.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: synthesis and litmus-based verification do not reduce to their inputs; the unspecified abstractions and self-cited correctness formalization are auditability concerns, not circular steps.

full rationale

The paper's claimed derivation chain is not circular. ShimGen takes separate FSM specifications of cluster and global protocols as inputs (Section 3.1) and produces shim FSMs by the three-step method of Section 4: classifying transactions with Algorithm 1, selecting stronger-or-equal global transactions with Algorithm 2, and fusing them with dependency guards (Section 4.4). None of these steps assumes the conclusion that the resulting protocol enforces compound consistency; that property is checked independently in Section 7 by Murphi litmus model checking, using the LOST-POP formalization [16] as an oracle for forbidden outcomes. The self-citation to [16] is a definitional dependency shared with the field, not a by-construction reduction, and the APU comparison and STREAM evaluation use external gem5 baselines. The main caveats are that the compound-consistency formalization [16] has overlapping authors and that the hand-crafted abstractions in Section 7 ('we develop an abstraction which preserves the behavior of the original protocol and shim') are not specified or shipped, so the exhaustive-verification claim is not independently auditable from the manuscript. This is a support/reproducibility gap rather than a circularity: no parameter is fitted and then renamed a prediction, and no equation is defined in terms of the target result.

Assumptions & free parameters 4 free parameters · 6 assumptions · 1 invented entities

The central claim depends on several hand-made modeling and verification choices: hand-crafted abstractions, user-supplied scope and consistency labels, and a finite litmus-test suite. No numeric constants are fitted to data, but these non-numeric choices play the same role as free parameters in supporting the verification.

free parameters (4)
  • Hand-crafted abstraction maps for model checking = custom per protocol, not published
    Section 7 says abstractions 'preserve the behavior' but they are not specified; verification soundness depends on them.
  • User-supplied scope labels = per-access labels
    Section 3.1 requires users to label cluster-scoped accesses; classification of one-offs depends on these labels.
  • User-supplied consistency mappings (ArMOR) = per-protocol translations
    Section 3.1 requires translations for weakly-ordered global protocols; these determine how one-off accesses are ordered.
  • Litmus test set = 7 tests, 52-444 variants per system
    Verification covers only the selected litmus tests; choice of tests is hand-made.
assumptions (6)
  • domain assumption Each protocol can be modeled as a finite state machine with a directory controller.
    Section 3.3 limits ShimGen to directory-based protocols without timestamps or update-based schemes.
  • domain assumption Compound consistency is the correct correctness criterion for heterogeneous systems.
    Section 1 and Section 7 rely on [16], a paper by overlapping authors; the APU bug finding is judged against this criterion.
  • ad hoc to paper Hand-crafted abstractions preserve all observable behaviors of the concrete protocols.
    Section 7 introduces abstractions without giving them; unsound abstractions would invalidate the model checking results.
  • domain assumption The seven common litmus tests cover the MCM behaviors relevant to compound consistency.
    Section 7 uses MP, Dekkers, IRIW, RWC, WRC, ISA2, CoWR; this is standard practice but not a completeness proof.
  • standard math Simulation relations factor over the handshaking composition and preserve safety properties.
    Section 7 cites Park [32] and Baier and Katoen [6]; standard theorem, but requires the abstraction to be a simulation.
  • domain assumption User-provided ArMOR mappings correctly capture consistency semantics of weak accesses.
    Section 3.1 defers ordering guarantees to user-supplied translations; if these are wrong, generated shims may be wrong.
invented entities (1)
  • shim API transaction classes (obtains, one-offs, revokes)
    purpose: Abstract classification that lets ShimGen map cluster transactions to global transactions with equal or stronger guarantees.
    A new taxonomy introduced in Section 4.2; it has no independent falsifiable handle outside this paper, but it is the core abstraction making synthesis possible.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Automated Synthesis of Heterogeneous, Hierarchical, Scoped Coherence Protocols." pith.science (2026). https://pith.science/paper/OCVFEGS7

@misc{pith2026260805965,
  author       = {Pith},
  title        = {Pith review of: Automated Synthesis of Heterogeneous, Hierarchical, Scoped Coherence Protocols},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OCVFEGS7}},
  note         = {Machine review of arXiv:2608.05965}
}
read the original abstract

Processor design is converging on a new model of cache-coherent shared memory characterized by heterogeneity, hierarchy, and scopes. Protocols like CXL or AMBA CHI are used as global protocols to combine multiple clusters, each with its own cluster-level coherence protocols. Manually designing shims to interface between these cluster and global protocols is subtle and error-prone. Automatic synthesis, on the other hand, makes simplifying assumptions like the single-writer multiple-reader (SWMR) invariant, that sacrifice performance for simplicity and guaranteed correctness. We present a shim API \textemdash a generic abstraction that enables us to classify protocol transactions by their semantic coherence guarantees. Our automated synthesis engine, ShimGen, uses this shim API to automatically compose protocols with both SWMR and relaxed accesses, taking advantage of modern architectural optimizations like scoped memory accesses and lazy invalidation. We demonstrate ShimGen's efficacy on two case studies. First, we compare its output to a manually-designed hierarchical protocol for the AMD APU released in gem5. ShimGen's output is similar to the existing protocol. However, we identify one scenario where the manually-designed protocol fails to uphold compound consistency, while ShimGen's does. Second, we compare the performance of a hierarchical protocol with a global protocol that exploits non-SWMR accesses to a hierarchical protocol with a strictly SWMR global protocol. The result shows the performance benefits of accommodating global protocols with non-SWMR behavior.

Figures

Figures reproduced from arXiv: 2608.05965 by the authors.

Figure 1
Figure 1. Heterogeneous processor made of two or more clusters—with each cluster using a distinct coherence [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Comparison to prior work. Mapping every cluster transaction to obtain global SWMR permission (top) [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. ShimGen Steps, Fusing a Spandex ReqWT Transaction With a CXL Global Protocol [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Message Passing litmus test on APU Protocol [PITH_FULL_IMAGE:figures/full_fig_p016_4.png]
Figure 5
Figure 5. Figure 5: Performance of Manually-Designed and Synthesized [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

39 extracted references · 28 canonical work pages

  1. [32]

    David Michael Ritchie Park. 1981. Concurrency and Automata on Infinite Sequences. InTheoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23-25, 1981, Proceedings (Lecture Notes in Computer Science, Vol. 104), Peter Deussen (Ed.). Springer, 167–183. https://doi.org/10.1007/BFB0017309

    doi:10.1007/bfb0017309 1981

  2. [6]

    2008.Principles of model checking

    Christel Baier and Joost-Pieter Katoen. 2008.Principles of model checking. MIT Press

    2008

  3. [1]

    [n. d.]. Compute Express Link. https://www.computeexpresslink.org/. Accessed: 18th June 2021

    work page 2021

  4. [2]

    [n. d.]. The AMBA CHI Specification. https://developer.arm.com/architectures/system-architectures/amba/amba-5. Accessed: 15th July 2019

    work page 2019

  5. [3]

    Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: Running tests against hardware.Lecture Notes in Computer Science6605 LNCS (2011). https://doi.org/10.1007/978-3-642-19835-9_5

    work page doi:10.1007/978-3-642-19835-9_5 2011

  6. [4]

    Sinclair, and Sarita V

    Jonathan Alsop, Matthew D. Sinclair, and Sarita V. Adve. 2018. Spandex: A Flexible Interface for Efficient Heterogeneous Coherence. InISCA

    work page 2018

  7. [5]

    d.].ARM v-8 Architecture Reference Manual

    ARM Limited [n. d.].ARM v-8 Architecture Reference Manual. ARM Limited

    work page

  8. [7]

    Jason F Cantin, James E Smith, Mikko H Lipasti, Andreas Moshovos, and Babak Falsafi. 2006. Coarse-grain coherence tracking: RegionScout and region coherence arrays.IEEE Micro26, 1 (2006), 70–79

    work page 2006

Show all 39 references
  1. [8]

    Beckmann, Steven K

    Shuai Che, Bradford M. Beckmann, Steven K. Reinhardt, and Kevin Skadron. 2013. Pannotia: Understanding irregular GPGPU graph applications. In2013 IEEE International Symposium on Workload Characterization (IISWC). 185–195. https://doi.org/10.1109/IISWC.2013.6704684

    2013

  2. [9]

    B. Choi, R. Komuravelli, H. Sung, R. Smolinski, N. Honarmand, S. V. Adve, V. S. Adve, N. P. Carter, and Ching-Tsun Chou

  3. [10]

    Clarke, D.E

    E.M. Clarke, D.E. Long, and K.L. McMillan. 1989. Compositional model checking. In[1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science. 353–362. https://doi.org/10.1109/LICS.1989.39190

    1989

  4. [11]

    Clarke, Orna Grumberg, and David E

    Edmund M. Clarke, Orna Grumberg, and David E. Long. 1992. Model Checking and Abstraction. InConference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Albuquerque, New Mexico, USA, January 19-22, 1992, Ravi Sethi (Ed.). ACM ...

    1992

  5. [12]

    Rachel Cleaveland and Caroline Tripperl. 2024. Memory Consistency Model-Aware Cache Coherence for Heteroge- neous Hardware. InProceedings of Formal Methods in Computer-Aided Design

    2024

  6. [13]

    Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. InConference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, Californ...

    1977

  7. [14]

    David L Dill. 1996. The Murphi Verification System. InCA V, Vol. 1102

    1996

  8. [15]

    Ferenbaugh

    Charles R. Ferenbaugh. 2015. PENNANT: an unstructured mesh mini-app for advanced architecture research.Concur- rency and Computation: Practice and Experience27, 17 (2015), 4555–4572. https://doi.org/10.1002/cpe.3422

    2015 doi

  9. [16]

    Andrés Goens, Soham Chakraborty, Susmit Sarkar, Sukarn Agarwal, Nicolai Oswald, and Vijay Nagarajan. 2023. Compound Memory Models.Proc. ACM Program. Lang.7, PLDI (2023), 1145–1168. https://doi.org/10.1145/3591267

    2023 doi

  10. [17]

    Leiserson

    Edya Ladan-Mozes and Charles E. Leiserson. 2008. A consistency architecture for hierarchical shared caches. In Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures. 11–22

    2008

  11. [18]

    Anatole Lefort, Julian Pritzi, Nicolò Carpentieri, David Schall, Simon Dittrich, Soham Chakraborty, Nicolai Oswald, and Pramod Bhatotia. 2026. vCXLGen: Automated Synthesis and Verification of CXL Bridges for Heterogeneous Architectures. InProceedings of the 31st ACM Internatio...

    2026

  12. [19]

    Anatole Lefort, David Schall, Nicolo Carpentieri, Julian Pritzi, Soham Chakraborty, Nicolai Oswald, and Pramod Bhatotia. 2026. C3: CXL Coherence Controllers for Heterogeneous Architectures . In2026 IEEE International Symposium on High Performance Computer Architecture (HPCA)

    2026

  13. [20]

    Jason Lowe-Power, Abdul Mutaal Ahmad, Ayaz Akram, Mohammad Alian, Rico Amslinger, Matteo Andreozzi, Adrià Armejach, Nils Asmussen, Srikant Bharadwaj, Gabe Black, Gedare Bloom, Bobby R. Bruce, Daniel Rodrigues Carvalho, Jerónimo Castrillón, Lizhong Chen, Nicolas Derumigny, Step...

    2020 arXiv

  14. [21]

    Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi. 2015. ArMOR: Defending Against Memory Consistency Model Mismatches in Heterogeneous Architectures. InProceedings of the International Symposium on Computer Architecture

    2015

  15. [22]

    Sela Mador-Haim, Rajeev Alur, and Milo M. K. Martin. 2010. Generating Litmus Tests for Contrasting Memory Consistency Models. InProceedings of the 22nd International Conference on Computer Aided Verification

    2010

  16. [23]

    Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi

    Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. 2015. CCICheck: using𝜇hb graphs to verify the coherence-consistency interface. InProceedings of the 48th International Symposium on Microarchitecture, MICRO 2015, Waikiki, HI, USA, December 5-9, 2015, ...

    2015

  17. [24]

    Opeoluwa Matthews and Daniel J. Sorin. 2017. Architecting Hierarchical Coherence Protocols for Push-button Parametric Verification. InProceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture. 477–489

    2017

  18. [25]

    McCalpin

    John D. McCalpin. 1995. Memory Bandwidth and Machine Balance in Current High Performance Computers.IEEE Computer Society Technical Committee on Computer Architecture (TCCA) Newsletter(Dec. 1995), 19–25

    1995

  19. [26]

    McMillan

    Kenneth L. McMillan. 2001. Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking. InCorrect Hardware Design and Verification Methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, Septe...

    2001 doi

  20. [27]

    Sorin, Mark D

    Vijay Nagarajan, Daniel J. Sorin, Mark D. Hill, and David A. Wood. 2020.A Primer on Memory Consistency and Cache Coherence(2 ed.). Morgan & Claypool Publishers

    2020

  21. [28]

    Olson, Mark D

    Lena E. Olson, Mark D. Hill, and David A. Wood. 2017. Crossing Guard: Mediating Host-Accelerator Coherence Interactions. InASPLOS. 163–176

    2017

  22. [29]

    Nicolai Oswald, Vijay Nagarajan, and Daniel J. Sorin. 2018. ProtoGen: Automatically Generating Directory Cache Coherence Protocols from Atomic Specifications. InISCA

    2018

  23. [30]

    Nicolai Oswald, Vijay Nagarajan, and Daniel J. Sorin. 2020. HieraGen: Automated Generation of Concurrent, Hierar- chical Cache Coherence Protocols. InProcedings of the 47th Annual International Symposium on Computer Architecture

    2020

  24. [31]

    Sorin, Vasilis Gavrielatos, Theo Olausson, and Reece Carr

    Nicolai Oswald, Vijay Nagarajan, Daniel J. Sorin, Vasilis Gavrielatos, Theo Olausson, and Reece Carr. 2022. HeteroGen: Automatic Synthesis of Heterogeneous Cache Coherence Protocols. In2022 IEEE International Symposium on High- Performance Computer Architecture (HPCA). 756–771

    2022

  25. [33]

    Xiaowei Ren, Daniel Lustig, Evgeny Bolotin, Aamer Jaleel, Oreste Villa, and David Nellans. 2020. HMG: Extending Cache Coherence Protocols Across Modern Hierarchical Multi-GPU Systems. In2020 IEEE International Symposium on High Performance Computer Architecture (HPCA)

    2020

  26. [34]

    Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors.Commun. ACM53, 7 (2010), 89–97. https: //doi.org/10.1145/1785414.1785443

    2010

  27. [35]

    Sinclair, Johnathan Alsop, and Sarita V

    Matthew D. Sinclair, Johnathan Alsop, and Sarita V. Adve. 2015. Efficient GPU Synchronization without Scopes: Saying No to Complex Consistency Models. InProceedings of the 48th International Symposium on Microarchitecture. 647–659

    2015

  28. [36]

    Sinclair, Johnathan Alsop, and Sarita V

    Matthew D. Sinclair, Johnathan Alsop, and Sarita V. Adve. 2017. HeteroSync: A benchmark suite for fine-grained synchronization on tightly coupled GPUs. In2017 IEEE International Symposium on Workload Characterization (IISWC). 239–249. https://doi.org/10.1109/IISWC.2017.8167781

    2017

  29. [37]

    2014.The RISC-V Instruction Set Manual, Volume I: Base user-level ISA

    Andrew Waterman, Yunsup Lee, David A Patterson, and Krste Asanovic. 2014.The RISC-V Instruction Set Manual, Volume I: Base user-level ISA

    2014

  30. [38]

    Lebeck, and Daniel J

    Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. 2010. Fractal Coherence: Scalably Verifiable Cache Coherence. In MICRO. 471–482

    2010

  31. [2011]

    InProceedings of the 20th International Conference on Parallel Architectures and Compilation Techniques

    DeNovo: Rethinking the Memory Hierarchy for Disciplined Parallelism. InProceedings of the 20th International Conference on Parallel Architectures and Compilation Techniques

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.