BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Correctness of Speculative Optimizations with Dynamic Deoptimizati
 on - Gabriel Scherer (Parsifal\, INRIA Saclay\, France)
DTSTART:20171102T150000Z
DTEND:20171102T160000Z
UID:TALK94885@talks.cam.ac.uk
CONTACT:Liang Wang
DESCRIPTION:High-performance dynamic language implementation make heavy us
 e of speculative optimizations to achieve speeds close to statically compi
 led languages. These optimizations are typically implemented by a just-in-
 time compiler that generates code optimized under a set of assumptions abo
 ut the state of the program and its environment. In certain cases\, a prog
 ram may finds itself executing code compiled under assumptions that have b
 ecome invalid\, the language implementation must\, then\, execute a bailou
 t procedure that exits the speculatively optimized code region. Effectivel
 y\, the implementation must deoptimize the program on-the- fly\; this enta
 ils finding a corresponding code region that does not rely on invalid assu
 mptions\, translating program state to that expected by the target code\, 
 and transferring control. The procedure is sometimes called on-stack-repla
 cement as it entails modifying stack frames\, and in some cases\, synthesi
 zing new ones for inlined functions. Reasoning about the correctness of sp
 eculative optimizations is challenging because the optimized code is not e
 quivalent to the source program. The main benefit of speculative optimizat
 ion is to entirely remove low-likelihood code paths. Soundness is only rec
 overed when the bailout mechanism is taken into account\, but even then\, 
 it is necessary to be able to recreate the program state exactly as expect
 ed by the unoptimized program.\n\nThe presented work -- joint work with Ol
 i Flückiger\, Ming-Ho Yee\, Aviral Goel\, Amal Ahmed and Jan Vitek at Nor
 theastern University -- looks closely at the interaction between compiler 
 optimization and deoptimization. We demonstrate that reasoning about specu
 lative optimizations is surprisingly easy when assumptions are reified in 
 the intermediate representation. To this end wepresent a model intermediat
 e representation (IR) that stands in for the high-level IR of a compiler f
 or a dynamic language. Our IR models core difficulties of speculative opti
 mization\, such as interleaving assumptions and optimizations\, and the in
 teraction with inlining. Our formalization stays at the IR level\, thus ab
 stracting orthogonal issues such as code generation and self mutation.  We
  describe a set of common optimizations (constant folding\, unreachable co
 de elimination\, and function inlining) and prove them correct in presence
  of speculative assumptions \n\nIn the talk I will not assume previous kno
 wledge of JIT compilation.\n\nBIO: Gabriel Scherer (Parsifal\, INRIA Sacla
 y\, France) researches programming languages\, most often typed functional
  languages\, and hacks on the OCaml compiler.
LOCATION:FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR