Document Open Access Logo

Verified Compilers for a Multi-Language World

Author Amal Ahmed

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2015.15.pdf
  • Filesize: 0.62 MB
  • 17 pages

Document Identifiers

Author Details

Amal Ahmed

Cite AsGet BibTex

Amal Ahmed. Verified Compilers for a Multi-Language World. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 15-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.SNAPL.2015.15

Abstract

Though there has been remarkable progress on formally verified compilers in recent years, most of these compilers suffer from a serious limitation: they are proved correct under the assumption that they will only be used to compile whole programs. This is an unrealistic assumption since most software systems today are comprised of components written in different languages - both typed and untyped - compiled by different compilers to a common target, as well as low-level libraries that may be handwritten in the target language. We are pursuing a new methodology for building verified compilers for today's world of multi-language software. The project has two central themes, both of which stem from a view of compiler correctness as a language interoperability problem. First, to specify correctness of component compilation, we require that if a source component s compiles to target component t, then t linked with some arbitrary target code t' should behave the same as s interoperating with t'. The latter demands a formal semantics of interoperability between the source and target languages. Second, to enable safe interoperability between components compiled from languages as different as ML, Rust, Python, and C, we plan to design a gradually type-safe target language based on LLVM that supports safe interoperability between more precisely typed, less precisely typed, and type-unsafe components. Our approach opens up a new avenue for exploring sensible language interoperability while also tackling compiler correctness.
Keywords
  • verified compilation
  • compositional compiler correctness
  • multi-language semantics
  • typed low-level languages
  • gradual typing

Metrics

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

References

  1. Pieter Agten, Bart Jacobs, and Frank Piessens. Sound modular verification of c code executing in an unverified context. In ACM Symposium on Principles of Programming Languages (POPL), Mumbai, India, January 2015. Google Scholar
  2. Amal Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In European Symposium on Programming (ESOP), pages 69-83, March 2006. Google Scholar
  3. Amal Ahmed and Matthias Blume. Typed closure conversion preserves observational equivalence. In International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, pages 157-168, September 2008. Google Scholar
  4. Amal Ahmed and Matthias Blume. An equivalence-preserving CPS translation via multi-language semantics. In International Conference on Functional Programming (ICFP), Tokyo, Japan, pages 431-444, September 2011. Google Scholar
  5. Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In ACM Symposium on Principles of Programming Languages (POPL), Savannah, Georgia, January 2009. Google Scholar
  6. Amal Ahmed, Robert Bruce Findler, Jeremy Siek, and Philip Wadler. Blame for all. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, pages 201-214, January 2011. Google Scholar
  7. Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In International Conference on Functional Programming (ICFP), Tallinn, Estonia, pages 78-91, September 2005. Google Scholar
  8. Amal Ahmed, Matthew Fluet, and Greg Morrisett. L3 : A linear language with locations. Fundamenta Informaticae, 77(4):397-449, June 2007. Google Scholar
  9. Amal Ahmed, Limin Jia, and David Walker. Reasoning about hierarchical storage. In IEEE Symposium on Logic in Computer Science (LICS), Ottawa, Canada, pages 33-44, June 2003. Google Scholar
  10. Amal Ahmed and David Walker. The logical approach to stack typing. In ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI), pages 74-85, January 2003. Google Scholar
  11. João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. Polymorphic contracts. In European Symposium on Programming (ESOP), March 2011. Google Scholar
  12. Nick Benton and Chung-Kil Hur. Biorthogonality, step-indexing and compiler correctness. In International Conference on Functional Programming (ICFP), Edinburgh, Scotland, September 2009. Google Scholar
  13. Nick Benton and Chung-Kil Hur. Realizability and compositional compiler correctness for a polymorphic language. Technical Report MSR-TR-2010-62, Microsoft Research, April 2010. Google Scholar
  14. Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel. Verified compilation for shared-memory C. In European Symposium on Programming (ESOP), April 2014. Google Scholar
  15. Adam Chlipala. A verified compiler for an impure functional language. In ACM Symposium on Principles of Programming Languages (POPL), Madrid, Spain, January 2010. Google Scholar
  16. Maulik A. Dave. Compiler verification: A bibliography. ACM SIGSOFT Software Engineering Notes, 28(6), 2003. Google Scholar
  17. Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Complete monitors for behavioral contracts. In European Symposium on Programming (ESOP), March 2012. Google Scholar
  18. Derek Dreyer, Georg Neis, and Lars Birkedal. The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4&5):477-528, 2012. Google Scholar
  19. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), Pittsburgh, Pennsylvania, pages 48-59, September 2002. Google Scholar
  20. Cormac Flanagan. Hybrid type checking. In ACM Symposium on Principles of Programming Languages (POPL), January 2006. Google Scholar
  21. Matthew Fluet, Greg Morrisett, and Amal Ahmed. Linear regions are all you need. In European Symposium on Programming (ESOP), pages 7-21, March 2006. Google Scholar
  22. Cedric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Benjamin Livshits. Fully abstract compilation to JavaScript. In ACM Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 371-384, 2013. Google Scholar
  23. Kathryn E Gray, Robert Bruce Findler, and Matthew Flatt. Fine-grained interoperability through mirrors and contracts. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), 2005. Google Scholar
  24. Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. Contracts made manifest. In ACM Symposium on Principles of Programming Languages (POPL), Madrid, Spain, pages 353-364, January 2010. Google Scholar
  25. Jessica Gronski, Kenneth Knowles, Aaron Tomb, Stephen N. Freund, and Cormac Flanagan. Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop (Scheme), pages 93-104, September 2006. Google Scholar
  26. Chung-Kil Hur and Derek Dreyer. A Kripke logical relation between ML and assembly. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, January 2011. Google Scholar
  27. Shriram Krishnamurthi, Peter Walton Hopkins, Jay Mccarthy, Paul T. Graunke, Greg Pettyjohn, and Matthias Felleisen. Implementation and use of the PLT Scheme web server. Higher-Order and Symbolic Computation, 20(4):431-460, 2007. Google Scholar
  28. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML : A verified implementation of ML. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, January 2014. Google Scholar
  29. Xavier Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In ACM Symposium on Principles of Programming Languages (POPL), Charleston, South Carolina, January 2006. Google Scholar
  30. Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. Google Scholar
  31. Andreas Lochbihler. Verifying a compiler for Java threads. In European Symposium on Programming (ESOP), March 2010. Google Scholar
  32. Jacob Matthews and Amal Ahmed. Parametric polymorphism through run-time sealing, or, theorems for low, low prices! In European Symposium on Programming (ESOP), pages 16-31, March 2008. Google Scholar
  33. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. In ACM Symposium on Principles of Programming Languages (POPL), Nice, France, pages 3-10, January 2007. Google Scholar
  34. Yasuhiko Minamide, Greg Morrisett, and Robert Harper. Typed closure conversion. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 271-283, January 1996. Google Scholar
  35. Greg Morrisett, Amal Ahmed, and Matthew Fluet. L3 : A linear language with locations. In Typed Lambda Calculi and Applications (TLCA), Nara, Japan, pages 293-307, April 2005. Google Scholar
  36. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999. Google Scholar
  37. Magnus O. Myreen. Verified just-in-time compiler on x86. In ACM Symposium on Principles of Programming Languages (POPL), Madrid, Spain, January 2010. Google Scholar
  38. Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal. Abstract predicates and mutable ADTs in Hoare Type Theory. In European Symposium on Programming (ESOP), pages 189-204, March 2007. Google Scholar
  39. Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. Verification of information flow and access control policies with dependent types. In IEEE Symposium on Security and Privacy, pages 165-179, 2011. Google Scholar
  40. Aleksandar Nanevski, Greg Morrisett, Avi Shinnar, Paul Govereau, and Lars Birkedal. Ynot: Dependent types for imperative programs. In International Conference on Functional Programming (ICFP), Victoria, British Columbia, Canada, pages 229-240, 2006. Google Scholar
  41. Georg Neis, Chung-Kil Hur, Jan-Oliver Kaiser, Craig McLaughlin, Derek Dreyer, and Viktor Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. Available at: http://www.mpi-sws.org/∼dreyer/papers/pilsner/paper.pdf, February 2015. Google Scholar
  42. Ocsigen. http://ocsigen.org. Google Scholar
  43. Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent interoperability. In Programming Languages meets Program Verification (PLPV), January 2012. Google Scholar
  44. Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pages 437-450, August 2004. Google Scholar
  45. James T. Perconti and Amal Ahmed. Verifying an open compiler using multi-language semantics. In European Symposium on Programming (ESOP), April 2014. Google Scholar
  46. Christian Queinnec. Inverting back the inversion of control or, continuations versus page-centric programming. SIGPLAN Not., 38(2):57-64, February 2003. Google Scholar
  47. Seaside. http://seaside.st. Google Scholar
  48. Jaroslav Sevcik, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. Relaxed-memory concurrency and verified compilation. In ACM Symposium on Principles of Programming Languages (POPL), Austin, Texas, 2011. Google Scholar
  49. Jeremy G. Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop (Scheme), pages 81-92, September 2006. Google Scholar
  50. Jeremy G. Siek and Walid Taha. Gradual typing for objects. In European Conference on Object-Oriented Programming (ECOOP), 2007. Google Scholar
  51. Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. Compositional compcert. In ACM Symposium on Principles of Programming Languages (POPL), Mumbai, India, 2015. Google Scholar
  52. Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, and Gavin M. Bierman. Gradual typing embedded securely in JavaScript. In ACM Symposium on Principles of Programming Languages (POPL), San Diego, California, pages 425-438, 2014. Google Scholar
  53. Asumu Takikawa, T. Stephen Strickland, Christos Dimoulas, Sam Tobin-Hochstadt, and Matthias Felleisen. Gradual typing for first-class classes. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), 2012. Google Scholar
  54. The LLVM Development Team. The LLVM reference manual. http://llvm.org [0]/docs [0]/LangRef.html. Google Scholar
  55. Jesse Tov. Stateful contracts for affine types. In European Symposium on Programming (ESOP), March 2010. Google Scholar
  56. Aaron Turon, Jacob Thamsborg, Amal Ahmed, Lars Birkedal, and Derek Dreyer. Logical relations for fine-grained concurrency. In ACM Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 201-214, January 2013. Google Scholar
  57. Vellvm: Verifying the llvm. http://www.cis.upenn.edu/∼stevez/vellvm/. Google Scholar
  58. Philip Wadler and Robert Bruce Findler. Well-typed programs can't be blamed. In European Symposium on Programming (ESOP), pages 1-16, March 2009. Google Scholar
  59. Peng Wang, Santiago Cuellar, and Adam Chlipala. Compiler verification meets cross-language linking via data abstraction. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), October 2014. Google Scholar
  60. Bennet Yee, David Sehr, Gregory Dardyk, J. Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. Native Client: A sandbox for portable, untrusted x86 native code. Communications of the ACM, 53(1):91-99, 2010. Google Scholar
  61. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In ACM Symposium on Principles of Programming Languages (POPL), Philadelphia, Pennsylvania, January 2012. Google Scholar
  62. Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Formal verification of SSA-based optimizations for LLVM. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Seattle, Washington, June 2013. 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 Imprint Privacy Contact