Reasoning About Foreign Function Interfaces: Blame and Nondeterministic Formal Semantics

Programming Languages;Formal Semantics;Foreign Function Interfaces;Lua;C

Turcotte, Alexiaffiliation1:Faculty of Mathematics ; advisor:Richards, Gregor ; Richards, Gregor ;

University of Waterloo

关键词: C;    Master Thesis;    Foreign Function Interfaces;    Programming Languages;    Formal Semantics;    Lua;   

Others  :  https://uwspace.uwaterloo.ca/bitstream/10012/13696/1/Turcotte_Alexi.pdf

瑞士|英语

来源: UWSPACE Waterloo Institutional Repository

【 摘 要 】

Foreign function interfaces (FFIs) are commonly used as a way to mix programming languages. In such systems, a program written in a host language calls functions written in a guest language from within the same program. Perhaps the most popular language to interface with is C, due in no small part to its performance (often gained through unsafe operations), and programmers often write performance-critical code in C and call it from other languages. But while C is a very performant language, it is far from being memory-safe, and one might expect C to introduce unsoundness into host language systems.This host/guest language relationship echoes that of typed and untyped code in gradual type systems. In such systems, untyped values flowing into typed code must be cast at the boundary between typed and untyped code, and this introduces the possibility for runtime type errors in otherwise statically guaranteed code. Similarly, when a host language calls a function written in a guest language, this introduces any unsoundness in the guest language to the host language, and new errors become possible at runtime. And when an FFI is being used to call C functions, anything is possible.In this thesis, we explore the effects of C on languages using a C FFI. To demonstrate, we give a formalization of Poseidon Lua, an environment wherein Typed Lua code may call C functions, cast C values, and allocate C data. To showcase the interaction between Lua and C, we choose to formalize a core calculus for Lua, and do not model C per se; instead, we reason about C as if C calls were a black-box, remaining general with respect to C's semantics, while carefully quantifying the effects that C can have on Lua by leveraging the concept of blame from gradual typing. We present a nondeterministic operational semantics for Poseidon Lua, and use blame to assure that C is always at fault for runtime errors in Lua.