TY - GEN
T1 - Verifying optimizations for concurrent programs
AU - Mansky, William
AU - Gunter, Elsa L.
PY - 2014
Y1 - 2014
N2 - While program correctness for compiled languages depends fundamentally on compiler correctness, compiler optimizations are not usually formally verified due to the effort involved, particularly in the presence of concurrency. In this paper, we present a framework for stating and reasoning about compiler optimizations and transformations on programs in the presence of relaxed memory models. The core of the framework is the PTRANS specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. We demonstrate our technique by verifying the correctness of a redundant store elimination optimization in a simple LLVM-like intermediate language, relying on a theorem that allows us to lift single-thread simulation relations to simulations on multithreaded programs.
AB - While program correctness for compiled languages depends fundamentally on compiler correctness, compiler optimizations are not usually formally verified due to the effort involved, particularly in the presence of concurrency. In this paper, we present a framework for stating and reasoning about compiler optimizations and transformations on programs in the presence of relaxed memory models. The core of the framework is the PTRANS specification language, in which program transformations are expressed as rewrites on control flow graphs with temporal logic side conditions. We demonstrate our technique by verifying the correctness of a redundant store elimination optimization in a simple LLVM-like intermediate language, relying on a theorem that allows us to lift single-thread simulation relations to simulations on multithreaded programs.
KW - Interactive theorem proving
KW - Optimizing compilers
KW - Program transformations
KW - Relaxed memory models
KW - Temporal logic
UR - http://www.scopus.com/inward/record.url?scp=84905736447&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84905736447&partnerID=8YFLogxK
U2 - 10.4230/OASIcs.WPTE.2014.15
DO - 10.4230/OASIcs.WPTE.2014.15
M3 - Conference contribution
AN - SCOPUS:84905736447
SN - 9783939897705
T3 - OpenAccess Series in Informatics
SP - 15
EP - 26
BT - 1st International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 1st International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2014
Y2 - 13 July 2014 through 13 July 2014
ER -