Document Open Access Logo

Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language

Authors Alexi Turcotte, Ellen Arteca, Gregor Richards

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.16.pdf
  • Filesize: 0.62 MB
  • 32 pages

Document Identifiers

Author Details

Alexi Turcotte
  • Northeastern University, Boston, MA, USA
Ellen Arteca
  • Northeastern University, Boston, MA, USA
Gregor Richards
  • University of Waterloo, Waterloo, ON, Canada

Acknowledgements

The authors would like to thank Rafi Turas for writing the implementation of these techniques in Poseidon Lua. We'd also like to thank Hugo Musso Gualandi for his valuable discussions/feedback. This work was partially funded by NSERC.

Cite AsGet BibTex

Alexi Turcotte, Ellen Arteca, and Gregor Richards. Reasoning About Foreign Function Interfaces Without Modelling the Foreign Language. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 16:1-16:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.16

Abstract

Foreign function interfaces (FFIs) allow programs written in one language (called the host language) to call functions written in another language (called the guest language), and are widespread throughout modern programming languages, with C FFIs being the most prevalent. Unfortunately, reasoning about C FFIs can be very challenging, particularly when using traditional methods which necessitate a full model of the guest language in order to guarantee anything about the whole language. To address this, we propose a framework for defining whole language semantics of FFIs without needing to model the guest language, which makes reasoning about C FFIs feasible. We show that with such a semantics, one can guarantee some form of soundness of the overall language, as well as attribute errors in well-typed host language programs to the guest language. We also present an implementation of this scheme, Poseidon Lua, which shows a speedup over a traditional Lua C FFI.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Interoperability
  • Software and its engineering → Semantics
Keywords
  • Formal Semantics
  • Language Interoperation
  • Lua
  • C
  • Foreign Function Interfaces

Metrics

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

Supplementary Materials

References

  1. M. Abadi, L. Cardelli, B. Pierce, and G. Plotkin. Dynamic Typing in a Statically-typed Language. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '89, pages 213-227, New York, NY, USA, 1989. ACM. URL: http://dx.doi.org/10.1145/75277.75296.
  2. CompCert. CompCert Main Page. http://compcert.inria.fr. Accessed: 2018-07-23.
  3. Facebook. luaffifb. https://github.com/facebookarchive/luaffifb. Accessed: 2019-01-10.
  4. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt. Semantics engineering with PLT Redex. Mit Press, 2009. Google Scholar
  5. Isaac Gouy. The Computer Language Benchmarks Game. https://benchmarksgame-team.pages.debian.net/benchmarksgame/. Accessed: 2019-01-10.
  6. Kathryn E Gray. Safe cross-language inheritance. In European Conference on Object-Oriented Programming, pages 52-75. Springer, 2008. Google Scholar
  7. Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. The essence of JavaScript. In European Conference on Object-Oriented Programming, pages 126-150. Springer, 2010. Google Scholar
  8. Atsushi Igarashi, Benjamin C Pierce, and Philip Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems (TOPLAS), 23(3):396-450, 2001. Google Scholar
  9. Julia. Calling C and Fortran Code. https://docs.julialang.org/en/stable/manual/calling-c-and-fortran-code/index.html. Accessed: 2018-07-14.
  10. Hanshu Lin. Operational semantics for Featherweight Lua. Master’s Projects, page 387, 2015. Google Scholar
  11. Lisp. CFFI The Common Foreign Function Interface. https://common-lisp.net/project/cffi/. Accessed: 2018-07-25.
  12. Tidal Lock. Tidal Lock Gradual Static Typing for Lua. https://github.com/fab13n/metalua/tree/tilo/src/tilo. Accessed: 2018-06-20.
  13. Lua. Lua 5.3 Documentation. https://www.lua.org/manual/5.3/. Accessed: 2018-06-20.
  14. André Murbach Maidl, Fabio Mascarenhas, and Roberto Ierusalimschy. Typed Lua: An optional type system for Lua. In Proceedings of the Workshop on Dynamic Languages and Applications, pages 1-10. ACM, 2014. Google Scholar
  15. MathWorks. Matlab Calling C Shared Libraries. https://www.mathworks.com/help/matlab/using-c-shared-library-functions-in-matlab-.html. Accessed: 2018-07-04.
  16. Jacob Matthews and Robert Bruce Findler. Operational semantics for multi-language programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 31(3):12, 2009. Google Scholar
  17. Microsoft. TypeScript - Language Specification Version 1.8. Technical report, Microsoft, January 2016. Google Scholar
  18. James Newsome and Dawn Xiaodong Song. Dynamic Taint Analysis for Automatic Detection, Analysis, and Signature Generation of Exploits on Commodity Software. In NDSS, volume 5, pages 3-4. Citeseer, 2005. Google Scholar
  19. Graham Ollis. Perl Perl Foreign Function Interface based on GNU ffcall. https://metacpan.org/pod/FFI. Accessed: 2018-07-06.
  20. Oracle. JNI specification. https://docs.oracle.com/javase/8/docs/technotes/guides/jni/spec/jniTOC.html. Accessed: 2019-06-10.
  21. Mike Pall. The LuaJIT Project. Web site: http://luajit. org, 2008. Google Scholar
  22. 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), volume 71 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:15, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.SNAPL.2017.12.
  23. Python. CFFI Documentation. https://cffi.readthedocs.io/en/latest/. Accessed: 2018-07-06.
  24. Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  25. Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, and Fabio Mascarenhas. Decoding Lua: Formal Semantics for the Developer and the Semanticist. In Proceedings of the 13th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2017, pages 75-86, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3133841.3133848.
  26. SWIG Team. SWIG. https://swig.org. Accessed: 2019-06-10.
  27. Sam Tobin-Hochstadt, Vincent St-Amour, Eric Dobson, and Asumu Takikawa. Typed Racket Documentation. https://docs.racket-lang.org/ts-guide/. Accessed: 2018-08-01.
  28. Philip Wadler and Robert Bruce Findler. Well-typed programs can’t be blamed. In European Symposium on Programming, pages 1-16. Springer, 2009. Google Scholar
  29. Alon Zakai. Emscripten: an LLVM-to-JavaScript compiler. In Proceedings of the ACM international conference companion on Object oriented programming systems languages and applications companion, pages 301-312. ACM, 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 Imprint Privacy Contact