Flambda2 Validator
This program is tentative and subject to change.
This talk will describe a validation tool for Flambda2, an optimizing middle-end for OCaml. Its optimizations are centered around inlining (replacing a function call with the function body) and applying simplications that become possible after inlining. Although such a transformation sounds innocuous, it is one of the most important—and tricky to implement—optimizations in the compiler pipeline. We increase confidence in Flambda 2’s optimizations by providing a relatively small and declarative definition of reduction to reduce optimized and unoptimized versions of the same program to syntactically equivalent terms. The tool is functional and can validate Flambda2’s optimizations for a substantial fraction of the OCaml standard library, our main test suite.
Paper (ocaml2024-final5.pdf) | 318KiB |
This program is tentative and subject to change.
Sat 7 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:30 | |||
09:00 22mTalk | On the design and implementation of Modular Explicits OCaml Pre-print File Attached | ||
09:22 22mTalk | Flambda2 Validator OCaml Pre-print File Attached | ||
09:45 22mTalk | A Non-allocating Optionin-person OCaml Richard A. Eisenberg Jane Street Pre-print File Attached | ||
10:07 22mTalk | Mixed Blocks: Storing More Fields Flatin-person OCaml Nicholas Roberts Jane Street Pre-print File Attached |