Daniel Lustig

Simon Cooksey

Olivier Giroux

Proceedings of the ISCA '22: The 49th Annual International Symposium on Computer Architecture, New York, New York, USA, June 18, 2022

2021

GPS: A Global Publish-Subscribe Model for Multi-GPU Memory Management.

[BibT_eX]

[DOI]

Proceedings of the MICRO '21: 54th Annual IEEE/ACM International Symposium on Microarchitecture, 2021

Efficient Multi-GPU Shared Memory via Automatic Optimization of Fine-Grained Transfers.

[BibT_eX]

[DOI]

Proceedings of the 48th ACM/IEEE Annual International Symposium on Computer Architecture, 2021

Need for Speed: Experiences Building a Trustworthy System-Level GPU Simulator.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Symposium on High-Performance Computer Architecture, 2021

2020

RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification.

[BibT_eX]

[DOI]

Yatin A. Manerkar

CoRR, 2020

HMG: Extending Cache Coherence Protocols Across Modern Hierarchical Multi-GPU Systems.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Symposium on High Performance Computer Architecture, 2020

2019

Security Verification via Automatic Hardware-Aware Exploit Synthesis: The CheckMate Approach.

[BibT_eX]

[DOI]

Caroline Trippel

IEEE Micro, 2019

Translation ranger: operating system support for contiguity-aware TLBs.

[BibT_eX]

[DOI]

Zi Yan

David W. Nellans

Proceedings of the 46th International Symposium on Computer Architecture, 2019

Nimble Page Management for Tiered Memory Systems.

[BibT_eX]

[DOI]

Zi Yan

David W. Nellans

Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, 2019

A Formal Analysis of the NVIDIA PTX Memory Consistency Model.

[BibT_eX]

[DOI]

Sameer Sahasrabuddhe

Olivier Giroux

Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, 2019

2018

Full-Stack Memory Model Verification with TriCheck.

[BibT_eX]

[DOI]

IEEE Micro, 2018

MeltdownPrime and SpectrePrime: Automatically-Synthesized Attacks Exploiting Invalidation-Based Coherence Protocols.

[BibT_eX]

[DOI]

Caroline Trippel

CoRR, 2018

CheckMate: Automated Synthesis of Hardware Exploits and Security Litmus Tests.

[BibT_eX]

[DOI]

Caroline Trippel

Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture, 2018

PipeProof: Automated Memory Consistency Proofs for Microarchitectural Specifications.

[BibT_eX]

[DOI]

Proceedings of the 51st Annual IEEE/ACM International Symposium on Microarchitecture, 2018

2017

Architectural and Operating System Support for Virtual Memory

[BibT_eX]

[DOI]

Synthesis Lectures on Computer Architecture, Morgan & Claypool Publishers, ISBN: 978-3-031-01757-5, 2017

Transistency Models: Memory Ordering at the Hardware-OS Interface.

[BibT_eX]

[DOI]

Geet Sethi

Muralidaran Vijayaraghavan

IEEE Micro, 2017

Weak Memory Models with Matching Axiomatic and Operational Definitions.

[BibT_eX]

[DOI]

Sizhuo Zhang

Dan Lustig

Arvind

CoRR, 2017

RTLcheck: verifying the memory consistency of RTL designs.

[BibT_eX]

[DOI]

Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture, 2017

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA.

[BibT_eX]

[DOI]

Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, 2017

Automated Synthesis of Comprehensive Memory Model Litmus Test Suites.

[BibT_eX]

[DOI]

Alexandros Papakonstantinou

Andrew Wright

Olivier Giroux

Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, 2017

2016

Exploring the Trisection of Software, Hardware, and ISA in Memory Model Design.

[BibT_eX]

[DOI]

CoRR, 2016

Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings.

[BibT_eX]

[DOI]

CoRR, 2016

COATCheck: Verifying Memory Ordering at the Hardware-OS Interface.

[BibT_eX]

[DOI]

Geet Sethi

Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015

Specifying, Verifying, and Translating Between Memory Consistency Models

[BibT_eX]

[DOI]

PhD thesis, 2015

Efficient Control and Communication Paradigms for Coarse-Grained Spatial Architectures.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2015

Verifying Correct Microarchitectural Enforcement of Memory Consistency Models.

[BibT_eX]

[DOI]

Michael Pellauer

IEEE Micro, 2015

CCICheck: using µhb graphs to verify the coherence-consistency interface.

[BibT_eX]

[DOI]

Proceedings of the 48th International Symposium on Microarchitecture, 2015

ArMOR: defending against memory consistency model mismatches in heterogeneous architectures.

[BibT_eX]

[DOI]

Proceedings of the 42nd Annual International Symposium on Computer Architecture, 2015

2014

Efficient Spatial Processing Element Control via Triggered Instructions.

[BibT_eX]

[DOI]

IEEE Micro, 2014

Pipe Check: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models.

[BibT_eX]

[DOI]

Michael Pellauer

Proceedings of the 47th Annual IEEE/ACM International Symposium on Microarchitecture, 2014

2013

TLB Improvements for Chip Multiprocessors: Inter-Core Cooperative Prefetchers and Shared Last-Level TLBs.

[BibT_eX]

[DOI]

ACM Trans. Archit. Code Optim., 2013

Triggered instructions: a control paradigm for spatially-programmed architectures.

[BibT_eX]

[DOI]

Proceedings of the 40th Annual International Symposium on Computer Architecture, 2013

Reducing GPU offload latency via fine-grained CPU-GPU synchronization.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE International Symposium on High Performance Computer Architecture, 2013

2011

Shared last-level TLBs for chip multiprocessors.

[BibT_eX]

[DOI]