Submitted in partial fulfillment of the requirements
for the degree of Doctor of Philosophy

Khoury College of Computer Sciences
Northeastern University
Boston, MA

Abstract

The success of just-in-time compilers is based on their ability to specialize code at run time. It allows them to dynamically observe the execution of a program and optimize code for properties of the current program state. Just-in-time compilation is the blackest of arts in language implementation; the initiation rituals include brutal debugging sessions and an oath to pierce all abstractions. While I enjoy flipping bits, I still believe that at least some of the suffering is avoidable and building just-in-time compilers could be a topic as precisely documented as any. Hence, a main motivation for writing this dissertation is to digest some of this black magic and capture it in simple and precise terms. This includes the following contributions:

• A calculus featuring a precise description of speculative optimizations with dynamic deoptimization.
• Context dispatch, a generic approach for specializing code up to a context of dynamically checked assumptions.
• A case study of a realistic language implementation following these implementation recipes, featuring an intermediate representation to analyze and compile R programs.

This dissertation consists of two parts. First, the models and theoretical findings are presented. The goal of that part is to explain how and why dynamic optimizations work, how dynamic information can be used for optimizations, and how assumptions interact in with static compiler optimizations. Additionally, it is discussed how the models combine and how complete they are with regards to a full-blown language implementation. Secondly, Ř is described and evaluated. Ř is an implementation of the R language, following the recipes introduced by the first part. This allows us to connect and evaluate the designs with a realistic implementation.

Acknowledgments

Along the way many, many people helped me shape raw curiosity into a useful tool and empowered me to write this dissertation.

Most importantly, my heartfelt thanks for the unconditional support go to my adviser, Jan Vitek. I will truly miss the joy of working with you.

Many thanks to my plentiful and awesome co-authors and co-conspirators, including Aurèle Barrière, Guido Chari, Aviral Goel, Jakob Hain, Jan Ječmen, Filip Křikava, Sebastián Krynski, Paley Li, Petr Maj, Gabriel Scherer, Andreas Wälchli, Ming-Ho Yee.

Without the encouragement and patience of many mentors I would not have started this endeavor. Most prominently, thank you Toon Verwaest and Oscar Nierstrasz for sending me down this rabbit-hole. Thanks for teaching me everything about compilers and VMs to Daniel Clifford, Tomas Kalibera, Ben Titzer.

I also thank the PLISS attendees, who shall remain anonymous, for openly sharing that every PhD comes with its fair share of doubt and resignation.

Last but not least I am very grateful to my committee for engaging with my work and helping me better understand and explain it. Thank you Amal Ahmed, Mathias Felleisen, Filip Pizlo, and Steve Blackburn. In particular Matthias for your dedication.

Thank you to all the people I love for everything we have and still will experience. See you in the streets.

Olivier Flückiger
August 2022

Contents

Chapter 1
Introduction

Just-in-time compilers are omnipresent in today’s technology stacks. The performance of the code they generate is central to the growing adoption of languages with dynamic features such as code loading, extensible objects, monkey-patching, introspection, or eval. These kind of features render precise static analysis impossible and lead to a wide range of possible behaviors, even in seemingly benign programs. To resolve this issue compilers specialize programs at run-time according to observed behaviors — they identify likely invariants and optimize¹ assuming the invariants hold. For instance,

• in prototype based languages classes of likely similar objects are identified using hidden classes [Chambers and Ungar, 1989],
• duck-typing and late bound call targets are made static by speculating on the stability of the dynamic call-graph and monomorphized by splitting [Hölzle, Chambers, and Ungar, 1991],
• methods are specialized to the types of arguments or other dynamic properties [Bezanson, Chen, Chung, Karpinski, Shah, Vitek, and Zoubritzky, 2018]
• class hierarchies are speculated to be stable [Paleczny, Vick, and Click, 2001],
• dynamic types of variables assumed stable [Hölzle and Ungar, 1994b].

Most optimizations in just-in-time compilers are based in some way on the premise that, from the vast range of possible behaviors only some will be exercised by any particular execution of a program. Specializing code to those particular behaviors has been fundamental in making dynamic languages practical in large applications. These kind of optimizations involve forming assumptions about likely behaviors, that are expected to hold true at run-time. Typically the assumptions are based on profiling data, gathered either from the current process or from previous invocations. This is a common practice, even utilized in ahead-of-time compilers, where it is known as profile guided optimizations. The advantage in a just-in-time scenario is that specialization can be explored lazily, generating only code that is actually needed, in contrast to the ahead-of-time case, where the generated code must handle all possible behaviors all the time. A fundamental problem in just-in-time compilation is therefore how to leverage dynamic analysis, i.e., an incomplete recording of the past behavior, for optimizations? In particular, how to speculate and specialize code for likely invariants, while still safely and efficiently handling the case where they turn out not to hold. The implementation thereof is often scattered around different components of the language implementation; for instance, devirtualization in a language with class loading relies on the interplay of collecting a dynamic call-graph in the runtime, optimizing under the assumption that it is stable and retiring code invalidated by the class loader, while handling the cases where the invalidated code is still being executed.

1.1 Motivation

In this area of run-time optimizations, there is a lack of well-documented and re-usable techniques. Specialization is typically ad-hoc, tied to peculiarities of the language or implementation, and often even distinct for different properties in the same system. For instance the specialization approach taken by Julia [Bezanson, Karpinski, Shah, and Edelman, 2012] requires a language with multi-method dispatch, the one by Truffle [Würthinger, Wimmer, Wöß, Stadler, Duboscq, Humer, Richards, Simon, and Wolczko, 2013] relies on their language implementation style using self-specializing AST interpreters. Speculative optimizations in particular are poorly documented and mistaken for an implementation detail on how to rewrite stack frames. This gap in the literature leads to island-solutions for each language and a reluctance by some language implementers to include speculation in their compiler. The reluctance is the result of a poor understanding of the underlying program transformations and missing off-the shelf techniques.

Speculation in particular is iconic for just-in-time compilation. Having a compiler available at run-time allows for multiple attempts at producing optimal code. This allows for aggressive optimization strategies, where code is expected to be wrongly optimized sometimes, but then subsequently and transparently replaced by updated and fixed code. Speculative optimizations stand out from other techniques by their ability to — at arbitrary program locations — exclude some parts of the source code from the code being optimized. This is achieved by guarding against unexpected behaviors with run-time checks and bailing out of the optimized code, back to the source code, if these guards fail. It follows that speculative optimizations allow us to trim down the vast range of possible behaviors and instead optimize and even analyze just for the expected ones. It also means, that some form of recovery action is necessary in the unexpected case. We refer to that action as deoptimization and it relies on some form of execution state rewriting by the underlying runtime, such as on-stack-replacement or stack-switching.

A non-speculating specialization on the other hand involves upfront splitting of the control-flow on a property. I will refer to them as contextual optimizations, as they specialize code to certain predicates over the program state. Often contextual optimizations result in the duplication of the code being optimized. Real-world examples include multi-method dispatching on argument types in Julia, where each function signature discovered through dispatch leads to a new function being compiled and optimized. Or, optimizations involving tail-duplication, such as message splitting in SELF, where the control-flow within a function is split on the type of a result of a message send to produce optimized continuations for expected dynamic types.

As a concrete example, consider a code fragment S, which is part of a lager program, and shall be specialized to a certain runtime context. For instance the fragment S could have a free variable x and the goal is to provide a particularly fast implementation for, say, the cases where x is 42. A fragment could be a function body, but also a smaller or bigger piece of code. Let’s assume S is the following expression:

For a simple non-speculating optimization we start with a transformation to duplicate the fragment into if (x == 42) then S else S. This allows us to optimize each clone of S independently under the contextual information whether x == 42 holds. Within the then branch, the compiler can assume x == 42 to be part of the static optimization context, and conversely within the else branch x != 42.

Now let us contrast this approach with a speculative optimization. In that case we simply state assert(x == 42); S. For expressions dominated by the assertion, the fact x == 42 is again part of the static optimization context. The case where that assumption does not hold, is not part of the code emitted by such a compiler.

In summary, a speculative optimization means that the compiler can simply assume a likely invariant at a certain program location, and the unexpected case falls outside the compilation unit. Under speculative optimizations we also allow instructions being executed optimistically and work being done that has to be discarded or even reverted if the assumption fails. A non-speculative optimization on the other hand produces code that cannot be invalidated. It is still possible to optimize for dynamic properties, though the properties are used in a non-speculative way.

Example

Consider the following vector access function in R

which converts the y argument to a number and then uses that number as an index into argument x. Assume we call the function with three different kinds of arguments as follows:

In the first two cases the type of the argument is known at the call site. This does not hold for the third case, because R evaluates arguments by need; pos() is only invoked, when the y argument is accessed for the first time, which happens during the execution of at. If we were to clone the function at and optimize it for different types of arguments, we can specialize it for three distinct cases: number[n] × number for the call-site at line 3, number[n] × string at line 5, and number[n] × any at line 8. The first two signatures directly lead to well optimized versions — at the source level they would look like:

The third case does not lend itself to any useful optimizations, since at the call-site it is unclear what the expression pos() eventually returns (excluding inter-procedural analysis for now). This is where speculation comes into play, and type-feedback from previous runs can be employed to narrow down the behavior to what we expect from the past. To make lazy evaluation specific, we’ll mark the position where arguments are evaluated with force. After forcing the argument expression, we can then speculate on its type and shape:

In case our assumptions are wrong, the assume instruction is supposed to fall back to the source version of this function. It allows us to ignore unlikely cases, i.e., in this case most of the implementation of vector access, which would have to deal with different vector types, indexing modes and possible errors. Of course for that to actually work, assume is more complicated than an assertion and more meta-data is required than is shown here.

Questions

An efficient implementation of a dynamic language must use information only available at run-time to optimize code. In particular this information is incomplete and changes over time. There are fundamentally two approaches to this problem, one is to speculate on likely properties and fall-back otherwise, the other is to somehow split control-flow on properties, which are checked up-front. Both of these approaches present problems and open questions.

Speculation

Specialization

1.2 Thesis

This dissertation presents a framework for soundly injecting assumptions into the optimizer of a just-in-time compiler. First, speculative optimizations with deoptimization as fallback mechanism are formalized in the sourir model. Sourir’s assume instruction enables optimizations based on arbitrary assumptions at any point. Second, context dispatch provides a generic approach for splitting on properties checked at run-time. Context dispatch allows to optimize functions lazily, up to the actually encountered contexts of assumptions, which act like static optimization contexts in an ahead-of-time compiler. I will defend the thesis that

To understand that statement I will briefly introduce the two models, summarize their contributions, and explicit the claims.

Sourir

chapter 2

• a semantic for deoptimization points, assumptions, deoptimization metadata, and the key invariants required for speculative optimizations;
• correctness proofs for speculative optimizations and classical optimizations in the presence of speculation; and
• the assume instruction for speculation that can be easily integrated in a compiler IR.

Context Dispatch

chapter 3

• add dynamic information to the static optimization context of a compiler and combine static and dynamic analysis for specialization;
• avoid over-specializing and support sharing of code; and
• efficiently dispatch to an optimal version under the current program state.

Sourir and context dispatch complement each other. I will also introduce a combined deoptless deoptimization strategy using context dispatch.

Claims

chapter 4

• The two approaches provide specializations on dynamic information in all important situations. The optimizing compiler in Ř uses dynamic information only in the form of assume instructions or optimization contexts from context dispatch. This claim is substantiated in chapter 4, which describes how sourir and context dispatch translate into the concrete implementation and how this implementation relies only on these two mechanisms for incorporating dynamic information.
• The optimizer is competitive. It significantly outperforms the Ř bytecode interpreter, the GNU R bytecode interpreter, and is comparable to Oracle’s JIT compiling FastR, but with faster warmup behavior. The performance evaluation in chapter 5 shows which assumptions and contexts are required for Ř to speed up R programs.

Non-Claims

Structure

This thesis is structured as follows. The two main contributions are presented in chapter 2 and chapter 3. The former presents a formalization of speculative optimizations and discusses the relationship of the model with implementations. The latter focuses on specialization using context dispatch and related applications. To validate my claims chapter 4 presents how these contributions are usable in a real-world implementation called Ř and chapter 5 shows that Ř is competitive. chapter 6 concludes and presents future work.

Publications

The Ř virtual machine is available and developed as free software at ř-vm.net.

The text of this dissertation is based or borrows from the following peer-reviewed publications:

• Correctness of speculative optimizations with dynamic deoptimization
  [Flückiger, Scherer, Yee, Goel, Ahmed, and Vitek, 2018] (POPL)
• R melts brains: an IR for first-class environments and lazy effectful arguments
  [Flückiger, Chari, Jecmen, Yee, Hain, and Vitek, 2019] (DLS)
• Sampling Optimized Code for Type Feedback
  [Flückiger, Krynski, Wälchli, and Vitek, 2020c] (DLS)
• Contextual Dispatch for Function Specialization
  [Flückiger, Chari, Yee, Jecmen, Hain, and Vitek, 2020b] (OOPSLA)
• Formally Verified Speculation and Deoptimization in a JIT Compiler
  [Barrière, Blazy, Flückiger, Pichardie, and Vitek, 2021] (POPL)
• Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations
  [Flückiger, Ječmen, Krynski, and Vitek, 2022b] (PLDI)

The experimental setup for various performance results can be reproduced by the following artifacts:

• Artifact of “Contextual Dispatch for Function Specialization”
  [Flückiger, Chari, Yee, Jecmen, Hain, and Vitek, 2020a] (OOPSLA)
• Artifact of “Deoptless: Speculation with Dispatched On-Stack Replacement and Specialized Continuations”
  [Flückiger, Jecmen, Krynski, and Vitek, 2022a] (PLDI)

Chapter 2
Assume: Speculation with Deoptimization

Many just-in-time compilers support some form of speculative optimization to avoid generating code for unlikely control-flow paths. For instance the prevalent polymorphism in a dynamic language causes even the simplest code to have non-trivial control flow. Consider the JavaScript snippet (example by Bebenita, Brandner, Fahndrich, Logozzo, Schulte, Tillmann, and Venter [2010]):

Without optimization one iteration of the loop executes 210 instructions; all arithmetic operations are dispatched and their results boxed. If the compiler is allowed to make the assumption it is operating on integers, the body of the loop shrinks down to 13 instructions. As another example, most Java implementations assume that non-final methods are not overridden. Speculating on this fact allows compilers to avoid emitting dispatch code [Ishizaki, Kawahito, Yasue, Komatsu, and Nakatani, 2000]. Newly loaded classes are monitored, and any time a method is overridden, the virtual machine invalidates code that contains devirtualized calls to that method. The validity of speculations is expressed as a predicate on the program state. If some program action, like loading a new class, falsifies that predicate, the generated code must be discarded. To undo an assumption, an implementation must ensure that functions compiled under that assumption are retired. This entails replacing affected code with a version that does not depend on the invalid predicate and, if a function currently being executed is found to contain invalid code, that function needs to be replaced on the fly. In such a case, it is necessary to transfer control to a different version of the function, and in the process, it may be necessary to materialize portions of the state that were optimized away and perform other recovery actions. In particular, if the invalidated function was inlined into another function, it is necessary to synthesize a new stack frame for the caller. This is referred to as deoptimization, or on-stack-replacement, and is found in most industrial-strength compilers.

Speculative optimization gives rise to a large and multi-dimensional design space that lies mostly unexplored. First, compiler writers must decide how to obtain information about program state. This can be done ahead-of-time by profiling, just-in-time by sampling or instrumenting code. Second, they must select which facts to record. This can range from information about the program, its class hierarchy, which packages were loaded, to information about the value of a particular mutable location in the heap. Finally, they must decide how to efficiently monitor the validity of speculations. While some points in this space have been explored empirically, existing systems have done it in an ad hoc manner that is often both language- and implementation-specific, and thus difficult to transfer.

The model shown here has a focused goal. The aim is to demystify the interaction between compiler transformations and deoptimization. When are two versions compiled under different assumptions equivalent? How should traditional optimizations be adapted when operating on code containing deoptimization points? In what ways does deoptimization inhibit optimizations? The assume model gives compiler writers the formal tools they need to reason about speculative optimizations. To do this in a way that is independent of the specific language being targeted and of implementation details relative to a particular compiler infrastructure, we have designed a high-level compiler intermediate representation (IR), named sourir, that is adequate for many dynamic languages without being tied to any one in particular.

A sourir program is made up of functions, and each function can have multiple versions. We equip the IR with a single instruction, named assume, specific to speculative optimization. This instruction has the role of describing what assumptions are being used to perform speculative optimization and what information must be preserved for deoptimization. It tests if those assumptions hold, and in case they do not, transfers control to another, less optimized version of the code. Reifying assumptions in the IR makes the interaction with compiler transformations explicit and simplifies reasoning. The assume instruction is more than a branch: when deoptimizing it replaces the current stack frame with a stack frame that has the variables and values expected by the target version, and, in case the function was inlined, it synthesizes missing stack frames. Furthermore, unlike a branch, its deoptimization target is not considered by the compiler during analysis and optimization. The code executed in case of deoptimization is invisible to the optimizer. This simplifies optimizations and reduces compile time as

the analysis remains local to the version being optimized and the deoptimization metadata is considered to be a stand-in for the target version.

As an example consider the loop from Listing 2.1. A possible translation to sourir is shown in Figure 2.1 (less relevant code elided). V base contains the original version. Helper functions Get and store implement JavaScript (JS) array semantics, and the function add implement JS addition. Version V native contains only primitive sourir instructions. This version is optimized under the assumption that the variable a is an array of primitive numbers, which is represented by the first assume instruction. Further, JS arrays can be sparse and contain holes, in which case access might need to be delegated to a getter function. For this example HL denotes such a hole. The second assume instruction reifies the compiler’s speculation that the array has no holes, by asserting the predicate t ≠ HL . It also contains the associated deoptimization metadata. In case the predicate does not hold, we deoptimize to a related position in the base version by recreating the variables in the target scope. As can be seen in the second assume, local variables are mapped as given by the so called varmap [ i  =  i , j =  i  + 1 ]; the current value of  i  is carried over into the target frame’s  i , whereas variable j has to be recomputed.

To visualize the approach let us consider an abstract graph of the execution. The speculative optimization appears as shown in Figure 2.2, gray boxes representing function versions.

Calling the function invokes the speculatively optimized version. If a dynamic guard fails, then a deoptimization happens, we transfer execution to the target version, into the middle of the function at deopt, discarding the optimized code.

2.1 On-Stack Replacement

Before going into details about how to correctly create and use the assume instruction in the compiler IR, this section takes a step back and presents the underlying implementation techniques and identifies the different pieces in a real-world deoptimization. This includes a preview of how to eventually lower an assume instruction to something a CPU can execute. In general the relevant implementation technique is known as on-stack replacement. OSR refers to an exceptional transfer of control between two versions of a function. It is employed by just-in-time compilers in situations where a function can or has to be replaced at once, without waiting for it to exit normally. To the user, this exchange is not observable, the new function transparently picks up where the old one stopped. On-stack refers to the fact that the involved functions have active stack frames that need to be rewritten. OSR is an umbrella term used in literature and practice to describe exceptional transfer of control for different reasons and using different kind of mappings between stack frames or program states. The term deoptimization and on-stack replacement are often used interchangeably. Although their meanings overlap, we should be more precise in their use.¹ The term deoptimization highlights the fact, that optimizations are being undone. A deoptimization transfers control from a speculatively optimized version with a failing assumption, to a less speculatively optimized version, undoing the failing assumption. On the other hand, the term OSR focuses on the implementation technique, whereby stack-frames are rewritten. OSR can be used for other applications, such as implementing exceptions, or tiering-up, i.e., changing from a less to a more optimized version. Similarly, deoptimization can be implemented without OSR, for instance by relying on a execution environment with support for stack-switching, or simply using tail-calls and lazy replacement. The latter strategy is employed by Ř.

As shown in the previous section, speculative optimizations and in particular deoptimization, needs a way of exiting and entering functions in the middle of execution, with low performance impact on the case where the guards hold. When the guard fails, then instead of continuing normally, the function is exceptionally terminated and replaced with the unoptimized baseline function, as visualized in Figure 2.2. A correct deoptimization requires the system to extract the state of the optimized function, transform it into a corresponding unoptimized state and then materialize it to continue the execution.

Definitions

Figure 2.3

Origin and target do not need to be constrained to a single stack frame and a single function. For example when exiting an inlined function, one origin function maps to multiple target functions. In other words, the stack frame of the origin needs to be split into multiple target stack frames.

OSR has been described as black magic due to the non-conventional control-flow that it introduces. A significant part of the complexity comes from the fact that most implementations do not provide clean abstractions for OSR. For example, extracting and rewriting the program state, i.e., steps (a) and (b) in Figure 2.3, are often not separated cleanly. Both of these two steps provide challenges, but for different reasons. Extracting the program state is challenging due to low-level concerns. We need very fine grained access to the internal state of the computation at the OSR points. This access has to be provided by the backend of our compiler, e.g., by exposing how the execution state is mapped to the hardware or the interpreter. On the other hand, mapping the extracted program state to a target state, i.e., creating a correct varmap, relies on the optimizer providing the required information.

Simplifications

In this architecture, there is only one compiler and one compilation direction between the two ends of the OSR. In other words, the origin code is the source code of this compiler, therefore the mapping takes just one step, from native to bytecode (BC). On the other hand, in the case where both ends of the OSR are compiled from some common source code, the mapping of execution states has two steps, as it needs to pass through the original source. Given the following two compilation tiers:

the second compilation mandates a mapping that lifts the state from an origin (native) state to a source state, the first compilation a mapping that lowers it to a target (BC) state. Therefore, the generic model is important in cases where OSR transitions from optimized to optimized code.

In sourir, the origin and target state of a deoptimization have the same representation. In other words the varmap corresponds to (c), the mapping (b) is the identity, since source and origin are identical. Furthermore (a) and (d) are trivial, since our execution states are semantic states of the sourir IR. This simplification was made to focus on the main problem of creating and maintaining a correct mapping for deoptimization.

Directions

Implementation Choices for OSR-out

Simplified OSR-in

2.2 Contributions and Limitations

We now turn our attention back to the optimizations. From now on this chapter stays at the abstraction level of a compiler intermediate representation. In that representation we develop notions and techniques to correctly produce and maintain the mapping (c) from Figure 2.3. We prove the correctness of a selection of traditional compiler optimizations in the presence of speculation; these are constant propagation, unreachable code elimination, and function inlining. The main challenge for correctness is that the transformations operate on one version in isolation and therefore only see a subset of all possible control flows. We show how to split the work to prove correctness between the pass that establishes a version-to-version correspondence and the actual optimizations. Furthermore, we introduce and prove the correctness of three optimizations specific to speculation, namely unrestricted deoptimization, predicate hoisting, and assume composition.

Our work makes several simplifying assumptions. We ignore the issue of generation of versions: we study optimizations operating on a program at a certain point in time, on a set of versions created before that time. We do not model the low-level details of code generation. Sourir is not designed for implementation, but about reasoning support for existing or new JIT implementations.

Most importantly, in sourir the origin and target state of a deoptimization have the same representation. This simplification was made to focus on the main problem of mapping the states. For an actual implementation the target state most likely has a different representation. For instance in Ř, and similarly in Java, the target is the bytecode interpreter. In other words deoptimization materializes program states of an interpreter — the deoptimization target is a bytecode offset, the target values are placed on the operand stack of the interpreter, and so on. We refer to chapter 4 for an example of how to bridge this gap. If we compare the varmaps of this implementation with the sourir model, then what changes are the left-hand sides of the mapping. Instead of creating a sourir environment of local variables, the target state for instance consists of an operand stack. For instance, instead of [ i  =  i , j =  i  + 1 ], the varmap might be [ stack  = ⟨i , i  + 1 ⟩]. Since the optimizer operates only on the right-hand sides of the varmaps, the changes affect only the front-end of the full compiler and do not affect the results from this chapter.

Finally, the assume IR might be lowered to some more optimized execution format, say a native binary. Lowering assume instructions is outside the scope of this chapter. The issues in doing so are similar to lowering a call instruction, but often great additional care is taken for the instruction to have as little overhead as possible if the guarding condition holds, as we expect this to be the default case. How the proofs can be extended to include native code is future work.

2.3 Related Work

OSR for deoptimization was pioneered in SELF by Hölzle, Chambers, and Ungar [1992]. At first, the idea was simply to deoptimize code to provide a source-level debugging experience. In that sense, it was a speculative optimization on the assumption that debugging is not used. Soon the idea was applied to speculatively optimize for all kinds of assumptions, from the stability of class hierarchies [Paleczny et al., 2001] to unlikely behavior in general [Burke, Choi, Fink, Grove, Hind, Sarkar, Serrano, Sreedhar, Srinivasan, and Whaley, 1999], and providing more and more flexibility to the optimizer in the presence of deoptimization [Soman and Krintz, 2006]. We are reaching the point where deoptimization is an off-the-shelf technique that more and more compilers are relying on for diverse purposes [Odaira and Hiraki, 2005, Schneider and Bolz, 2012, Duboscq, Würthinger, and Mössenböck, 2014, Stadler, Welc, Humer, and Jordan, 2016, Ap and Rohou, 2017, Qunaibit, Brunthaler, Na, Volckaert, and Franz, 2018, Pizlo, 2014]. The common idea is that deoptimization leads the control-flow back to less optimized code. Most modern just-in-time compilers rely on speculative compilation to generate code for a subset of the possible behaviors of a function. The drawback of speculation is that it does not scale well with very dynamic behavior, as the speculation applies indiscriminately. Another drawback of speculation is that deoptimization is costly, as the compiler needs to add and maintain safe-points which inhibit some optimizations.

OSR-in (i.e., using OSR to transition from a less to a more optimized version) was first described by Hölzle and Ungar [1994a] in their recompilation strategy. When a small function is invoked often, they rather recompile the caller and replace it using OSR-in. SELF, being an interactive system, was concerned with compilation pauses. Especially with splitting-based optimizations that could lead to an explosion of code size. Chambers and Ungar [1991] address this issue by identifying uncommon source-level control-flows and deferring their compilation. Suganuma, Yasue, and Nakatani [2003] describe the natural extension of this idea where the deferred compilation is implemented by means of OSR. The Jikes RVM extensively relied on OSR-in for profile-driven deferred compilation as described by Fink and Qian [2003]. Deferred compilation can be understood as a speculative optimization that assumes an unlikely source-level branch is not taken.

Several works discuss implementation challenges and ease of use with regards to OSR. Duboscq, Würthinger, Stadler, Wimmer, Simon, and Mössenböck [2013] present how deoptimization points and metadata are implemented in the Graal compiler IR. Lameed and Hendren [2013], Kedlaya, Robatmili, Cas caval, and Hardekopf [2014], D’Elia and Demetrescu [2016] provide frameworks for supporting OSR in LLVM.

Most compilers use an architecture, where OSR transitions are only possible between versions linked by one compilation step. A notable exception are Wimmer, Jovanovic, Eckstein, and Würthinger [2017] who present OSR from optimized to optimized code. The goal is to use an optimizing compiler as the baseline compiler. They note that it requires “a two-way matching of two scope descriptors describing the same abstract frame.” In terms of our definitions in the previous section, this corresponds to an origin and a target state, which are related through a corresponding source state.

On the other hand, the one-step architecture is sometimes further simplified by the optimizer having the same source and target language. For example Béra, Miranda, Denker, and Ducasse [2016] advocate a VM architecture that uses a bytecode-to-bytecode optimizer, or Essertel, Tahboub, and Rompf [2021] implement OSR as source-to-source transformation. Wang, Blackburn, Hosking, and Norrish [2018] argue for a common low-level code format for all optimization levels and a low-level virtual machine, the Mu micro VM [Wang, Lin, Blackburn, Norrish, and Hosking, 2015], to efficiently execute this code. OSR as a mechanism is provided by the virtual machine, e.g.,, by means of a swapstack primitive operation. A similar argument is made by Desharnais and Brunthaler [2021]. As a result OSR is trivial to implement on top of such an architecture, since all the implementation complexity has to be handled already by the lower layer. Note however, that such a one-language approach, while simplifying the implementation, does not simplify the creation of a correct mapping for undoing optimizations. The problem of keeping two versions’ execution states synchronized across optimization passes still applies. That’s why the assume model in this dissertation also makes this one-language simplifying assumption, because it aims to solve the problem of correct mappings in isolation.

Some dynamic languages go to great lengths to avoid introducing speculation and deoptimization at all [Belyakova, Chung, Gelinas, Nash, Tate, and Vitek, 2020].

JIT Correctness

Previous work has made in-roads in demystifying JIT compilation. Myreen [2010] presents a verified JIT compiler from a stack-based bytecode to x86. The work focuses on self-modifying code, which modern JITs typically do not use anymore. The reasons are that for security reasons memory cannot be writable and executable at the same time, plus invalidating instruction caches is an expensive operation. What is not covered by Myreen are compiler optimizations and any kind of speculation, deoptimization, or specialization.

Guo and Palsberg [2011] discussed the soundness of trace-based compilers. When optimizing a trace, the rest of the program is not known to the optimizer, so optimizations such as dead-store elimination are unsound: a store might seem useless in the trace itself, but actually impacts the semantics of the rest of the program. On the other hand, free variables of the trace can be considered constant for the entire trace.

D’Elia and Demetrescu [2018] present an LLVM extension with OSR exit and entry points, and their interaction with optimization passes. Béra et al. [2016] present a verifier for a bytecode-to-bytecode optimizer. By symbolically executing optimized and unoptimized code, they verify that the deoptimization metadata produced by their optimizer correctly maps the symbolic values of the former to the latter at all deoptimization points.

There is a rich literature on formalizing compiler optimizations. The CompCert project [Leroy and Blazy, 2008] for example implements many optimizations, and contains detailed proof arguments for a data-flow optimization used for constant folding that is similar to ours. In fact, sourir is close to CompCert’s RTL language but comes with versions and assumptions. There are formalizations for tracing compilers [Guo and Palsberg, 2011, Dissegna, Logozzo, and Ranzato, 2014], but we are unaware of any other formalization effort for speculative optimizations in general.

2.4 Speculation in a Nutshell

This section introduces our IR and its design principles. We first present the structure of programs and the assume instruction. Then, the following subsections explain how sourir maintains multiple equivalent versions of the same function, each with a different set of assumptions to enable speculative optimizations. All concepts introduced in this and the next section are formalized in section 2.6.

Sourir is an untyped language with lexically scoped mutable variables and first-class functions. As an example the function in Figure 2.4 queries a number n from the user and initializes an array with values from 0 to n-1. By design, sourir is a cross between a compiler representation and a high-level language. We have equipped it with sufficient expressive power so that it is possible to write interesting programs in a style reminiscent of dynamic languages.² The only features that are critical to our result are versions and assumptions. Versions are the counterpart of dynamically generated code fragments. Assumptions, represented by the assume instruction, support dynamic deoptimization of speculatively compiled code. The syntax of sourir instructions is shown in Figure 2.5.

Sourir supports defining a local variable, removing a variable from scope, variable assignment, creating arrays, array assignment, (unstructured) control flow, input and output, function calls and returns, assumptions, and terminating execution. Control-flow instructions take explicit labels, which are compiler-generated symbols but we sometimes give them meaningful names for clarity of exposition. Literals are integers, Booleans, and nil. Together with variables and function references, they form simple expressions. Finally, an expression is either a simple expression or an operation: array access, array length, or primitive operation (arithmetic, comparison, and logic operation). Expressions are not nested—this is common in intermediate representations such as A-normal form [Sabry and Felleisen, 1992]. We do allow bounded nesting in instructions for brevity.

A program P is a set of function declarations. The body of a function is a list of versions indexed by a version label, where each version is an instruction sequence. The first instruction sequence in the list (the active version) is executed when the function is called. F ranges over function names, V over version labels, and L over instruction labels. An absolute reference to an instruction is thus a triple F.V.L. Every instruction is labeled, but for brevity we omit unused labels.

Versions model the speculative optimizations performed by the compiler. The only instruction that explicitly references versions is assume. It has the form assume e^∗ else ξ ξ^∗ with a list of predicates (e^∗) and deoptimization metadata ξ and ξ ^∗ . When executed, assume evaluates its predicates; if they hold execution skips to the next instruction. Otherwise, deoptimization occurs according to the metadata. The format of ξ is F.V.L [x₁ = e₁,..,x_n = e_n], which contains a target F.V.L and a varmap [x₁ = e₁,..,x_n = e_n]. To deoptimize, a fresh environment for the target is created according to the varmap. Each expression e_i is evaluated in the old environment and bound to x_i in the new environment. The environment specified by ξ replaces the current one. Deoptimization might also need to create additional continuations, if assume occurs in an inlined function. In this case multiple ξ of the form F.V.L x [x₁ = e₁,..,x_n = e_n] can be appended. Each one synthesizes a continuation with an environment constructed according to the varmap, a return target F.V.L, and the name x to hold the returned result—this situation and inlining are discussed in 2.5. The purpose of deoptimization metadata is twofold. First, it provides the necessary information for jumping to the target version. Second, its presence in the instruction stream allows the optimizer to keep the mapping between different versions up-to-date.

For simplicity, assumptions are modeled as guard expressions which are always checked at the point of the assume instructions. This is not a limitation and still allows us to have remote dependencies using a global dependency array to store their state. See section 2.7 for details.

Example

size ( x )

V o V b

Consider the function  size in Figure 2.6 which computes the size of a vector x . In version V b, x is either nil or an array with its length stored at index 0. The optimized version V o expects that the input is never nil. Classical compiler optimizations can leverage this fact: unreachable code removal prunes the unused branch. Constant propagation replaces the use of el with its value and updates the varmap so that it restores the deleted variable upon deoptimization to the base version V b.

Deoptimization Invariants

show ( x )

V o V w V b

A version is the unit of optimization and deoptimization. Thus we expect that each function will have one original version and possibly many optimized versions. Versions are constructed such that they preserve two crucial invariants: (1) version equivalence and (2) assumption transparency. By the first invariant all versions of a function are observationally equivalent. The second invariant ensures that even if the assumption predicates do hold, deoptimizing to the target should be correct. Thus one could execute an optimized version and its base in lockstep; at every assume the varmap provides a complete mapping from the new version to the base. This simulation relation between versions is our correctness argument. The transparency invariant allows us to add assumption predicates without fear of altering program semantics. Consider a function show in Figure 2.7, which prints its argument  x . Version V o respects both invariants: any value for x will result in the same behavior as the base version and deoptimizing is always possible. On the other hand, V w, which is equivalent because it will never deoptimize, violates the second invariant: if it were to deoptimize, the value of x would be set to 42, which is almost always incorrect. We present a formal treatment of the invariants and the correctness proofs in section 2.6.

Creating Fresh Versions

We expect that versions are chained. A compiler will create a new version, say V 1 , from an existing version V 0 by copying all instructions from the original version and chaining their

fun ()

V 2 V 1 V 0

deoptimization targets. The latter is done by updating the target and varmap of assume instructions such that all targets refer to V 0 at the same label as the current instruction. As the new version starts out as a copy, the varmap is the identity function. For instance, if the target contains the variables x and y , then the varmap is [ x = x , z = z ]. Additional assume instructions can be added; assume instructions that bear no predicates (i.e.,, the predicate list is either empty or just tautologies) can be removed while preserving equivalence. As an example in Figure 2.8, the new version V 2 is a copy of V 1 ; the instruction at L0 was added, the instruction at L1 was updated, and the one at L2 was removed.

size ( x )

V dup  V b …

Updating assume instructions is not required for correctness. But the idea behind a new version is that it captures a set of assumptions that can be undone independently from the previously existing assumptions. Thus, we want to be able to undo one version at a time. In an implementation, versions might, for example, correspond to optimization tiers.³ This approach can lead to a cascade of deoptimizations if an inherited assumption fails; we discuss this in 2.5. In the following sections we use the base version V b of Figure 2.6 as our running example. As a first step, we generate the new version V dup with two fresh assume instructions shown in Figure 2.9. Initially the predicates are true and the assume instructions never fire. Version V b stays unchanged.

Injecting Assumptions

We advocate an approach where the compiler first injects assumption predicates, and then uses them for optimizations. In contrast, earlier work would apply an unsound optimization and then recover by adding a guard (see, for example, Duboscq et al. [2013]). While the end result is the same, the different perspective helps with reasoning about correctness. Assumptions are Boolean predicates, similar to user-provided assertions. For example, to speculate on a branch target, the assumption is the branch condition or its negation. It is therefore correct for the compiler to expect that the predicate holds immediately following an assume. Injecting predicates is done after establishing the correspondence between two versions with assume instructions, as presented above. Inserting a fresh assume into a function is difficult in general, as one must determine where to transfer control to or how to reconstruct the target environment. On the other hand, it is always correct to add a predicate to an existing assume . Thanks to the assumption transparency invariant it is always safe to deoptimize more often. For instance, in assume   x ≠nil, x > 10  else … the predicate x ≠nil was narrowed down to x > 10 .

2.5 Optimizations

In the previous section we introduced our approach for establishing a fresh version of a function that lends itself to speculative optimizations. Next, we introduce classical compiler optimizations that are exemplary of our approach. Then we give additional transformations for the assume instruction and conclude with a case study. All transformations introduced in this section are proved correct in section 2.6.

Constant Propagation

Consider a simple constant propagation pass that finds constant variables and then updates all uses. This pass maintains a map from variable names to constant expressions or unknown. The map is computed for every position in the instruction stream using a data-flow analysis. Following the approach by Kildall [1973], the analysis has an update function to add and remove constants to the map. For example analyzing var   x = 2 or x ← 2 adds the mapping x → 2. The instruction var  y = x + 1 adds y → 3 to the previous map. Finally, drop  x removes a mapping. Control-flow merges rely on a join function for intersecting two maps; mappings which agree are preserved, while others are set to unknown. In a second step, expressions that can be evaluated to values are replaced and unused variables are removed. No additional care needs to be taken to make this pass correct in the presence of assumptions. This is because in sourir, the expressions needed to reconstruct environments appear in the varmap of the assume and are thus visible to the constant propagation pass. Additionally, the pass can update them, for example, in assume  true else F .V .L [ x = y + z ], the variables y and z are treated the same as in call  h = foo ( y + z ). They can be replaced and will not artificially keep constant variables alive.

Constant propagation can become speculative. After the instruction assume  x = 0  else …, the variable x is 0. Therefore, x → 0 is added to the state map. This is the only extension required for speculative constant propagation. As an example, in the case where we speculate on a nil check

the map is x →¬nil after L2 . Evaluating the branch condition under this context yields ¬nil == nil, and a further optimization opportunity presents itself.

Unreachable Code Elimination

size ( x )

V pruned  V b …

As shown above, an assumption coupled with constant folding leads to branches becoming deterministic. Unreachable code elimination benefits from that. We consider a two step algorithm: the first pass replaces branch e  L1 L2 with goto L1 if e is a tautology and with goto L2 if it is a contradiction. The second pass removes unreachable instructions. In our running example from Figure 2.9, we add the predicate x ≠nil to the empty assume at L2 . Constant propagation shows that the branch always goes to L3 , and unreachable code elimination removes the dead statement at L4 and branch. This creates the version shown in Figure 2.10. Additionally, constant propagation can replace el by 32. By also replacing its mention in the varmap of the assume at L2 , el becomes unused and can be removed from the optimized version. This yields version V o in Figure 2.6 at the top.

Function Inlining

main()

V inl V b

size ( x )

V o  V b …

Function inlining is our most involved optimization, since assume instructions inherited from the inlinee need to remain correct. The inlining itself is standard. Name mangling is used to separate the caller and callee environments. As an example Figure 2.11 shows the inlining of size into a function main. Naïvely inlining without updating the metadata of the assume at L2 will result in an incorrect deoptimization, as execution would transfer to size.V b.L2 with no way to return to the main function. Also, main’s part of the environment is discarded in the transfer and permanently lost. The solution is to synthesize a new stack frame. As shown in the figure, the assume at in the optimized main is thus extended with main .V b.Lret   s  [ pl = pl , vec = vec ].This creates an additional stack frame that returns to the base version of main, and stores the result in s with the entire caller portion of the environment reconstructed. It is always possible to compute the continuation, since the original call site must have a label and the scope at this label is known. Overall, after deoptimization, it appears as if version V b of main had called version V b of size . Note, it would be erroneous to create a continuation that returns to the optimized version of the caller V inl . If deoptimization from the inlined code occurs, it is precisely because some of its assumptions are invalid. Multiple continuations can be appended for further levels of inlining. The inlining needs to be applied bottom up: for the next level of inlining, e.g.,, to inline V inl into an outer caller, renamings must also be applied to the expressions in the extra continuations, since they refer to local variables in V inl .

Unrestricted Deoptimization

The assume instructions are expensive: they create dependencies on live variables and are barriers for moving instructions. Hoisting a side-effecting instruction over an assume is invalid, because if we deoptimize the effect happens twice. Removing a local variable is also not possible if its value is needed to reconstruct the target environment. Thus it makes sense to insert as few assume instructions as possible. On the other hand it is desirable to be able to “deoptimize everywhere”—checking assumptions in the basic block in which they are used can avoid unnecessary deoptimization—so there is a tension between speculation and optimization. Reaching an assume marks a stable state in the execution of the program that we can fall back to, similar to a transaction. Implementations like the one by Duboscq et al. [2013] separate deoptimization points and the associated guards into two separate instructions to be able to deoptimize more freely. As long as the effects of instructions performed since the last deoptimization point are not observable, it is valid to throw away intermediate results and resume control from there. Effectively, in sourir this corresponds to moving an assume instruction forward in the instruction stream, while keeping its deoptimization target fixed.

An assume can be moved over another instruction if that instruction:

1. has no side-effects and is not a call instruction,
2. does not interfere with the varmap or predicates, and
3. has the assume as its only predecessor instruction.

The first condition prevents side-effects from happening twice. The second condition can be enabled by copying the affected variables at the original assume instruction location (i.e.,, taking a snapshot of the required part of the environment).⁴ The last condition prevents capturing traces incoming from other basic blocks where (1) and (2) do not hold for all intermediate instructions since the original location. This is not the weakest condition, but a reasonable, sufficient one.

size ( x ) V any  V b …

size ( x ) V any  V b …

Let us consider a modified version of our running example in Figure 2.12. Again, we have an assume before the branch. However, now we would like to place a guard only inside one of the branches. There is an interfering instruction at L4 that modifies x . By creating a temporary variable to hold the value of x at the original assume location, so it is possible to resolve the interference. As shown in Figure 2.13 the assume can now move inside the branch and a predicate can be added on the updated x . Note that the target is unchanged. This approach allows for the (logical) separation between the deoptimization point and the position of assumption predicates. In the transformed example a stable deoptimization point is established at the beginning of the function by storing the value of x , but then the assumption is checked only in one branch. The intermediate states are ephemeral and can be safely discarded when deoptimizing. For example the variable el is not mentioned in the varmap here, so it is not captured by the assume. Instead it is recomputed by the original code at the deoptimization target size.V b.L1 . To be able to deoptimize from any position it is sufficient to have an assume after every side-effecting instruction, call, and control-flow merge.

Predicate Hoisting

Moving an assume backwards in the code would require replaying the moved-over instructions in the case of deoptimization. Hoisting assume  true else  size.V b.L2  [ el = el ,…] above var  el = 32 is allowed if the varmap is changed to [ el = 32 ,…] to compensate for the lost definition. However this approach is tricky and does not work for instructions with multiple predecessors as it could lead to conflicting compensation code. But a simple alternative to hoisting assume is to hoist a predicate from one assume to a previous one. To understand why, let us decompose the approach into two steps. Given an assume at L1 that dominates a second one at L2 , we copy a predicate from the latter to the former. This is valid because the assumption transparency invariant allows strengthening predicates. A data-flow analysis can determine if the copied predicate from L1 is available at L2 , in which case it can be removed from the original instruction. In our running example, version V pruned in Figure 2.10 has two assume instructions and one predicate. It is trivial to hoist x ≠nil, since there are no interfering instructions. This allows us to remove the assume with the larger scope. More interestingly, in the case of a loop-invariant assumption, predicates can be hoisted out of the loop.

Assume Composition

As we have argued in 2.4, it is beneficial to undo as few assumptions as possible. On the other hand, deoptimizing an assumption added in an early version cascades through all the later versions. To be able to remove chained assume instructions, we show that assumptions are composable. If an assume in version V 3 transfers control to a target V 2 .La that is itself an assumption with V 1 .Lb as target, then we can combine the metadata to take both steps at once. By the assumption transparency invariant, the pre- and post-deoptimization states are equivalent: even if the assumptions are not the same, it is correct to conservatively trigger the second deoptimization. For example, consider the instruction assume e else F .V 2 .La  [ x = 1 ] that jumps to assume e′ else F .V 0 .Lb  [ y = x ]. They can be combined into assume e,e′ else F .V 0 .Lb  [ y = 1 ]. This new unified assume skips the intermediate version V 2 and goes to V 0 directly. This could be an interesting approach for multi-tier JITs: after the system stabilizes, intermediate versions are rarely used and may be discarded.

Case Study

div ( tagx , x , tagy , y )

V base

(a)

	assume  tagx = NUM , tagy = NUM  else div.V b.L1  […]
	branch  x = 0   LerrorL4
L4	return y ∕ x
	…

(b)

	assume  tagx = NUM , x ≠ 0  else div.V b.L1  […]
	branch  tagy ≠ NUM   LslowL4
L4	return y ∕ x
	…

(c)

	assume  tagx = NUM , tagy = NUM , x ≠ 0  else div.V b.L1  […]
	return y ∕ x

(d)

We conclude with an example. In dynamic languages code is often dispatched on runtime types. If types were known, code could be specialized, resulting in faster code with fewer checks and branches. Consider Figure 2.14(a) which implements a generic binary division function that expects two values and their type tags. No static information is available; the arguments could be any type. Therefore, multiple checks are needed before the division; for example the slow branch will require even more checks on the exact value of the type tag. Suppose there is profiling information that indicates numbers can be expected. The function is specialized by speculatively pruning the branches as shown in Figure 2.14(b). In certain cases, sourir’s transformations can make it appear as though checks have been reordered. Consider a variation of the previous example, that speculates on x , but not y as shown in Figure 2.14(c). In this version, both checks on x are performed first and then the ones on y , whereas in the unoptimized version they are interleaved. By ruling out an exception early, it is possible to perform the checks in a more efficient order. The fully speculated-on version contains only the integer division and the required assumptions (Figure 2.14(d)). This version has no more branches and is a candidate for inlining.

Limitations

A limitation of the assume model is that the varmap contains only silent expressions. Implementations may try to defer some instructions to occur only when deoptimizing. As an example consider an optimization to elide array allocation, e.g., rewriting the definition ‘array  x = [ 3 ]’ to ‘var  x = 3 ’. If x was captured by an assume instruction, then deoptimization would have to be able to convert the scalar 3 into a singleton array, which is not possible with an expressions. For this reason Ř allows for arbitrary instructions to be deferred and only executed when a guard fails.

Further, unrestricted deoptimization as shown above requires moving the assume instruction and therefore prevents speculation at its original location. Also, before inlining we need to preserve a copy of the current caller version. Both of these limitations are overcome by Barrière et al. [2021].

2.6 Assume Formalized

A sourir program contains several functions, each of which can have multiple versions. This high-level structure is described in Figure 2.15. The first version is considered the currently active version and will be executed by a call instruction. Each version consists of a stream of labeled instructions. We use an indentation-based syntax that directly reflects this structure and omit unreferenced instruction labels.

Besides grammatical and scoping validity, we impose the following well-formedness requirements to ease analysis and reasoning. We require all guard expressions e in assume e^∗ else ξ ξ^∗ to be statically known to produce a value. In practice this is not a limitation since partial functions can be extended to evaluate to false. The last instruction of each version of the main function is stop. Two variable declarations for the same name cannot occur in the same instruction stream. This simplifies reasoning by letting us use variable names to unambiguously track information depending on the declaration site. Different versions have separate scopes and can have names in common. If a function reference F is used, that function F must exist. Origin and target of control-flow transitions must have the same set of declared variables. This eases determining the environment at any point. To jump to a label L, all variables not in scope at L must be dropped (drop  x ).

Operational Semantics

Expressions

Figure 2.16

Figure 2.17

₁

_n

[Literal]

[Funref]

[Lookup]

[SimpleExp]

[Primop]

[VecLen]

[VecAccess]

Instructions and Programs

^∗

Figure 2.18

₁

_n

Figure 2.20

[Refl]

[SilentCons]

[ActionCons]

The relation CC′ specifies that executing the next instruction may result in the configuration C′. The action A_τ indicates whether this reduction is observable: it is either the silent action, written τ, an I/O action read lit or print lit, or stop. We write C C′ when there are zero or more steps from C to C′. The trace T is a list of non-silent actions in the order in which they appeared. Actions are defined in Figure 2.19, and the full reduction relation is given in Figure 2.20.

Most rules get the current instruction, I(L), perform an operation, and advance to the next label, referred to by the shorthand . The read lit and print lit actions represent observable I/O operations. They are emitted by Read and Print in Figure 2.20. The action read lit on the read x transition may be any literal value. This is the only reduction rule that is non-deterministic. Note that the relation C C′, containing only sequences of silent reductions, is deterministic.

The stop reduction emits the stop transition, and also produces a configuration with no instructions, 𝜀. This is a technical device to ensure that the resulting configuration does not reduce further. A program with a silent loop has a different trace from a program that halts.

Equivalence of Configurations: Bisimulation

We use weak bisimulation to prove equivalence between configurations. The idea is to define, for each program transformation, a correspondence relation R between configurations over the original and transformed programs. We show that related configurations have the same observable behavior, and reducing them results in configurations that are themselves related. Two programs are equivalent if their starting configurations are related.

In the remainder, the adjective weak is always implied. The following result is standard, and essential to compose the correctness proof of subsequent transformation passes.

Deoptimization Invariants

We can now give a formal definition of the invariants from 2.4: Version Equivalence holds if any pair of versions (V₁,V₂) of a function F are bisimilar; Assumption Transparency holds if for any configuration C, at an assume e^∗ else ξ ξ^∗, C, is bisimilar to deoptimize(C,ξ,ξ^∗), as defined in Figure 2.20, DeoptimizeConf.

Creating Fresh Versions and Injecting Assumptions

Configuration C is over location F.V.L if it is ⟨PP(F,V)LK^∗ME⟩. Let C[F.V.L ← F′ .V′ .L′] be ⟨PP(F′,V′)L′K^∗ME⟩. More generally, C[X ← Y ] replaces various components of C. For example, C[P₁ ←P₂] updates the program in C; if only the versions change between two locations F.V.L and F.V′ .L, write C[V ←V′] instead of repeating the locations, etc.

Proof. Consider P₁ with a function F with active version V₁. Adding a version yields P₂ with new active version V₂ of F such that

• any label L of V₁ exists in V₂L: the instruction at L in V₁ and V₂ are identical except for assume instructions updated so that assume e^∗ else ξ ξ^∗ in V₁ has an assume  e^∗ else F.V₁ .L Id in V₂ where Id is the identity over the environment at L.
• V₂ may contain extra empty assume instructions: for any instruction i at L in V₁, V₂ may contain an assume of the form assume true else F.V₁ .L Id, where Id is the identity mapping over the environment at L, followed by i at a fresh label L′.

Let us write I₁ and I₂ for the instructions of V₁ and V₂ respectively. Stack K₂^∗ is a replacement of K₁^∗ if it is obtained from K₁^∗ by replacing continuations of the form ⟨I₁ L x E⟩ by ⟨I₂ L x E⟩. Replacement is a device used in the proof and does not correspond to any of the reduction rules. We define a relation R as the smallest relation such that :

1. For any configuration C₁ over P₁, R relates C₁ to C₁ [P₁ ←P₂].
2. For any configuration C₁ over a F.V₁ .L such that L in V₂ is not an added assume, R relates C₁ to C₁ [P₁ ←P₂][V₁ ←V₂].
3. For any configuration C₁ over a F.V₁ .L such that at L in V₂ is a newly added assume followed by label L′, R relates C₁ to both (a) C₁[F.V₁ .L ← F.V₂ .L] and (b) C₁ [F.V₁ .L ←F.V₂ .L′].
4. For any related pair (C₁,C₂) ∈ R, where K₁^∗ is the call stack of C₂, for any replacement K₂^∗, the pair (C₁,C₂[K₁^∗ ← K₂^∗]) is in R.

The proof proceeds by showing that R is a bisimulation. If a related pair (C₁,C₂) ∈ R comes from the cases (1), (2) or (3) of the definition of R, we say that it is a base pair. A pair (C₁,C₂) in case (4) is defined from another pair (C₁,C′₂) ∈ R, such that the call stack of C₂ is a replacement of the stack of C′₂. If (C₁,C′₂) ∈ R is a base pair, we say that it is the base pair of (C₁,C₂). Otherwise, we say that the base pair of (C₁,C₂) is the base pair of (C₁,C′₂).

Bisimulation proof: generalities To prove that R is a bisimulation, consider all related pairs (C₁,C₂) ∈ R and show that a reduction from C₁ can be matched by C₂ and conversely. Without loss of generality, assume that C₂ is not a newly added assume instruction – that the base pair of (C₁,C₂) is not in the case (3,b) of the definition of R. Indeed, the proof of the case (3,b) follows from proof of the case (3,a). In the case (3,b), C₂ is a newly added assume instruction assume true else … at L followed by L′ . C₂ can only reduce silently into C′₂ C₂[L ← L′], which is related to C₁ by the case (3,a). The empty reduction sequence from C₁ matches this reduction from C₂. Conversely, assume the result in the case (3,a), then any reduction of C₁ can be matched from C′₂, and thus matched from C₂ by prepending the silent reduction C₂C′₂ to the matching reduction sequence. Finally, if (C₁,C₂) comes from case (4) and has a base pair (C₁,C′₂) from (3,b), and C₂ has label L followed by L′, then the bisimulation property for (C₁,C₂) ∈ R comes from the one of (C₁,C₂[L ← L′]) ∈ R by the same reasoning. Bisimulation proof: easy cases The easy cases of the proof are the reductions C₁C′₁ where neither C₁ nor C′₁ are over V₁, and the reductions C₂C′₂ where neither C₂ nor C′₂ are over V₂. For C₁C′₁, define C′₂ as C′₁[P₁ ← P₂], and both C₂ C′₂ and (C′₁,C′₂) ∈ R hold. The C₂ C′₂ case is symmetric, defining C′₁ as C′₂ [P₂ ←P₁]. Bisimulation proof: harder cases The harder cases are split in two categories: version-change reductions (deoptimizations, functions call and returns), and same-version reductions within V₁ in P₁ or V₂ in P₂ respectively.

We consider same-version reductions first. Without loss of generality, assume that the pair (C₁,C₂) ∈ R is a base pair, that is a pair related by the cases (2) or (3) of the definition of R, but not (4) – the case that changes the call stack of the configuration. Indeed, if pair (C₁,C′₂) ∈ R comes from (4), the only difference between this pair and its base pair (C₁,C₂) ∈ R is in the call stack of C₂ and C′₂. This means that C₂ and C′₂ have the exact same reduction behavior for non-version-change reductions. As long as the proof that the related configurations C₁ and C₂ match each other does not use version-change reductions (a property that holds for the proofs of the non-version-change cases below), it also applies to C₁ and C′₂. For a reduction C₂ C′₂ that is not a version-change reduction (deoptimization, call or return), prove that it can be matched from C₁ by distinguishing whether C₂ or C′₂ are assume instructions, coming from V₁ or newly added.

• If none of them are assume instructions, then they are both in the case (2) of the definition of R, they are equal to C₁[V₁ ← V₂] and C′₁[V₁ ← V₂] respectively, so C₁ C′₁ and (C′₁,C′₂) ∈ R hold.
• If C₂ or C′₂ are assume instructions coming from V₁, the same reasoning holds – the problematic case where the assume is C₂ and the guards do not pass is not considered here as the reduction is not a deoptimization.
• If C′₂ is a newly added assume in V₂ at L followed by L′, C₂ is an instruction of V₂ copied from V₁, so (C₁,C₂) are in the case (2) of the definition of R and C₁ is C₁[V₂ ←V₁]. The reduction from C₂ corresponds to a reduction C₁C′₁ in P₁ with C′₁ C′₂[V₂ ←V₁], and (C′₁,C′₂) ∈ R by the case (3,a) of the definition of R.

The reasoning for transitions C₁C′₁ that have to be matched from C₂ and are not version-change transitions (deoptimization, function calls or return) is similar. C₂ cannot be a new assume, so we have C₂C′₂, and either C′₂ is not a new assume and matches C₁ by case (2) of the definition of R, or it is a new assume and it matches it by the case (3,a).

Bisimulation proof: final cases The cases that remain are the hard cases of version-change reductions: function call, return and deoptimization. If C₁C′₁ is a deoptimization reduction, then C₁ is over a location F.V₁ .L in P₁, and its instruction is assume e^∗ else ξ ξ^∗, and C′₁ is deoptimize(C₁,ξ,ξ^∗). C₂ is over the copied instruction assume e^∗ else F.V₁ .L Id and Id is the identity. C₂ also deoptimizes, given that the tests yield the same results in the same environment, so we have C₂ C′₂ for C′₂ deoptimize (C₂,F.V.L₁ Id,∅). C′₂ is over F.V₁ .L, that is the same assume instruction as C₁, so it also deoptimizes, to C′′₂ deoptimize (C′₂,ξ,ξ^∗). We show that C′₁ and C′′₂ are related by R:

• If (C₁,C₂) ∈ R is a base pair, then C₁ is C₂[V₂ ←V₁]. In particular, the two configurations have the same environment, and C′₂ is identical to C₂ except it is over F.V.L₁. It is thus equal to C₁. As a consequence, C′₁ and C′′₂ , which are obtained from C₁ and C′₂ by the same deoptimization reduction, are the same configurations, and related in R.
• If C₁ and C₂ are related by the case (4) of the definition of R, the stack of C₂ is a replacement of the stack of C₁. The same reasoning as in the previous case shows that configurations C′₁ and C′′₂ are identical, except that the stack of C′′₂ is a replacement of the stack of C′₁: they are related by the case (4) of the definition of R.

Conversely, if C₂C′₂ is a deoptimization instruction then, by the same reasoning as in the proof of matching a deoptimization of C₁, C′₂ is identical to C₁ (modulo replaced stacks). This means that the empty reduction sequence from C₁ matches the reduction of C₂ .

If C₁C′₁ is a function call transition,

⟨P1I1LK1∗ME⟩⟨P 1I′1L′(K∗,⟨I 1 (L+1)  x  E⟩)ME′⟩

C₂ is on the same call with the same arguments, so it takes a transition C₂C′₂ of the form

⟨P2I2LK2∗ME⟩⟨P 2I′2L′(K∗,⟨I 2 (L+1)  x  E⟩)ME′⟩

The stack of C′₂ is a replacement of the stack of C′₁: assuming that K₂^∗ is a replacement of K₁^∗, the difference in the new continuation is precisely the definition of stack replacement — note that it is precisely this reasoning step that required the addition of case (4) in the definition of R. Also, the new instruction streams I′₁ and I′₂ are either identical (if the function is not F itself) or equal to I₁ and I₂ respectively, so we do have (C′₁,C′₂) ∈ R as expected. The proof of the symmetric case, matching a function call from C₂, is identical.

If C₁C′₁ is a function return transition

⟨P1I1L(K∗,⟨I′ 1 L′ x E′⟩)ME⟩⟨P1I′1L′K1∗ME′[x ←v]⟩

then C₂C′₂ is also a function return transition

⟨P2I2L(K∗,⟨I′ 2 L′ x E′⟩)ME⟩⟨P2I′2L′K2∗ME′[x ←v]⟩

We have to show that C′₁ and C′₂ are related by R. The environments and heaps of the two configurations are identical. We know that the stack of C₂ is a replacement of the stack of C₁, which means that K₂^∗ a replacement of K₁^∗, and that either I′₁ and I′₂ are identical or they are respectively equal to I₁ and I₂. In either case, C′₁ and C′₂ are related by R. The proof of the symmetric case, matching a function return from C₂, is identical. We have established that R is a bisimulation.

Finally, remark that our choice of R also proves that the new version respects the assumption transparency invariant. A new assume at L in V₂ is of the form assume true else F.V₁ .L Id, with Id the identity environment. Any configuration C over F.V₂ .L is related by R⁻¹ to C[F.V₂ .L ← F.V₁ .L], which is equal to the configuration deoptimize(C,F.V₁ .L Id,∅). These two configurations are related by the bisimulation R⁻¹, so they are bisimilar. □

Optimization Correctness

The proofs of the optimizations from section 2.5 are easier than the proofs for deoptimization invariants in the previous section (although, as program transformations, they seem more elaborate). This follows from the fact that the classical optimizations rewrite an existing version and interact little with deoptimization.

Constant Propagation

We say that given a version V, a static environment SE for label L maps a subset of the variables in scope at L to values. A static environment is valid, written SE ⊨L, if for any configuration C over L reachable from the start of V, SE is a subset of the lexical environment E. Constant propagation can use a classic work-queue data-flow algorithm to compute a valid static environment SE at each label L. It then replaces, in the instruction at L, each expression or simple expression that can be evaluated in SE by its value. This is speculative since assumption predicates of the form x = lit populate the static environment with the binding x →lit.

The restriction of our bisimulation R to reachable configurations introduced is crucial for the proof to work. Indeed, a configuration that is not reachable may not respect the static environment SE. Consider the following example, with V 1 on the left and V 2 on the right.

₁

₁

₁

₁

₂

₂

₂

₂

Unreachable Code Elimination

The following two lemmas are trivial: the simple version-change mapping between configurations on the two version is clearly a bisimulation. In the first case, this comes from the case that branch  true  L₁L₂ and goto L₁ reduce in the example same way. In the second case, unreachable configurations are not even considered by the proof.

Function Inlining

Assume that the function F has active version V callee . If the new version contains a call to F, call  res = F(e₁,..,e_n ) with return label Lret (the label after the call), inlining removes the call and instead:

• declares a fresh mutable return variable var  res = nil;
• for the formal variables x,.. of F, defines the argument variables var x₁ = se₁,..,var x_n = se_n;
• inserts the instructions from V callee , replacing each instruction returne by the sequence:
  res ←e; drop x₁; ... ; drop x_n; goto Lret

Unrestricted Deoptimization

Consider P₁ containing an assume at L₁, followed by i_m at L₂ (L₁+1). Let i_m be such it has a unique successor, is the unique predecessor of L₁, and is not a function call, has no side-effect, does not modify the heap (array write or creation), and does not modify the variables mentioned in the assume. Under these conditions, we can move the assume immediately after the successor of i_m. Let us name P₂ the program modified in this way.

Predicate Hoisting

Hoisting predicates takes a version V₁, an expression e, and two labels L₁,L₂, such that the instruction at L₁,L₂ are both assume instructions and e is a part of the predicate list at L₁. The pass copies e from L₁ to L₂, if all variables mentioned in e are in scope at L₂. If, after this step the e can be constant folded to true at L₁ by the optimization from 2.5, then it is removed from L₁, otherwise the whole version stays unchanged.

Assume Composition

Let V₁,V₂,V₃ be three versions of a function F with instruction streams I₁,I₂,I₃, and labels L₁,L₂,L₃, such that there are two instructions I₁(L₁) = assume e₁ else F.V₂ .L₂ VA₁ and I₂ (L₂) = assume e₂ else F.V₃ .L₃ VA₂. The composition pass creates a new program P₂ from P₁ identical but the assume P₂ (F.V₁.L₁) is replaced by assume e₁,e₂ else F.V₃ .L₃ VA₂ ∘VA₁ where the composition ([x₁ = e₁,..,x_n = e_n] ∘VA) is defined as [x₁ = e₁{∀y ∈VA},..,x_n = e_n{∀y ∈VA}].

2.7 Discussion

Our formalization raises new questions and makes apparent certain design choices. In this section, we present insights into the design space for JIT implementations.

The Cost of Assuming

Figure 2.21

2.5

Lazy Deoptimization

stuck ()

V base

cont ( x )

V opt

undo ()

V s123 V s12 V s1

assumptions from runtime checks. Specifically, let GUARDS [ 13 ] = true be the runtime check, where the global array GUARDS is a collection of all remote assumptions that can be invalidated by an operation, such as an array assignment. In terms of correctness, both eager and lazy deoptimization are similar; however, we would need to prove correctness of the dependency mechanism that modifies the global array.

Jumping Into Optimized Code

Figure 2.22

Figure 2.23

Fine-Grained Deoptimization

Figure 2.24

₂

₃

₁

₃

₃

section 3.4

Simulating a Tracing JIT

Bala, Duesterwald, and Banerjia

2000

Gal, Eich, Shaver, Anderson, Mandelin, Haghighat, Kaplan, Hoare, Zbarsky, Orendorff, Ruderman, Smith, Reitmaier, Bebenita, Chang, and Franz

2009

Guo and Palsberg

2011

Figure 2.25

while

Then unreachable code elimination yields the following code, resembling a trace.

Say x is not accessed after the store in this optimized version. In sourir, it is obvious why dead store elimination of x would be unsound: the deoptimization metadata indicates that x is needed for deoptimization and the store operation can only be removed it can be replayed. In this specific example, a constant propagation pass could update the metadata to materialize the write of 0, only when deoptimizing at the second assume. But, before the code can be reduced, loop unrolling might result in intermediate versions that are much larger than the original program. In contrast, tracing JITs can handle this case without the drastic expansion in code size [Gal et al., 2009], but lose more information about instructions outside of the trace.

Relation to Real-World Systems

Chromium

2022

Duboscq et al.

2013

2.8 CoreJIT: Towards a Verified JIT

Eventually the building blocks presented in this thesis could be the foundation for writing an end-to-end verified JIT compiler. First steps were already made by Barrière et al. [2021]. The main differences with the formalization presented so far are that CoreJIT also models the creation of optimized code at run-time, that the formalization is mechanized, and that the deoptimization invariant was made more precise, by splitting Assume into two instructions Anchor and Assume. This section summarizes our findings from that paper, with the focus on the comparison to the sourir model.

CoreIR is inspired by CompCert’s RTL Leroy [2009]. As a simplification over sourir, CoreIR only features two versions per function, an optimized and a baseline one. Two CoreIR instructions are related to speculation, Anchor and Assume. Together they look and behave very similar to assume from sourir. The split was made to better describe the dynamics of the optimization process. The Anchor instruction represents a potential deoptimization point, i.e., a location in an optimized function where the correspondence with its baseline version is known to the compiler and thus deoptimization can occur. For instance, in Anchor F.l [r = r+1] the target F.l specifies the function (F) and label (l) to jump to, the mapping [r = r+1] is the varmap.

Anchors are inserted first in the optimization pipeline, before any changes are made to the program. Choosing where to insert them is important as they determine where speculation can happen. Speculation itself is performed by inserting Assume instructions. An assume based on the previous anchor is for instance Assume x=1 F.l [r = r’+1], which expresses the expectation that register x has value 1. This instruction behaves like the assume instruction in sourir. Unlike anchors, assumes can be inserted at any time during compilation.

The role of anchors is subtle. As already shown it is possible to move an assume instructions to support deoptimization at any location. To make this more practical, the Anchor stays at its original location, without tying it to additional data-dependencies by guard expressions. To add an Assume, the compiler finds the dominating Anchor and copies its deoptimization metadata. If there is no anchor, then the assumption cannot be made.

For the proofs, anchors have yet another role. They justify the insertion of Assume instructions. For this, the Anchor instructions have a non-deterministic semantics, an anchor can randomly choose to deoptimize. Crucially, deoptimization is always semantically correct, nothing is lost by returning to the baseline code eagerly other than performance. An inserted Assume is thus correct if it follows an Anchor and the observable behavior of the program is unchanged regardless which instruction deoptimizes.

Let’s consider the example in Figure 2.26. On the left is the version before inserting an assume, on the right after. In this case there is an Anchor followed by a conditional Branch and we insert the Assume instruction only in one of the branches. As mentioned, Anchor has a non-deterministic semantic, it can either continue or deoptimize. Therefore, the respective states must be matched for all its successor instructions, i.e., for both the case where it falls through (solid lines), as well as when it deoptimizes (via dashed lines). To that end the states between Anchor and Assume are matched both to a fall-through Anchor and a deoptimizing Anchor trace. In other words the assumption insertion pass codifies the assumption transparency invariant. The benefit of having anchors is that the assumes they dominate can be placed further down the instruction stream. The compiler must make sure that the intervening instructions do not affect deoptimization. This separation is important in practice as it allows a single Anchor to justify speculation at a range of different program points. All Anchor instructions are removed in the last step of the optimization pipeline. Initially the varmap of an Assume instruction will be identical to its dominating Anchor, but, as the following example shows, this can change through subsequent program transformations.

Illustrative Example

Listing 2.2

label l2 of function F registers z and x always have values 7 and 75. Function F can thus be specialized. Listing 2.3 adds an Opt version to F where an anchor has been added at l4.

In order to deoptimize to the baseline, the anchor must capture all of the arguments of the function (x, y, z) as well as the local register d. The compiler is able to constant propagate d, so the anchor remembers its value. The speculation is done by e.g., Assume z=7 ... which specifies what is expected from the state of the program and the dominating anchor. The optimized version has eliminated dead code and propagated constants. If the speculation holds, then this version is equivalent to Base. Despite the overhead of checking validity of the speculation, the new version should be faster: the irrelevant computation of a has been removed and x*x is speculatively constant folded. If the speculation fails, then the execution should return to Base, at label l1 where the closest Anchor is available, and reconstruct the original environment. This involves for instance materializing the constant folded variable d. As we see here, Assume does not have to be placed right after an Anchor instruction. This will cause deoptimization to appear to jump back in time and some instructions will be executed twice. It is up to the compiler to ensure these re-executed instructions are idempotent. As can be seen in the example, different Assume instructions originating from the same Anchor, can end up with different varmaps.