research-article

Public Access

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

Authors:

Caroline Trippel,

Yatin A. Manerkar,

Michael Pellauer,

Margaret MartonosiAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 45, Issue 1

Pages 119 - 133

https://doi.org/10.1145/3093337.3037719

Published: 04 April 2017 Publication History

Abstract

Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardware-software stack, requiring thoroughly verified specifications, compilers, and implementations at the interfaces between layers. Current verification techniques evaluate segments of the system stack in isolation, such as proving compiler mappings from a high-level language (HLL) to an ISA or proving validity of a microarchitectural implementation of an ISA.

This paper makes a case for full-stack MCM verification and provides a toolflow, TriCheck, capable of verifying that the HLL, compiler, ISA, and implementation collectively uphold MCM requirements. The work showcases TriCheck's ability to evaluate a proposed ISA MCM in order to ensure that each layer and each mapping is correct and complete. Specifically, we apply TriCheck to the open source RISC-V ISA [55], seeking to verify accurate, efficient, and legal compilations from C11. We uncover under-specifications and potential inefficiencies in the current RISC-V ISA documentation and identify possible solutions for each. As an example, we find that a RISC-V-compliant microarchitecture allows 144 outcomes forbidden by C11 to be observed out of 1,701 litmus tests examined. Overall, this paper demonstrates the necessity of full-stack verification for detecting MCM-related bugs in the hardware-software stack.

References

[1]

Sarita Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, 29(12):66--76, 1996.

Digital Library

[2]

Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems (TOPLAS), 36(2):7:1--7:74, July 2014.

[3]

ARM. ARM Cortex-A9 technical reference manual ARMv7-A, 2008--2012. http://infocenter.arm.com/help/topic/com.arm.doc.ddi0388i/DDI0388I_cortex_a9_r4p1_trm.pdf.

[4]

ARM. Cortex-A9 MPCore, programmer advice notice, read-after-read hazards. ARM Reference 761319., 2011. http://infocenter.arm.com/help/topic/com.arm.doc.uan0004a/UAN0004A_a9_read_read.pdf.

[5]

Krste Asanovic, Rimas Avizienis, Jonathan Bachrach, Scott Beamer, David Biancolin, Christopher Celio, Henry Cook, Daniel Dabbelt, John Hauser, Adam Izraelevitz, Sagar Karandikar, Ben Keller, Donggyu Kim, John Koenig, Yunsup Lee, Eric Love, Martin Maas, Albert Magyar, Howard Mao, Miquel Moreto, Albert Ou, David A. Patterson, Brian Richards, Colin Schmidt, Stephen Twigg, Huy Vo, and Andrew Waterman. The Rocket Chip generator. Technical Report UCB/EECS-2016-17, EECS Department, University of California, Berkeley, Apr 2016.

[6]

Mark Batty, Alastair F. Donaldson, and John Wickerson. Overhauling SC atomics in C11 and OpenCL. In 43rd Annual Symposium on Principles of Programming Languages (POPL), 2016.

Digital Library

[7]

Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. The problem of programming language concurrency semantics. In 24th European Symposium on Programming (ESOP), part of the European Joint Conferences on Theory and Practice of Software (ETAPS), 2015.

[8]

Mark Batty, Kayvan Memarian, Scott Owens, Susmit Sarkar, and Peter Sewell. Clarifying and compiling C/C++ concurrency: From C++11 to POWER. In 39th Annual Symposium on Principles of Programming Languages (POPL), 2012.

Digital Library

[9]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. Mathematizing C++concurrency. In 38th Annual Symposium on Principles of Programming Languages (POPL), 2011.

Digital Library

[10]

Colin Blundell, Milo M.K. Martin, and Thomas F. Wenisch. InvisiFence: Performance-transparent memory ordering in conventional multiprocessors. In 36th Annual International Symposium on Computer Architecture (ISCA), 2009.

Digital Library

[11]

Hans-J. Boehm. Threads cannot be implemented as a library. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '05, pages 261--268, New York, NY, USA, 2005. ACM.

Digital Library

[12]

Hans-J. Boehm and Sarita V. Adve. Foundations of the C++concurrency memory model. In 29th Conference on Programming Language Design and Implementation (PLDI), 2008.

[13]

Luis Ceze, James Tuck, Pablo Montesinos, and Josep Torrellas. BulkSC: Bulk enforcement of sequential consistency. In 34th Annual International Symposium on Computer Architecture (ISCA), 2007.

Digital Library

[14]

William W. Collier. Reasoning About Parallel Architectures. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1992.

Digital Library

[15]

M. Elver and V. Nagarajan. TSO-CC: Consistency directed cache coherence for TSO. In 20th International Symposium on High Performance Computer Architecture (HPCA), 2014.

[16]

Kourosh Gharachorloo. Memory Consistency Models for Shared-memory Multiprocessors. PhD thesis, Stanford University, Stanford, CA, USA, 1996.

Digital Library

[17]

Kourosh Gharachorloo, Daniel Lenoski, James Laudon, Phillip Gibbons, Anoop Gupta, and John Hennessy. Memory consistency and event ordering in scalable shared-memory multiprocessors. 17th International Symposium on Computer Architecture (ISCA), 1990.

Digital Library

[18]

Chris Gniady and Babak Falsafi. Speculative sequential consistency with little custom storage. In International Conference on Parallel Architectures and Compilation Techniques (PACT), 2002.

[19]

Chris Gniady, Babak Falsafi, and T.N. Vijaykumar. Is SC + ILP = RC? 41st International Symposium on Computer Architecture (ISCA), 1999.

Digital Library

[20]

Dibakar Gope and Mikko H. Lipasti. Atomic SC for simple in-order processors. In 20th International Symposium on High Performance Computer Architecture HPCA, 2014.

[21]

Martonosi Research Group. Check research tools and papers website, 2017. http://check.cs.princeton.edu.

[22]

Sudheendra Hangal, Durgam Vahia, Chaiyasit Manovit, and Juin-Yeu Joseph Lu. TSOtool: A program for verifying memory systems using the memory consistency model. In 31st Annual International Symposium on Computer Architecture (ISCA), 2004.

Digital Library

[23]

Derek R. Hower, Blake A. Hechtman, Bradford M. Beckmann, Benedict R. Gaster, Mark D. Hill, Steven K. Reinhardt, and David A. Wood. Heterogeneous-race-free memory models. In 19th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2014.

Digital Library

[24]

ISO/IEC. Programming Languages -- C++, 2014.

[25]

Daniel Jackson. Software Abstractions: logic, language, and analysis. MIT Press, 2012.

Digital Library

[26]

Pete Keleher, Alan L. Cox, and Willy Zwaenepoel. Lazy release consistency for software distributed shared memory. In 19th Annual International Symposium on Computer Architecture, 1992.

Digital Library

[27]

Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. MPI-SWS, Tech. rep. MPI-SWS-2016-011, 2016.

[28]

Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computing, 28(9):690--691, 1979.

Digital Library

[29]

Changhui Lin, Vijay Nagarajan, Rajiv Gupta, and Bharghava Rajaram. Efficient sequential consistency via conflict ordering. In 17th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2012.

Digital Library

[30]

Daniel Lustig, Michael Pellauer, and Margaret Martonosi. PipeCheck: Specifying and verifying microarchitectural enforcement of memory consistency models. In 47th International Symposium on Microarchitecture (MICRO), 2014.

Digital Library

[31]

Daniel Lustig, Geet Sethi, Margaret Martonosi, and Abhishek Bhattacharjee. COATCheck: Verifying Memory Ordering at the Hardware-OS Interface. In Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems, 2016.

Digital Library

[32]

Daniel Lustig, Caroline Trippel, Michael Pellauer, and Margaret Martonosi. ArMOR: Defending against memory consistency model mismatches in heterogeneous architectures. In 42nd International Symposium on Computer Architecture (ISCA), 2015.

Digital Library

[33]

Daniel Lustig, Andrew Wright, Alexandros Papakonstantinou, and Olivier Giroux. Automated synthesis of comprehensive memory model litmus test suites. 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2017.

Digital Library

[34]

Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. An axiomatic memory model for POWER multiprocessors. In 24th International Conference on Computer Aided Verification (CAV), 2012.

Digital Library

[35]

Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using μhb graphs to verify the coherence-consistency interface. In 48th International Symposium on Microarchitecture (MICRO), 2015.

Digital Library

[36]

Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and proof loophole for the C/C

[37]

to POWER and armv7 trailing-sync compiler mappings. CoRR, abs/1611.01507, 2016.

[38]

Milo M. K. Martin, Daniel J. Sorin, Harold W. Cain, Mark D. Hill, and Mikko H. Lipasti. Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing. In 34th International Symposium on Microarchitecture (MICRO), 2001.

[39]

Paul E. McKenney and Raul Silvera. Example POWER implementation for C/C++memory model, 2011. http://www.rdrop.com/users/paulmck/scalability/paper/N2745r.2011.03.04a.html.

[40]

Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. In 19th International Conference on Functional Programming (ICFP), 2014.

Digital Library

[41]

Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002.

[42]

Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2009.

Digital Library

[43]

Gustavo Petri, Jan Vitek, and Suresh Jagannathan. Cooking the books: Formalizing JMM implementation recipes. In 29th European Conference on Object-Oriented Programming (ECOOP), 2015.

[44]

Parthasarathy Ranganathan, Vijay S. Pai, and Sarita V. Adve. Using speculative retirement and larger instruction windows to narrow the performance gap between memory consistency models. In 9th Symposium on Parallel Algorithms and Architectures (SPAA), 1997.

Digital Library

[45]

RISC-V Foundation. RISC-V port of Linux kernel, 2016. https://github.com/riscv/riscv-linux/blob/master/arch/riscv/include/asm/barrier.h.

[46]

Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. Synchronising C/C++ and POWER. In 33rd Conference on Programming Language Design and Implementation (PLDI), 2012.

Digital Library

[47]

Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding power multiprocessors. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 175--186, New York, NY, USA, 2011. ACM.

Digital Library

[48]

Peter Sewell. C/c++11 mappings to processors. 2016.

[49]

Peter Sewell et al. C/C++11 mappings to processors, 2016. https://www.cl.cam.ac.uk/ pes20/cpp/cpp0xmappings.html.

[50]

Abhayendra Singh, Satish Narayanasamy, Daniel Marino, Todd Millstein, and Madanlal Musuvathi. End-to-end sequential consistency. In 39th International Symposium on Computer Architecture (ISCA), 2012.

[51]

SPARC International. The SPARC Architecture Manual (Version 9). Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1994.

Digital Library

[52]

J. M. Tendler, J. S. Dodson, J. S. Fields, H. Le, and B. Sinharoy. POWER4 system microarchitecture. IBM Journal of Research and Development, 46(1):5--25, January 2002.

Digital Library

[53]

Linus Torvalds et al. Linux kernel, 2016. https://github.com/torvalds/linux/blob/master/arch/alpha/include/asm/barrier.h.

[54]

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. Common compiler optimisations are invalid in the C11 memory model and what we can do about it. In 42nd Symposium on Principles of Programming Languages (POPL), 2015.

Digital Library

[55]

Viktor Vafeiadis and Chinmay Narayan. Relaxed separation logic: A program logic for C11 concurrency. In 28th International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 2013.

Digital Library

[56]

Andrew Waterman, Yunsup Lee, David A. Patterson, and Krste Asanovic. The RISC-V instruction set manual, volume I: User-level ISA, version 2.1. Technical Report UCB/EECS-2016-118, EECS Department, University of California, Berkeley, May 2016.

[57]

Thomas F. Wenisch, Anastasia Ailamaki, Babak Falsafi, and Andreas Moshovos. Mechanisms for store-wait-free multiprocessors. In 34th International Symposium on Computer Architecture (ISCA), 2007.

Digital Library

[58]

John Wickerson, Mark Batty, Tyler Sorensen, and George A Constantinides. Automatically comparing memory consistency models. 44th Symposium on Principles of Programming Languages (POPL), 2017.

Digital Library

Cited By

Aimoniotis PKvalsvik AChen XSjälander MKaxiras S(2023)ReCon: Efficient Detection, Management, and Use of Non-Speculative Information LeakageProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3613424.3623770(828-842)Online publication date: 28-Oct-2023
https://dl.acm.org/doi/10.1145/3613424.3623770
Huang BZhang HSubramanyan PVizel YGupta AMalik S(2018)Instruction-Level Abstraction (ILA)ACM Transactions on Design Automation of Electronic Systems10.1145/328244424:1(1-24)Online publication date: 21-Dec-2018
https://dl.acm.org/doi/10.1145/3282444
Graf MAndrade Gdos Santos L(2023)EveCheck: An Event-Driven, Scalable Algorithm for Coherent Shared Memory VerificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.317805142:2(683-696)Online publication date: Feb-2023
https://doi.org/10.1109/TCAD.2022.3178051
Show More Cited By

Index Terms

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
1. General and reference
  1. Cross-computing tools and techniques
    1. Verification
2. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
        Consistency
      2. Formal methods
        Software verification

Recommendations

TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
ASPLOS '17

Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardware-software stack, requiring ...
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems

Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardware-software stack, requiring ...
An evaluation of speculative instruction execution on simultaneous multithreaded processors

Modern superscalar processors rely heavily on speculative execution for performance. For example, our measurements show that on a 6-issue superscalar, 93% of committed instructions for SPECINT95 are speculative. Without speculation, processor resources ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 45, Issue 1

Asplos'17

March 2017

812 pages

ISSN:0163-5964

DOI:10.1145/3093337

Editor:
Babak Falsafi
Interim

Issue’s Table of Contents

ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems
April 2017
856 pages
ISBN:9781450344654
DOI:10.1145/3037697
General Chairs:
Yunji Chen
Institute of Computing Technology, CAS, China
,
Olivier Temam
Google, USA
,
Program Chair:
John Carter
IBM, USA

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 April 2017

Published in SIGARCH Volume 45, Issue 1

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

37
Total Citations
View Citations
1,382
Total Downloads

Downloads (Last 12 months)217
Downloads (Last 6 weeks)44

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Aimoniotis PKvalsvik AChen XSjälander MKaxiras S(2023)ReCon: Efficient Detection, Management, and Use of Non-Speculative Information LeakageProceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3613424.3623770(828-842)Online publication date: 28-Oct-2023
https://dl.acm.org/doi/10.1145/3613424.3623770
Huang BZhang HSubramanyan PVizel YGupta AMalik S(2018)Instruction-Level Abstraction (ILA)ACM Transactions on Design Automation of Electronic Systems10.1145/328244424:1(1-24)Online publication date: 21-Dec-2018
https://dl.acm.org/doi/10.1145/3282444
Graf MAndrade Gdos Santos L(2023)EveCheck: An Event-Driven, Scalable Algorithm for Coherent Shared Memory VerificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.317805142:2(683-696)Online publication date: Feb-2023
https://doi.org/10.1109/TCAD.2022.3178051
Young MHu ALemieux G(2022)Cache Abstraction for Data Race Detection in Heterogeneous Systems with Non-coherent AcceleratorsACM Transactions on Embedded Computing Systems10.1145/353545722:1(1-25)Online publication date: 13-Dec-2022
https://dl.acm.org/doi/10.1145/3535457
Mezger BSantos DDilillo LZeferino CMelo D(2022)A Survey of the RISC-V Architecture Software SupportIEEE Access10.1109/ACCESS.2022.317412510(51394-51411)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3174125
Nagarajan VSorin DHill MWood DNagarajan VSorin DHill MWood D(2022)Specifying and Validating Memory Consistency Models and Cache CoherenceA Primer on Memory Consistency and Cache Coherence10.1007/978-3-031-01764-3_11(253-273)Online publication date: 28-Mar-2022
https://doi.org/10.1007/978-3-031-01764-3_11
Simner BArmstrong APichon-Pharabod JPulte CGrisenthwaite RSewell P(2022)Relaxed virtual memory in Armv8-AProgramming Languages and Systems10.1007/978-3-030-99336-8_6(143-173)Online publication date: 29-Mar-2022
https://doi.org/10.1007/978-3-030-99336-8_6
Windsor MDonaldson AWickerson J(2022)High‐coverage metamorphic testing of concurrency support in C compilersSoftware Testing, Verification and Reliability10.1002/stvr.181232:4Online publication date: 22-Mar-2022
https://doi.org/10.1002/stvr.1812
Hsiao YMulligan DNikoleris NPetri GTrippel C(2021)Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model ImplementationsMICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3466752.3480087(679-694)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1145/3466752.3480087
Feliu JRos AAcacio MKaxiras S(2021)ITSLF: Inter-Thread Store-to-Load Forwardingin Simultaneous MultithreadingMICRO-54: 54th Annual IEEE/ACM International Symposium on Microarchitecture10.1145/3466752.3480086(1296-1308)Online publication date: 18-Oct-2021
https://dl.acm.org/doi/10.1145/3466752.3480086
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents