Skip to main content
SpringerLink
Log in
Book cover

International Static Analysis Symposium

SAS 2013: Static Analysis pp 304–323Cite as

Witnessing Program Transformations

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7935))

Abstract

We study two closely related problems: (a) showing that a program transformation is correct and (b) propagating an invariant through a program transformation. The second problem is motivated by an application which utilizes program invariants to improve the quality of compiler optimizations. We show that both problems can be addressed by augmenting a transformation with an auxiliary witness generation procedure. For every application of the transformation, the witness generator constructs a relation which guarantees the correctness of that instance. We show that stuttering simulation is a sound and complete witness format. Completeness means that, under mild conditions, every correct transformation induces a stuttering simulation witness which is strong enough to prove that the transformation is correct. A witness is self-contained, in that its correctness is independent of the optimization procedure which generates it. Any invariant of a source program can be turned into an invariant of the target of a transformation by suitably composing it with its witness. Stuttering simulations readily compose, forming a single witness for a sequence of transformations. Witness generation is simpler than a formal proof of correctness, and it is comprehensive, unlike the heuristics used for translation validation. We define witnesses for a number of standard compiler optimizations; this exercise shows that witness generators can be implemented quite easily.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  2. Allen, R., Kennedy, K.: Optimizing Compilers for Modern Architectures. Morgan Kaufmann (2002)

    Google Scholar 

  3. Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: Asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29–43. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  4. Barthe, G., Kunz, C.: An abstract model of certificate translation. ACM Trans. Program. Lang. Syst. 33(4), 13 (2011)

    Article  Google Scholar 

  5. Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14–25 (2004)

    Google Scholar 

  6. Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13–31 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  7. Dijkstra, E.: Guarded commands, nondeterminacy, and formal derivation of programs. CACM 18(8) (1975)

    Google Scholar 

  8. Dijkstra, E., Scholten, C.: Predicate Calculus and Program Semantics. Springer (1990)

    Google Scholar 

  9. Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75–88 (2004), Webpage at llvm.org

  10. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42–54. ACM (2006)

    Google Scholar 

  11. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  12. Manna, Z., McCarthy, J.: Properties of programs and partial function logic. Journal of Machine Intelligence 5 (1970)

    Google Scholar 

  13. Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (2001)

    Google Scholar 

  14. Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 304–318. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  15. Muchnick, S.: Advanced Compiler Design & Implementation. Morgan Kaufmann, San Francisco (1997)

    Google Scholar 

  16. Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 284–296. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  17. Namjoshi, K.S.: Lifting temporal proofs through abstractions. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 174–188. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation, PLDI 2000, pp. 83–95 (2000)

    Google Scholar 

  19. Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: OSDI, pp. 229–243. ACM (1996)

    Google Scholar 

  20. Pnueli, A., Siegel, M., Shtrichman, O.: The code validation tool (CVT)- automatic verification of a compilation process. Software Tools for Technology Transfer 2(2), 192–201 (1998)

    Article  MATH  Google Scholar 

  21. Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the Run-Time Result Verification Workshop (July 2000)

    Google Scholar 

  22. Tristan, J.-B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI, pp. 295–305 (2011)

    Google Scholar 

  23. Zuck, L.D., Pnueli, A., Goldberg, B.: Voc: A methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003)

    Google Scholar 

  24. Zuck, L.D., Pnueli, A., Goldberg, B., Barrett, C.W., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. Formal Methods in System Design 27(3), 335–360 (2005)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bell Laboratories, Alcatel-Lucent, USA

    Kedar S. Namjoshi

  2. University of Illinois at Chicago, USA

    Lenore D. Zuck

Authors
  1. Kedar S. Namjoshi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lenore D. Zuck
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052, Redmond, WA, USA

    Francesco Logozzo

  2. One Microsoft Way, Microsoft Research, 98052, Redmond,, WA,, USA

    Manuel Fähndrich

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Namjoshi, K.S., Zuck, L.D. (2013). Witnessing Program Transformations. In: Logozzo, F., Fähndrich, M. (eds) Static Analysis. SAS 2013. Lecture Notes in Computer Science, vol 7935. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38856-9_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38856-9_17

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38855-2

  • Online ISBN: 978-3-642-38856-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation