-
Model Checking Race-freedom When "Sequential Consistency for Data-race-free Programs" is Guaranteed
Authors:
Wenhao Wu,
Jan Hückelheim,
Paul D. Hovland,
Ziqing Luo,
Stephen F. Siegel
Abstract:
Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modific…
▽ More
Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP.
△ Less
Submitted 20 July, 2023; v1 submitted 29 May, 2023;
originally announced May 2023.
-
QContext: Context-Aware Decomposition for Quantum Gates
Authors:
Ji Liu,
Max Bowman,
Pranav Gokhale,
Siddharth Dangwal,
Jeffrey Larson,
Frederic T. Chong,
Paul D. Hovland
Abstract:
In this paper we propose QContext, a new compiler structure that incorporates context-aware and topology-aware decompositions. Because of circuit equivalence rules and resynthesis, variants of a gate-decomposition template may exist. QContext exploits the circuit information and the hardware topology to select the gate variant that increases circuit optimization opportunities. We study the basis-g…
▽ More
In this paper we propose QContext, a new compiler structure that incorporates context-aware and topology-aware decompositions. Because of circuit equivalence rules and resynthesis, variants of a gate-decomposition template may exist. QContext exploits the circuit information and the hardware topology to select the gate variant that increases circuit optimization opportunities. We study the basis-gate-level context-aware decomposition for Toffoli gates and the native-gate-level context-aware decomposition for CNOT gates. Our experiments show that QContext reduces the number of gates as compared with the state-of-the-art approach, Orchestrated Trios.
△ Less
Submitted 3 February, 2023;
originally announced February 2023.
-
Report of the HPC Correctness Summit, Jan 25--26, 2017, Washington, DC
Authors:
Ganesh Gopalakrishnan,
Paul D. Hovland,
Costin Iancu,
Sriram Krishnamoorthy,
Ignacio Laguna,
Richard A. Lethin,
Koushik Sen,
Stephen F. Siegel,
Armando Solar-Lezama
Abstract:
Maintaining leadership in HPC requires the ability to support simulations at large scales and fidelity. In this study, we detail one of the most significant productivity challenges in achieving this goal, namely the increasing proclivity to bugs, especially in the face of growing hardware and software heterogeneity and sheer system scale. We identify key areas where timely new research must be pro…
▽ More
Maintaining leadership in HPC requires the ability to support simulations at large scales and fidelity. In this study, we detail one of the most significant productivity challenges in achieving this goal, namely the increasing proclivity to bugs, especially in the face of growing hardware and software heterogeneity and sheer system scale. We identify key areas where timely new research must be proactively begun to address these challenges, and create new correctness tools that must ideally play a significant role even while ram** up toward exacale. We close with the proposal for a two-day workshop in which the problems identified in this report can be more broadly discussed, and specific plans to launch these new research thrusts identified.
△ Less
Submitted 21 May, 2017;
originally announced May 2017.
