Document Open Access Logo

Verifying Optimizations for Concurrent Programs

Authors William Mansky, Elsa L. Gunter

PDF
Thumbnail PDF

File

OASIcs.WPTE.2014.15.pdf
  • Filesize: 441 kB
  • 12 pages

Document Identifiers

Author Details

William Mansky
Elsa L. Gunter

Cite As Get BibTex

William Mansky and Elsa L. Gunter. Verifying Optimizations for Concurrent Programs. In First International Workshop on Rewriting Techniques for Program Transformations and Evaluation. Open Access Series in Informatics (OASIcs), Volume 40, pp. 15-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/OASIcs.WPTE.2014.15

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.

Subject Classification

Keywords
  • optimizing compilers
  • interactive theorem proving
  • program transformations
  • temporal logic
  • relaxed memory models

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Sebastian Burckhardt, Madanlal Musuvathi, and Vasu Singh. Verifying local transformations on relaxed memory models. In Proceedings of the 19th Joint European Conference on Theory and Practice of Software, International Conference on Compiler Construction, CC'10/ETAPS'10, pages 104-123, Berlin, Heidelberg, 2010. Springer-Verlag. Google Scholar
  2. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Jaco de Bakker and Jan van Leeuwen, editors, Automata, Languages and Programming, volume 85 of Lecture Notes in Computer Science, pages 299-309. Springer Berlin / Heidelberg, 1980. URL: http://dx.doi.org/10.1007/3-540-10003-2_79.
  3. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1985. Google Scholar
  4. Sara Kalvala, Richard Warburton, and David Lacey. Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst., 31(4):1-48, 2009. Google Scholar
  5. Jens Krinke. Context-sensitive slicing of concurrent programs. SIGSOFT Softw. Eng. Notes, 28(5):178-187, September 2003. Google Scholar
  6. Sorin Lerner, Todd Millstein, and Craig Chambers. Automatically proving the correctness of compiler optimizations. SIGPLAN Not., 38:220-231, May 2003. Google Scholar
  7. Xavier Leroy. A formally verified compiler back-end. J. Autom. Reason., 43(4):363-446, December 2009. Google Scholar
  8. Hongjin Liang, Xinyu Feng, and Ming Fu. A rely-guarantee-based simulation for verifying concurrent program transformations. In Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL'12, pages 455-468, New York, NY, USA, 2012. ACM. Google Scholar
  9. LLVM Language Reference Manual. http://llvm.org/docs/LangRef.html, April 2014. Google Scholar
  10. William Mansky, Dennis Griffith, and Elsa L. Gunter. Specifying and executing optimizations for parallel programs. Accepted for publication by GRAPHITE'14. Google Scholar
  11. William Mansky and Elsa Gunter. A framework for formal verification of compiler optimizations. In Proceedings of the First international conference on Interactive Theorem Proving, ITP'10, pages 371-386, Berlin, Heidelberg, 2010. Springer-Verlag. Google Scholar
  12. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press, 1990. Google Scholar
  13. Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In TACAS'98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pages 151-166, London, UK, 1998. Springer-Verlag. Google Scholar
  14. Pradeep S. Sindhu, Jean-Marc Frailong, and Michel Cekleov. Formal specification of memory models. In Michel Dubois and Shreekant Thakkar, editors, Scalable Shared Memory Multiprocessors, pages 25-41. Springer US, 1992. Google Scholar
  15. Jaroslav Ševčík. Safe optimisations for shared-memory concurrent programs. SIGPLAN Not., 46(6):306-316, June 2011. Google Scholar
  16. Jaroslav Ševčik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. Relaxed-memory concurrency and verified compilation. SIGPLAN Not., 46(1):43-54, January 2011. Google Scholar
  17. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. Finding and understanding bugs in C compilers. SIGPLAN Not., 46(6):283-294, June 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact