FunTAL: mixing a functional language with assembly.

Daniel Patterson, Jamie Perconti, Christos Dimoulas, Amal Ahmed.

To appear in Programming Language Design and Implementation (PLDI) 2017.

paper and technical appendix.

We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting compositional reasoning about the mix. A central challenge in developing such a multi-language is how to bridge the gap between assembly, which is staged into calls to continuations, and high-level code, where subterms return a result. We present a compositional stack-based typed assembly language that supports components, comprised of one or more basic blocks, that may be embedded in high-level contexts. We also present a logical relation for FunTAL that supports reasoning about equivalence of high-level components and their assembly replacements, mixed-language programs with callbacks between languages, and assembly components comprised of different numbers of basic blocks.


Artifact: a FunTAL type checker and small-step machine.

Daniel Patterson and Gabriel Scherer.

Source code and build instructions: github.com/dbp/funtal

We present a type checker and stepper for the FunTAL machine semantics. We include well-typed, runnable examples from the paper, as well as a few smaller examples to start with. With our artifact, you write programs and then type check / load them into a FunTAL machine. You can then step forward and backwards through the evaluation. At each step, the machine shows the registers, stack, and heap, as well as the redex and the context.

Important: the programs entered into the editor should be Fun programs at the top; a pure TAL component C can be embedded as FT[t,?]C where t is the return type, as we see in examples below. We do this so that all programs run through the stepper have a return value.

Note: there are some syntactic differences from the presentation in the paper, which nonetheless we expect will be the primary reference for the language. These changes were made to eliminate the necessity of unicode, reduce ambiguity in the grammar, and make the type checking algorithm syntax-directed. We summarize these changes at the bottom of this page.

Examples from paper:

Additional examples: Import | Simple call | Omega | Mutable reference

Examples with errors:


Registers:

          
Stack:

          
Redex:

          
Context/Result:

          
Heap:

        


Syntactic differences from the paper:

PaperArtifactDescription
(ι; ..., l → h, ...) ([instr; ...],[l -> h, ...]) TAL components use brackets around instructions and the heap fragment.
τFT e FT[t,s] e FT (Fun outside, TAL inside) boundary specifies the type s that the stack has after running e.
τFT e FT[t,?] e FT boundaries can use ? to indicate that running e will not modify the type of the stack (though values may be modified), allowing s to be inferred.
import r,σTFτ e import r1, s as z, t TF{e}; import binds the stack s on return as z with Fun expression e of type t.
α, ζ, ε a1, z21, e5 TAL type variables must begin with a, stack variables with z, and return marker variables with e.
· | τ :: ... :: | t :: ... :: Empty stack prefixes (in protect, stack modifying lambdas) are written as ::, and stack prefixes end with ::.
∀, μ, λ, ∃, • forall, mu, lam, exists, * Greek letters and quantifiers are replaced by english keywords.
* The concrete stack symbol is written *.
u[ω] u[ω, ω...] TAL instantiation is n-ary. (This was mentioned as syntactic sugar.)
{χ; σ}q {χ; σ} q The return marker superscript is just written in line.
λφφ(x:τ...).t lam[φ][φ](x:τ...).e,
(τ...) [φ] -> [φ] τ
The stack prefixes of stack-modifying functions are bracketed, in line.
unpack <α, rd> u unpack <α, rd>, u The TAL instruction unpack has comma-separated argument, for consistency with other instructions.
l -> <1, 2>,
l' -> (code[δ]...)
[l -> ref <1, 2>,
 l' -> box (code[δ]...)]
Heap values are preceded by an explicit mutability marker box or ref.