Linking Types for Multi-Language Software: Have Your Cake and Eat It Too

Authors Daniel Patterson, Amal Ahmed



PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.12.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Daniel Patterson
Amal Ahmed

Cite As Get BibTex

Daniel Patterson and Amal Ahmed. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.SNAPL.2017.12

Abstract

Large software systems are and should be implemented with many different languages, each suited to the domain of the task at hand. High-level business logic may be written in Java or OCaml, resource-intensive components may be written in C or Rust, and high-assurance components may be written in Coq. In some development shops, domain-specific languages are used in various parts of systems to better separate the logic of particular problems from the plumbing of general-purpose programming. But how are programmers to reason about such multi-language systems?

Currently, for a programmer to reason about a single source component within this multi-language system, it is not sufficient for her to consider how her component behaves in source-level contexts. Instead, she is required to understand the target contexts that her component will be run in after compilation - which requires not only understanding aspects of the compiler, but also how target components are linked together. These target contexts may have behavior inexpressible in the source, which can impact the notion of equivalence that justifies behavior-preserving modifications of code, whether programmer refactorings or compiler optimizations. But while programmers should not have to reason about arbitrary target contexts, sometimes multi-language linking is done exactly to gain access to features unavailable in the source.

To enable programmers to reason about components that link with behavior inexpressible in their language, we advocate that language designers incorporate specifications for linking into the source language. Such specifications should allow
a programmer to reason about inputs from other languages in a way that remains close to the semantics of her language. Linking types are a well-specified minimal extension of a source language that allow programmers to annotate where in their programs they can link with components that are not expressible in their unadulterated source language. This gives them  fine-grained control over the contexts that they must reason about and the equivalences that arise.

Subject Classification

Keywords
  • Linking
  • program reasoning
  • equivalence
  • expressive power of languages
  • fully abstract compilation

Metrics

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

References

  1. Amal Ahmed. Verified Compilers for a Multi-Language World. In Thomas Ball, Rastislav Bodik, Shriram Krishnamurthi, Benjamin S. Lerner, and Greg Morrisett, editors, 1st Summit on Advances in Programming Languages (SNAPL 2015), volume 32 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15-31, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2015.15.
  2. 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
  3. 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
  4. 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
  5. 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
  6. Guy E. Blelloch and Robert Harper. Cache and I/O efficient functional algorithms. In ACM Symposium on Principles of Programming Languages (POPL), Rome, Italy, pages 39-50, January 2013. Google Scholar
  7. William J. Bowman and Amal Ahmed. Noninterference for free. In International Conference on Functional Programming (ICFP), Vancouver, British Columbia, Canada, September 2015. Google Scholar
  8. Luca Cardelli. Program fragments, linking, and modularization. In ACM Symposium on Principles of Programming Languages (POPL), Paris, France, pages 266-277, January 1997. Google Scholar
  9. Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Jan Hoffmann. Relational cost analysis. In ACM Symposium on Principles of Programming Languages (POPL), Paris, France, January 2017. Google Scholar
  10. Dominique Devriese, Marco Patrignani, and Frank Piessens. Fully-abstract compilation by approximate back-translation. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, 2016. Google Scholar
  11. Vijay D'Silva, Mathias Payer, and Dawn Song. The correctness-security gap in compiler optmization. In Language-theoretic Security IEEE Security and Privacy Workshop (LangSec), 2015. Google Scholar
  12. Matthias Felleisen. On the expressive power of programming languages. In Science of Computer Programming, pages 134-151. Springer-Verlag, 1990. Google Scholar
  13. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In ACM Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 595-608, January 2015. Google Scholar
  14. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Resource Aware ML. In 24rd International Conference on Computer Aided Verification (CAV'12), volume 7358 of Lecture Notes in Computer Science, pages 781-786. Springer, 2012. Google Scholar
  15. 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
  16. Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. Lightweight verification of separate compilation. In ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg, Florida, pages 178-190. ACM, 2016. Google Scholar
  17. 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
  18. Daan Leijen. Koka: Programming with row polymorphic effect types. In Mathematically Structured Functional Programming, Grenoble, France, April 2014. Google Scholar
  19. 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
  20. Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363-446, 2009. Google Scholar
  21. Paul Blain Levy. Call-by-Push-Value. Ph. D. dissertation, Queen Mary, University of London, London, UK, March 2001. Google Scholar
  22. Andreas Lochbihler. Verifying a compiler for Java threads. In European Symposium on Programming (ESOP), March 2010. Google Scholar
  23. 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. In International Conference on Functional Programming (ICFP), Vancouver, British Columbia, Canada, August 2015. Google Scholar
  24. Max S. New, William J. Bowman, and Amal Ahmed. Fully abstract compilation via universal embedding. In International Conference on Functional Programming (ICFP), Nara, Japan, September 2016. Google Scholar
  25. Marco Patrignani, Pieter Agten, Raoul Strackx, Bart Jacobs, Dave Clarke, and Frank Piessens. Secure compilation to protected module architectures. ACM Transactions on Programming Languages and Systems, 37(2):6:1-6:50, April 2015. Google Scholar
  26. Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. FunTAL: Reasonably mixing a functional language with assembly. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Barcelona, Spain, June 2017. To appear. Available at URL: http://www.ccs.neu.edu/home/amal/papers/funtal.pdf.
  27. Daniel Patterson, Jamie Perconti, Christos Dimoulas, and Amal Ahmed. FunTAL: Reasonably mixing a functional language with assembly (technical appendix). Available at http://www.ccs.neu.edu/ [0]home/ [0]amal/ [0]papers/ [0]funtal-tr.pdf, April 2017. Google Scholar
  28. James T. Perconti and Amal Ahmed. Verifying an open compiler using multi-language semantics. In European Symposium on Programming (ESOP), April 2014. Google Scholar
  29. 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
  30. 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
  31. Jesse Tov and Riccardo Pucella. Stateful contracts for affine types. In European Symposium on Programming (ESOP), March 2010. Google Scholar
  32. 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