Reasoning About Foreign Function Interfaces: Blame and Nondeterministic Formal Semantics

dc.contributor.authorTurcotte, Alexi
dc.date.accessioned2018-08-31T18:42:43Z
dc.date.available2018-08-31T18:42:43Z
dc.date.issued2018-08-31
dc.date.submitted2018-08-28
dc.description.abstractForeign 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.en
dc.identifier.urihttp://hdl.handle.net/10012/13696
dc.language.isoenen
dc.pendingfalse
dc.publisherUniversity of Waterlooen
dc.subjectProgramming Languagesen
dc.subjectFormal Semanticsen
dc.subjectForeign Function Interfacesen
dc.subjectLuaen
dc.subjectCen
dc.titleReasoning About Foreign Function Interfaces: Blame and Nondeterministic Formal Semanticsen
dc.typeMaster Thesisen
uws-etd.degreeMaster of Mathematicsen
uws-etd.degree.departmentDavid R. Cheriton School of Computer Scienceen
uws-etd.degree.disciplineComputer Scienceen
uws-etd.degree.grantorUniversity of Waterlooen
uws.contributor.advisorRichards, Gregor
uws.contributor.affiliation1Faculty of Mathematicsen
uws.peerReviewStatusUnrevieweden
uws.published.cityWaterlooen
uws.published.countryCanadaen
uws.published.provinceOntarioen
uws.scholarLevelGraduateen
uws.typeOfResourceTexten

Files

Original bundle

Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Turcotte_Alexi.pdf
Size:
438.96 KB
Format:
Adobe Portable Document Format
Description:

License bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
6.08 KB
Format:
Item-specific license agreed upon to submission
Description: