12.6 Optimization Correctness and Tradeoffs

An optimization is valid only when every behavior allowed by the source program is represented correctly by the transformed program under the language's rules. “Both returned 42 in my test” is evidence, not a proof. Observable behavior may also include I/O order, volatile access, exceptions, termination, allocation, synchronization, floating-point details, and debugging guarantees.

The compiler must first define its contract. In some languages signed overflow wraps; in others it traps or is undefined. Floating-point expressions may require strict IEEE behavior unless fast-math flags relax it. Concurrency introduces memory-order rules that ordinary algebra cannot ignore.

Preconditions make rewrites correct

Every rewrite should be understood as a rule plus preconditions:

x / x  →  1

This is not universally valid. x may be zero, NaN, infinity, or an effectful expression evaluated twice in the source representation. A safer rule specifies the type, proves nonzero and finite values where required, and ensures evaluation count is preserved.

Similarly, moving a load out of a loop requires proof that no iteration writes an alias, that no intervening synchronization changes the value, and that executing the load earlier does not introduce a new fault. Optimizer correctness lives in these side conditions.

Differential testing and translation validation

One practical defense is differential execution: run source IR and optimized IR on the same generated inputs and compare results plus event traces. Random and coverage-guided generation can find surprising counterexamples involving overflow, exceptional paths, aliasing, or side effects.

Testing cannot cover an infinite input space. Formal proofs, verified peephole-rule generators, SMT solvers, and translation validation provide stronger assurance. Translation validation checks each produced before/after pair rather than proving the optimizer implementation once for all inputs. Independent IR verification should also run after every pass to catch broken types, dominance, phi edges, and terminators.

When a fuzzer finds a mismatch, reduce it to the smallest function that still fails. A ten-instruction counterexample with one relevant flag is far more useful than a full application. Preserve the seed, target, optimization pipeline, and semantic mode in a regression test.

Optimization is multi-objective

Even a legal transformation may not be desirable. Compilers balance:

• runtime latency and throughput;

• compilation time and memory use;

• code size and instruction-cache pressure;

• startup time versus peak performance;

• debug quality, reproducibility, and energy use.

Inlining may remove call overhead and expose constants, but it grows code and makes later analyses more expensive. Loop unrolling reduces branches but increases size and register pressure. Vectorization accelerates regular loops but may need runtime checks and a scalar fallback. There is rarely one configuration that dominates all others.

Optimization levels are policies

An optimization level such as -O0, -O2, or -Os is not a quality score. It is a policy selecting passes, thresholds, repetition limits, and assumptions for a use case. A development build may prioritize fast compilation and predictable debugging. A production server may spend more compile time on throughput. Embedded software may prioritize size and deterministic timing.

Profile-guided optimization further specializes decisions using observed hot paths and call targets. Profiles are samples, not laws: the optimized program must remain correct for unobserved inputs, and the compiler should avoid overfitting rare training behavior.

A disciplined optimization pipeline records why each transformation fired, measures before and after on representative workloads, and keeps legality separate from cost modeling. Correctness is the non-negotiable boundary; performance is an empirical engineering decision inside that boundary.