Greta Yorsh on Compiler Optimization and Feedback

Ron Minsky welcomes Greta Yorsh, a compiler engineer on Jane Street’s London team. Her background spans program analysis, verification, industry and academia; since 2018 she has worked on the OCaml compiler.

Yorsh studied computer science and economics in Israel, then pursued a computer-science PhD focused on software verification. She worked on program analysis at IBM Watson, on the GCC backend for ARM, and later taught and researched compilers at Queen Mary University of London before joining Jane Street.

Verification research seeks to prove that a program satisfies desired properties using reasoning about source code. Yorsh found the general problem difficult and wanted to understand what real users needed. Talking to developers showed her that performance can matter alongside correctness, making compiler optimization an appealing application of formal techniques.

At ARM she saw how instruction- and machine-specific optimizations can change performance. A compiler must also be correct because so much software depends on its output. That combination gave her a practical, measurable optimization goal with demanding correctness requirements.

Minsky describes formal verification as proving that an implementation conforms to a specification. General questions about program behavior are undecidable, but tools can still help with restricted cases or with additional work supplied by the programmer.

Yorsh distinguishes a separate logical specification from the more integrated specifications supplied by types. Maintaining a separate specification as code evolves is difficult. Tooling can check the code and specification together, but the programmer still has to produce both; automation can reduce that burden.

Testing checks concrete executions and can find a bug quickly where a general proof is expensive. Yorsh is interested in combining the approaches: formal methods can suggest useful tests, while concrete executions can help guide or accelerate reasoning about a larger space of behavior.

Minsky offers a programmer’s perspective: types give guarantees about certain properties across executions, while tests check particular runs. Neither a well-typed program nor a handful of passing tests ensures complete correctness, but together they can be much more effective than either alone.

Yorsh sketches one family of techniques. Execute a program, collect observed states and abstract them into descriptions covering related states. A decision procedure can identify a state or path not yet covered, which can then guide another execution. The interaction can increase coverage and reduce the expensive work left for verification.

The discussion turns to superoptimization. Yorsh explains that a backend needs information about instruction costs, registers and hardware behavior. Conventional compilers apply separate passes for tasks such as instruction selection, register allocation and scheduling; choices interact across passes, so individually sensible decisions need not produce the best overall result.

While working on ARM microarchitectures, she found it hard to make the compiler emit a known better sequence because changing one pass affects others. Superoptimization offers another frame: search for a solution satisfying the constraints together instead of relying solely on a fixed sequence of local transformations.

A superoptimizer takes an instruction sequence and seeks an equivalent one optimized against a cost measure. Historically the goal could be the shortest sequence, but on modern hardware more instructions can sometimes run faster than a shorter sequence containing expensive operations.

The candidate must behave the same as the original on the relevant inputs. Proving arbitrary programs equivalent is undecidable, so early work restricted the problem to straight-line sequences and used testing; later approaches expressed semantics as constraints and used decision procedures. Verification and search still have significant costs.

Minsky contrasts the conventional compiler’s modular intermediate representations and passes with superoptimization’s search over possible code. The modular design makes a large system understandable but can obscure interactions; the search frame makes a cost and correctness criterion explicit, though it may be expensive.

Yorsh would like to see superoptimization used more, especially as a tool for compiler builders and exceptionally performance-critical code. She does not expect expensive search to become a routine step in every developer’s daily build as the technology stood at the time.

A formal description of a hardware architecture can also parameterize the search. In an idealized version, a new machine description could help produce good code without manually redesigning every intricate backend pass. Yorsh sees potential for hardware and compiler designers to explore how much benefit a new architecture can deliver.

Minsky notes that a superoptimizer can measure the gap between a practical compiler’s output and a better sequence. He worries that an hours-long search would make application development feedback too slow. Yorsh agrees the most immediate use is helping infrastructure designers, while suggesting that some expensive work might be reused for a source-language and target pair.

Asked about moving between academia and industry, Yorsh says research offers time to understand and design powerful techniques, but access to users can be limited and novelty is rewarded. Industry brings different constraints and scale, yet gives her direct feedback on whether familiar tools actually help developers.

At Jane Street she worked on feedback-directed optimization, also known as profile-guided optimization. Traditional instrumentation adds measurements to the program; sampling can collect profiles with less perturbation. Representative runs indicate which paths are hot, information unavailable to a purely static compiler.

In the work she describes, the profile guides code layout: the order of functions in an executable and basic blocks within functions. Frequently executed code placed close together can make better use of instruction caches, reducing time spent fetching instructions from slower levels of memory.

Minsky recalls early results of roughly 10%, 15% or 20% improvement in some important programs just from rearranging instructions. Yorsh explains that these are workload-dependent gains from locality, not a universal promise for every program.

The team also found value in stability. A developer saw a slowdown after an unrelated library change; feedback-directed layout removed the observed difference by keeping frequently used code together. Predictable results make it easier to tell whether a small optimization is real rather than an artifact of layout.

They discuss using feedback-directed layout in compiler benchmarks to reduce noise. Another research direction intentionally randomizes layout and studies a distribution of outcomes, potentially with statistical sampling. Minsky notes that repeatedly perturbing and rerunning a benchmark can be costly.

Minsky places feedback-directed optimization between static compilation and fully dynamic approaches such as just-in-time compilation. Hardware itself also predicts and reorders work. He asks how a different processor’s capabilities would change the work worth doing in a compiler.

Yorsh says hardware observes recent execution while the compiler can reason about more of the program’s structure and possible future paths. Each optimization also has a cost, whether in compile time, runtime or energy. Hardware improvements can benefit many compilers, while a language compiler’s improvements serve its own users across architectures.

For some programs, memory access, allocation and garbage collection dominate small instruction-level improvements. Data layout and access patterns may then matter more. Yorsh mentions profiling tools being developed by colleagues to make those patterns visible.

Yorsh had not programmed in OCaml before joining Jane Street. Once she adjusted her thinking, she found it concise and well suited to expressing program analyses and transformations compared with the Java infrastructure she had used. Garbage collection also removes some explicit memory-management concerns.

She values the type checker once she learned to interpret its messages: it catches many mistakes while she works, although testing remains necessary. Minsky agrees that type systems differ substantially in expressiveness and in the assistance they give programmers.

As an optimization target, the OCaml compiler presented unfamiliar design choices. Yorsh came to appreciate a relatively portable backend that aims first for correct, understandable code and lets hardware do some optimization. The architecture-specific portion is small, but fixed passes make certain transformations difficult to add.

She explains the common frontend, middle-end and backend division. The frontend parses and type-checks a source language; the middle-end performs transformations that can be more independent of source and target; the backend generates code for a specific processor. Shared intermediate stages let a compiler infrastructure support multiple languages and architectures.

Minsky asks about ARM as its use expands, including Apple’s announced move to ARM-based desktops. Yorsh has not benchmarked OCaml on ARM and qualifies her answer as an impression from the backend code: it may have received less architecture-specific attention than heavily optimized compilers such as GCC.

Different ARM microarchitectures make different demands. In-order execution can make instruction scheduling particularly important, and register restrictions affect allocation choices. She also sees potential to improve register allocation on AMD64, but wants representative evidence that the investment will help actual workloads.

Access to real applications, developers and benchmarks is one of the benefits of her role: it lets the compiler team test ideas and get feedback quickly. It also makes the consequences of mistakes visible.

Yorsh recounts an optimization that introduced a miscompilation because she misunderstood an OCaml compiler detail. A test caught it, though the test was not routinely run. She says she did not believe it damaged running production systems, but colleagues still had to coordinate rollbacks and spend time avoiding the issue.

She appreciated the response: fix the mistake, ask why the test was missed, add it to the process and examine whether the compiler’s intermediate representation could prevent similar errors. Minsky says that learning-oriented response is part of the culture they try to maintain.

The pair turn to upstream collaboration. Jane Street does not own OCaml, and changes must be persuasive to its wider maintainers. An optimization motivated by internal applications may be difficult to demonstrate externally, especially when the largest executables contain proprietary code.

Yorsh suggests sharing performance tools and benchmarks with other industrial and academic OCaml users. Trust and participation in the community help technical discussions, but do not guarantee that a feature useful to one firm belongs in a general-purpose compiler.

Minsky mentions the Sandmark benchmark collection developed around multicore OCaml as a promising shared resource. Open-source code can expose some issues, but large-scale behavior may depend on workloads that cannot be published in full.

Yorsh notes that upstream maintainers must balance performance against portability, predictable behavior and the cost of maintaining complex features. A compiler that makes it easier to add or enable specialized passes could provide a middle ground between a fixed backend and a large collection of permanently maintained optimizations.

Minsky agrees that modularity can lower the shared maintenance burden and make experiments easier to carry as separate changes. Teams could gather evidence, iterate and eventually propose a mature improvement upstream. Yorsh adds that other users could give feedback more easily if trying a feature did not require changing their build systems.

They close by observing that the conversation has returned to feedback: profiles help optimize programs, and user feedback helps improve compilers themselves.