A consistency checker for memory subsystem traces
Authors:
- 1 October 2016
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 133-140
Abstract
Verifying the memory subsystem in a modern shared-memory multiprocessor is a big challenge. Optimized implementations are highly sophisticated, yet must provide subtle consistency and liveness guarantees for the correct execution of concurrent programs. We present a tool that supports efficient specification-based testing of the memory subsystem against a range of formally specified consistency models. Our tool operates directly on the memory subsystem interface, promoting a compositional approach to system-on-chip verification, and can be used to search for simple failure cases - assisting rapid debug. It has recently been incorporated into the development flows of two open-source implementations - Berkeley's Rocket Chip(RISC-V) and Cambridge's BERI (MIPS) - where it has uncovered a number of serious bugs.Keywords
This publication has 13 references indexed in Scilit:
- A generic synthesisable test bench2015
- Chisel2012
- Understanding POWER multiprocessors2011
- The semantics of x86-CC multiprocessor machine codeACM SIGPLAN Notices, 2009
- Completely Verifying Memory Consistency of Test Program Executions2006
- Efficient algorithms for verifying memory consistency2005
- Shared memory consistency models: a tutorialComputer, 1996
- On testing cache-coherent shared memories1994
- Myths about the mutual exclusion problemInformation Processing Letters, 1981
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess ProgramsIEEE Transactions on Computers, 1979