A Linear First-Order Functional Intermediate Language for Verified Compilers
- First Online:
Abstract
We present the linear first-order intermediate language IL for verified compilers. IL is a functional language with calls to a nondeterministic environment. We give IL terms a second, imperative semantic interpretation and obtain a register transfer language. For the imperative interpretation we establish a notion of live variables. Based on live variables, we formulate a decidable property called coherence ensuring that the functional and the imperative interpretation of a term coincide. We formulate a register assignment algorithm for IL and prove its correctness. The algorithm translates a functional IL program into an equivalent imperative IL program. Correctness follows from the fact that the algorithm reaches a coherent program after consistently renaming local variables. We prove that the maximal number of live variables in the initial program bounds the number of different variables in the final coherent program. The entire development is formalized in Coq.
1 Introduction
We study the intermediate language IL for verified compilers. IL is a linear functional language with calls to a nondeterministic environment.
We are interested in translating IL to a register transfer language. To this end, we give IL terms a second, imperative interpretation called IL/I. IL/I interprets variable binding as assignment, and function application as goto, where parameter passing becomes parallel assignment.
For some IL terms, the functional interpretation coincides with the imperative interpretation. We call such terms invariant. We develop an efficiently decidable property we call coherence that is sufficient for invariance. To translate IL to IL/I, translating to the coherent subset of IL suffices, i.e. the entire translation can be done in the functional setting.
Inspired by the correspondence between SSA [8] and functional programming [2, 10], we formulate a register assignment algorithm [9] for IL and show that it realizes the translation to IL/I. For example, the algorithm translates program (a) in Fig. 1 to program (b). Correctness follows from two facts: First, register assignment consistently renames program (a) such that the variable names correspond to program (b). Second, program (b) is coherent, hence let binding and imperative assignment behave equivalently. Parameter passing in IL/I can be eliminated by inserting parallel assignments [9]. In program (b), all parameters i, n can simply be removed, as they constitute self-assignments.
A key property of SSA-based register assignment is that the number of imperative registers required after register assignment is bounded by the maximal number of simultaneously live variables [9], which allows register assignment to be considered separate from spilling. We show that our algorithm provides the same bound on the number of different variable names in the resulting IL/I term.
1.1 Related Work
Correspondences between imperative and functional languages were investigated already by Landin [11]. The correspondence between SSA and functional programming is due to Appel [2] and Kelsey [10] and consists of a translation from SSA programs to functional programs in continuation passing style (CPS) [1, 15]. Chakravarty et al. [6] reformulate SSA-based sparse conditional constant propagation on a functional language in administrative normal form (ANF) [16]. Our intermediate language IL is in ANF, and a sub-language (up to system calls) of the ANF language presented in Chakravarty et al. [6].
Two major compiler verification projects using SSA exist. CompCertSSA [3] integrates SSA-based optimization passes into CompCert [13]. VeLLVM [17, 18] is an ongoing effort to verify the production compiler LLVM [12]. Both projects use imperative languages with \(\phi \)-functions to enable SSA, and do not consider a functional intermediate language. As of yet, neither of the projects verifies register assignment in the SSA setting. In the non-SSA setting, a register allocation algorithm, which also deals with spilling, has been formally verified [5].
Beringer et al. [4] use a language with a functional and imperative interpretation for proof carrying code. They give a sufficient condition for the two semantics to coincide which they call Grail normal form (GNF). GNF requires functions to be closure converted, i.e. all variables a function body depends on must be parameters.
Chlipala [7] proves correctness for a compiler from Mini-ML to assembly including mutable references, but without system calls. Register assignment uses an interference graph constructed from liveness information. Chlipala restricts functions to take exactly one argument and requires the program to be closure converted prior to register assignment. This means liveness coincides with free variables and values shared or passed between functions reside in an (argument) tuple in the heap: Effectively, register assignment is function local. Chlipala does not prove bounds on the number of different variables used after register assignment and does not investigate the relationship to \(\alpha \)-equivalence.
1.2 Contributions and Outline
We formally define the functional intermediate language IL and its imperative interpretation, IL/I. We establish the notion of live variables via an inductive definition. We identify terms for which both semantic interpretations coincide via the decidable notion of coherence.
Inspired by SSA-based register allocation, we formulate a register assignment algorithm for IL and prove that it realizes an equivalence preserving transformation to IL/I. We show the size of the maximal live set bounds the number of names after register assignment.
All results in this paper have formal Coq proofs, and the development is available online (see Sect. 9). We omit proofs in the paper for space reasons. An extended version is available [DBLP:journals/corr/SchneiderSH15].
The paper is structured as follows: We introduce the functional language IL in Sect. 2 and the imperative language IL/I in Sect. 3. Program equivalence is defined in Sect. 4. We define invariance in Sect. 5, establish a notion of live variables in Sect. 6, and present coherence in Sect. 7. Register assignment is treated in Sect. 8.
2 IL
Values, Variables, and Expressions. We assume a set \(\mathbb {V}\) of values and a function \(\beta :\mathbb {V}\rightarrow \{0,1\}\) that we use to simplify the semantic rule for the conditional. By convention, v ranges over \(\mathbb {V}\). We use the countably-infinite alphabet \(\mathcal {V}\) for names x, y, z of values, which we call variables.
We assume a type \( Exp \) of expressions. By convention, e ranges over \( Exp \). Expressions are pure, their evaluation is deterministic and may fail, hence expression evaluation is a function \(\left[ \!\left[ \cdot \right] \!\right] \,: Exp \rightarrow (\mathcal {V}\rightarrow \mathbb {V}_{\bot })\rightharpoonup \mathbb {V}_{\bot }\). Environments are of type \(\mathcal {V}\rightarrow \mathbb {V}_{\bot }\) to track uninitialized variables. We assume a function \({\text {fv}}: Exp \rightarrow set \,\mathcal {V}\) such that for all environments \(V,V'\) that agree on \({\text {fv}}(e)\) we have \(\left[ \!\left[ e\right] \!\right] \,V=\left[ \!\left[ e\right] \!\right] \,V'\). We lift \(\left[ \!\left[ \cdot \right] \!\right] \,\) pointwise to lists of expressions in a strict fashion: \(\left[ \!\left[ \overline{e}\right] \!\right] \,\) yields a list of values if none of the expressions in \(\overline{e}\) failed, and \(\bot \) otherwise.
Syntax. IL is a functional language with a tail-call restriction and system calls. IL syntactically enforces a first-order discipline by using a separate alphabet \(\mathcal {F}\) for names f, g of function type, which we call labels. IL uses a third alphabet \(\mathcal {A}\) for names \(\alpha \) which we call actions. The term \(\mathsf{let }\,x=\alpha \,\mathsf{in }\,\ldots \) is like a system call \(\alpha \) that non-deterministically returns a value. The formal development treats system calls with arguments. Their treatment is straightforward and omitted here for the sake of simplicity.
A closure is a tuple \((V,\overline{x},s)\in \mathcal {C}\) consisting of an environment V, a parameter list \(\overline{x}\), and a function body s. Since a function f in a context \(F;f:\ldots ;F'\) can refer to function definitions in F (and to itself), the first-order restriction allows the closures to be non-recursive: function closures do not need to close under labels. An application \(f \overline{e}\) causes the function context F to rewind to \(F^f\), i.e. up to the definition of f (rule \(\textsc {App} \)). In contrast to higher-order formulations, we do not define closures mutually recursively with the values of the language.
A system call\(\mathsf{let }~x=\alpha \,~\mathsf{in }~s\) invokes a function \(\alpha \) of the system, which is not assumed to be deterministic. This reflects in the rule \(\textsc {Extern} \), which does not restrict the result value of the system call other than requiring that it is a value. The semantic transition records the system call name \(\alpha \) and the result value v in the event \(v=\alpha \).
IL is linear in the sense that the execution of each term either passes control to a strict subterm, or applies a function that never returns. This ensures no run-time stack is required to manage continuations. While, by contrast, uses sequentialization ; to manage a stack of continuations.
3 Imperative Interpretation of IL: IL/I
4 Program Equivalence
To relate programs from different languages, we abstract from a configuration’s internal behavior and only consider interactions with the environment (via system calls) and termination behavior. IL’s reduction relation forms a labeled transition system (LTS) over configurations.
Definition 1
4.1 Partial Traces
Definition 2
(Trace Equivalence).\(\sigma \simeq \sigma ' :\!\iff \mathcal {P}{\sigma }=\mathcal {P}{\sigma '}\)
Lemma 1
\(\sigma \) silently diverges if and only if \(\mathcal {P}{\sigma }=\{\epsilon \}\).
4.2 Bisimilarity
We give a sound and complete characterization of trace equivalence via bisimilarity. Bisimilarity enables coinduction as proof method for program equivalence, which is more concise than arguing about traces directly. We say a configuration \(\sigma \) is ready if the next step is a system call. We write \(\sigma _2 \mathop {\leadsto }\limits ^{R}\sigma _1\) for \(\forall \sigma _1', \sigma _1\mathop {\longrightarrow }\limits ^{\phi }\sigma _1' \Rightarrow \exists \sigma '_2, \sigma _2\mathop {\longrightarrow }\limits ^{\phi }\sigma _2' \wedge \sigma _1'\mathrel {R}\sigma _2'\). We write \(\sigma \Downarrow _{}{w}\) (where \(w\in \mathbb {V}_{\bot }\)) if \(\sigma \longrightarrow ^*\sigma '\) such that \(\sigma '\) is \(\longrightarrow \)-terminal and \( res (\sigma ')=w\).
Definition 3
Bisim-Silent allows to match finitely many steps on both sides, as long as all transitions are silent. This makes sense for IDRS, but would not yield a meaningful definition otherwise. Bisim-Silent ensures that every external transition of \(\sigma _1'\) is matched by the same external transition of \(\sigma _2'\), and vice versa. This ensures that if two programs are in relation, they react to every possible result value of the external call in a bisimilar way. The premises that \(\sigma _1',\sigma _2'\) are ready is there to simplify case distinctions by ensuring that the next event cannot be \(\tau \).
Theorem 1
(Soundness and Completeness). Let \((S, \mathcal {E}, \mathop {\longrightarrow }\limits ^{}_{}, res , \tau )\) be an IDRS and \(\sigma , \sigma ' \in S\). Then: \( \sigma \sim \sigma ' ~\iff ~ {\sigma }\simeq {\sigma '} \)
The semantics of IL and of IL/I each forms an IDRS. We define \( res \) such that \( res (\sigma )=v\) if \(\sigma \) is of the form (F, V, e) and \(\left[ \!\left[ e\right] \!\right] \,V=v\). Otherwise, \( res (\sigma )=\bot \). The definitions for IL/I are analogous. To relate configurations IL to IL/I, we form a reduction system on the sum \(\varSigma _F + \varSigma _I\) of the configurations and lift \(\longrightarrow \) and \( res \) accordingly. It is easy to see that the resulting reduction system is internally deterministic. If not clear from context, we use an index \(\sigma _F\), \(\sigma _I\) to indicate which language a configuration belongs to.
5 Invariance
We call a term invariant if it has the same traces in both the functional and the imperative interpretation.
Definition 4
Invariance is undecidable. We develop a syntactic, efficiently decidable criterion sufficient for invariance, which we call coherence. Coherence simplifies the translation between IL and IL/I.
6 Liveness
A variable x is significant to a program s and a context L, if there is an environment V and a value v such that \((L,V,s)_I\not \simeq (L,V[x\mapsto v],s)_I\). Significance is not decidable, as it is a non-trivial semantic property.
Liveness analysis is a standard technique in compiler construction to over-approximate the set of variables significant to the evaluation of an imperative program. While usual characterizations of live variables rely on data-flow equations [14], we define liveness inductively on the structure of IL’s syntax. To the best of our knowledge, such an inductive definition is not in literature. The inductive definition factorizes the correctness aspect from the algorithmic aspect of liveness analysis.
We embed liveness information in the syntax of IL by introducing annotations for function definitions: The term \(\mathsf{fun }\,f\,\overline{x}\,:\,X\,=s\,\mathsf{in }\,t\) is annotated with a set of variables X.
6.1 Inductive Definition of the Liveness Judgment
Description of the Rules. Live-Op ensures that all variables free in \(\eta \) are live. Every live variable of the continuation s except x must be live at the assignment. We require x to be live in the continuation. Live-Cond ensures that the live variables of a conditional at least contain the free variables of the condition, and the variables live in the consequence and alternative. Live-Exp ensures that for programs consisting of a single expression e at least the free variables of e are live. Live-App ensures that the free variables of every argument are live, and that the globals \(X_1\) of f are live at the call site. Live-Fun records the annotation \(X_1\) as globals for f in \(\varLambda \), ensures that \(X_1\cup \overline{x}\) is a large enough live set for the function body, and that \(X_1\) does not contain parameters of f. The live variables \(X_2\) of the continuation t must be live at the function definition (Fig. 4).
Theorem 2
(Liveness is Decidable). For all \(\varLambda \), X and annotated s, it is efficiently decidable whether \({\varLambda \vdash \mathbf{live }\,{}s:X}\) holds.
The proof of Theorem 2 is constructive and yields an efficient, extractable decision procedure. The decision procedure recursively descends on the program structure, checking the conditions of the appropriate rule in every step.
6.2 Liveness Approximates Significance
LiveCtx1 ensures that X does not contain parameters and that \(X\cup \overline{x}\) is a large enough live set for the function body s under the context \(\varLambda ;f: X\).
We can now formally state the soundness of the live predicate. We prove that if \({{\varLambda \vdash \mathbf{live }\,{}s:X}}\), then \(X\) contains at least the significant variables of s in every context L that satisfies the assumptions \(\varLambda \). We write \(V=_{X}V'\) if V and \(V'\) agree on X, that is if \(\forall x\in {X}, V x = V' x\).
Theorem 3
For every program s, if \({{\varLambda \vdash \mathbf{live }\,{}s:X}}\) and \({{L\,\models \,\varLambda }}\) and \(V=_{X}V'\), then \((L,V,s)_I \simeq (L,V',s)_I\).
7 Coherence
Coherence is a syntactic condition that ensures that a program is invariant. Coherence is defined relative to liveness information \({{\varLambda \vdash \mathbf{live }\,{}s:X}}\).
7.1 Inductive Predicate
Description of the Rules.Coh-Op deals with binding a variable x. Every function that has x as a global (i.e. \(x\in \varLambda f\)) becomes unavailable, and must be removed from \(\varLambda \). We write \(\lfloor \varLambda \rfloor _{X}\) to remove all definitions from \(\varLambda \) that require more globals than \(X\). Trivally, \(\lfloor \varLambda \rfloor _{\mathcal {V}}=\varLambda \). To remove all definitions from \(\varLambda \) that use x as global, we use \(\lfloor \varLambda \rfloor _{\mathcal {V}\setminus \{x\}}\).
Coh-App ensures only available functions can be applied, since \(\varLambda \) maps functions that are not available to \(\bot \). Coh-Fun deals with function definitions. When the definition of a function f is encountered, its globals X according to the annotation are recorded in \(\varLambda \). In the function body s, only functions that require at most X as globals are available, so the context is restricted to \(\lfloor \varLambda ;f:X\rfloor _{X}\).
Theorem 4
(Coherence is Decidable). For all \(\varLambda \) and annotated s, it is efficiently decidable whether \(\varLambda ~\vdash \mathbf{coh }\,{}s\) holds.
7.2 Coherent Programs are Invariant
Given a configuration (F, V, t) such that \(F f = (V', \overline{x}, s)\), the agreement invariant describes a correspondence between the values of variables in the function closure \(V'\) and the environment V. If the closure of f is available, the closure environment \(V'\) agrees with the primary environment V on f’s globals X: \({V' =_{X} V}\). We write \(F,V\models \varLambda \) if \(\forall f\in \textit{dom} \,{F}\cap \textit{dom} \,{\varLambda },~ V' =_{X} V\) (where \(\varLambda f = X\) and \(F f = (V',\overline{x}, s)\)).
CohC-Con encodes two requirements: First, the body of f must be coherent under the context restricted to the globals \(X\) of f (cf. Coh-Fun). Second, \(X\cup \overline{x}\) must suffice as live variables for the function body s under some assumptions \(\varLambda '\) such that \(\varLambda ;f:X\) approximates \(\varLambda '\). Approximation ensures stability under restriction: \(\varLambda \vdash \mathbf{coh }\,{}F\Rightarrow \lfloor \varLambda \rfloor _{X}\vdash \mathbf{coh }\,{}F\).
We define \( strip (V,\overline{x},s)~=~(\overline{x},s)\) and lift \( strip \) pointwise to contexts.
Theorem 5
(Coherence Implies Invariance). Let \(\varLambda ~\vdash \mathbf{coh }\,{}s\) and \(\varLambda \vdash \mathbf{coh }\,{}F\) and \({\varLambda '\vdash \mathbf{live }\,{}s:X}\) such that \(\varLambda \preceq \varLambda '\). Then for all \(V=_{X}V'\) such that \(F,V\models \varLambda \), it holds \((F,V,s)_F\simeq ( strip \,F, V', s)_I\).
Theorem 5 reduces the problem of translating between IL/I and IL to the problem of establishing coherence. For the translation from IL to IL/I, it suffices to establish coherence while preserving IL semantics. Since SSA and functional programming correspond [2, 10], the translation from IL/I to IL can be seen as SSA construction [8], and the translation from IL to IL/I, which we treat in the next section, as SSA destruction.
8 Translating from IL/F to IL/I via Coherence
The simplest method to establish coherence while preserving IL semantics is \(\alpha \)-renaming the program apart. A renamed-apart program (for formal definition see [DBLP:journals/corr/SchneiderSH15]) is coherent, since every function is always available. The properties of \(\alpha \)-conversion ensure semantic equivalence.
- 1.
We define the notion of local injectivity for a function \(\rho :\mathcal {V}\rightarrow \mathcal {V}\). We show that renaming with a locally injective \(\rho \) yields an \(\alpha \)-equivalent and coherent program \(\rho \,s\).
- 2.
We give an algorithm \( rassign \) and show that it constructs a locally injective \(\rho \) that uses the minimal number of different names.
We introduce more liveness annotations before every term in the syntax, i.e. wherever a term s appeared before, now a term \(\langle X \rangle \,s\) appears that annotates s with the set X. From now on, \(s,t\) range over such annotated terms. We define the projection \([\langle X \rangle \,s]=X\). The annotation corresponds directly to the live set parameter \(X\) of the relation \({\varLambda \vdash \mathbf{live }\,{}s:X}\), hence it suffices to write \({\varLambda \vdash \mathbf{live }\,{}s}\) for annotated programs.
8.1 Local Injectivity
- (1)
The program must be without unreachable code, i.e. in every subterm \(\mathsf{fun }\,f\,\overline{x}=s\,\mathsf{in }\,t\) it must be the case that f is applied in t.
- (2)
A variable in \(\mathcal {V}_B(s)\) must not occur in a set of globals in \(\varLambda \). We define \(\varLambda \subseteq {U}~:\!\iff ~\forall {f}\in \textit{dom} \,\varLambda ,~\varLambda \,f\subseteq {U}\).
- (3)
A variable in \(\mathcal {V}_B(s)\) must not occur in the annotation [s]. We write \(s\subseteq {U}\) if for every subterm t of s it holds that every \(x\in [t]\) is either in U or bound at t in s.
For renamed-apart programs, these conditions ensure that the live set X in Inj-Fun always contains the globals \(X_1\) of f (cf. Live-App).
Theorem 6
Theorem 6 states that the renamed program \(\rho \,s\) is coherent under the assumptions \(\rho ~(\lfloor \varLambda \rfloor _{[s]})\), i.e. the point-wise image of \(\lfloor \varLambda \rfloor _{[s]}\) under \(\rho \).
Renaming with a locally injective renaming produces an \(\alpha \)-equivalent program (for formal definition see [DBLP:journals/corr/SchneiderSH15]), and hence preserves program equivalence:
Theorem 7
Let \(s\) be a renamed-apart program without unreachable code such that \({\varLambda \vdash \mathbf{live }\,{}s}\), \(\varLambda \subseteq {\text {fv}}(s)\) and \(s\subseteq {\text {fv}}(s)\). Let \({\rho },{d}:\mathcal {V}\rightarrow \mathcal {V}\) such that \({\rho }\) is the inverse of \({d}\) on \({\text {fv}}(s)\). Then \(\rho \vdash {{\varvec{inj}}}\, {{\varvec{s}}}~\Longrightarrow \,~{{\rho },{d}\vdash \rho \,s \,\sim _\alpha \, s}\)
8.2 A Simple Register Assignment Algorithm
We prove in Theorem 8 that the algorithm is correct for any choice of \({ fresh }\) and \( freshlist \), as long as they satisfy the specifications above.
Theorem 8
Let s be renamed-apart such that \({\varLambda \vdash \mathbf{live }\,{}s}\), \(\varLambda \subseteq {\text {fv}}(s)\) and \(s\subseteq {\text {fv}}(s)\). Let \(\rho \) be injective on [s]. Then: rassign \(\rho \,{{\varvec{s}}}\,\vdash \,{{\varvec{inj}}}\,{{\varvec{s}}}\).
Our implementation of fresh implements the heuristic of simply choosing the smallest unused variable. Theorem 9 shows that for this choice of \({ fresh }\), the largest live set determines the number of required names. We use \(\mathcal {S}(k)\) to denote the set of the k smallest variables, and \(\mathcal {V}_O(s)\) to denote the set of variables occurring (free or in a binding position) in s.
Theorem 9
Assume \({ fresh }\,X\) yields a variable less or equal to |X|. Let \(s\) be renamed-apart such that \({\varLambda \vdash \mathbf{live }\,{}s}\), \(\varLambda \subseteq {\text {fv}}(s)\) and \(s\subseteq {\text {fv}}(s)\). Let k be the size of the largest set of live variables in \(s\), and \( rassign \,\rho \,s = \rho '\). If \(\rho ({\text {fv}}(s)) \subseteq \mathcal {S}(n)\) then \(\rho ' (\mathcal {V}_O(s)) \subseteq \mathcal {S}( max \{n,k\})\).
We prove a slightly generalized version of Theorem 9 by induction on s.
9 Formal Coq Development
Each theorem and lemma in this paper is proven as part of a larger Coq development, which is available online1. The development extracts to a simple compiler that, for instance, produces program (b) when given program (a) from the introduction as input.
The formalization uses De-Bruijn representation for labels, and named representation for variables. Notable differences to the paper presentation concern the treatment of annotations, the technical realization of the definition of liveness, and the inductive generalizations of Theorems 6–9.
10 Conclusion
We presented the functional intermediate language IL and developed the notion of coherence, which provides for a canonical and verified translation between functional and imperative programs. We formulate a register assignment algorithm by recursion on the structure of IL that achieves the same bound on the number of required registers as SSA-based register assignment. Coherence allowed us to justify correctness without directly arguing about program semantics by proving that the algorithm \(\alpha \)-renames to a coherent program.
Acknowledgments
This research has been supported in part by a Google European Doctoral Fellowship granted to the first author.