License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WPTE.2014.15
URN: urn:nbn:de:0030-drops-45869
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4586/
Go to the corresponding OASIcs Volume Portal

Mansky, William ; Gunter, Elsa L.

Verifying Optimizations for Concurrent Programs

pdf-format:
p015-03-mansky.pdf (0.4 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{mansky_et_al:OASIcs:2014:4586,
  author =	{William Mansky and Elsa L. Gunter},
  title =	{{Verifying Optimizations for Concurrent Programs}},
  booktitle =	{First International Workshop on Rewriting Techniques for Program Transformations and Evaluation},
  pages =	{15--26},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-70-5},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{40},
  editor =	{Manfred Schmidt-Schau{\ss} and Masahiko Sakai and David Sabel and Yuki  Chiba},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4586},
  URN =		{urn:nbn:de:0030-drops-45869},
  doi =		{10.4230/OASIcs.WPTE.2014.15},
  annote =	{Keywords: optimizing compilers, interactive theorem proving, program transformations, temporal logic, relaxed memory models}
}

Keywords: optimizing compilers, interactive theorem proving, program transformations, temporal logic, relaxed memory models
Collection: First International Workshop on Rewriting Techniques for Program Transformations and Evaluation
Issue Date: 2014
Date of publication: 13.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI