An optimization needs a semantic proof

Prerequisites: Expressions, types, control flow, and machine-number representations.

Learning objectives

• State the observable behavior a transformation must preserve.
• Find counterexamples to algebraic rewrites under finite arithmetic.
• Explain aliasing and side-effect barriers to optimization.

Equivalence depends on the language

An optimization changes implementation while preserving behavior required by the language and program contract. The relevant behavior can include returned values, memory updates, I/O, exceptions, and allowed ordering. Equality over mathematical real numbers is not automatically equality over machine floating point or a language with observable effects.

Consider replacing x*0 with zero. Over ordinary mathematical integers this is valid. For IEEE-style floating point, x might be infinity or NaN, for which multiplication can produce NaN rather than zero. Replacing a function call f()*0 with zero may also remove the call’s output, mutation, or exception. The expression’s value is only part of the proof obligation.

Find a concrete counterexample

Reassociating (a+b)+c into a+(b+c) is valid for exact real addition, but intermediate floating-point rounding can differ. Using ordinary Python floats on common binary64 implementations gives a visible example:

a, b, c = 1e16, -1e16, 1.0
left = (a + b) + c
right = a + (b + c)
assert left == 1.0
assert right == 0.0

The cancellation in the first grouping exposes the one, while the addition of one to the large-magnitude negative value rounds away that contribution in the second grouping. A compiler may allow such transformations only under a semantic contract or explicitly selected options that permit the relevant differences. Those options change what the programmer may assume.

Memory introduces hidden dependencies

Suppose an IR loads from address p, stores through address q, then loads from p again. Reusing the first loaded value is valid only if the intervening store cannot change the observed location, or another rule makes the reuse safe. Different variable names p and q do not prove distinct addresses. Alias analysis establishes facts or conservatively leaves uncertainty.

Similarly, moving a division out of a conditional can introduce a divide-by-zero event on a path where the original expression never ran. Loop-invariant code motion must account for whether the operation is safe to execute earlier and whether memory it reads remains unchanged. Dead code elimination must preserve observable effects even when a result is unused.

A sound workflow writes the transformation, lists preconditions, and tests adversarial boundary cases: zero, extremes, NaNs where relevant, aliases, exceptions, and empty loops. Testing finds counterexamples but does not prove all-input equivalence by itself. Formal reasoning, verified rewrite rules, and carefully specified IR semantics supply stronger justification. Performance measurement comes after correctness because a faster program with changed required behavior is a different program.

Primary reading

• LLVM Language Reference (LLVM Project).

Practice problem

A transformation replaces two loads from p with one cached value even though a store through q occurs between them. Give a concrete aliasing counterexample. Then explain why moving 10/x from inside if x != 0 to before that conditional can change behavior. State preconditions that would make each proposed transformation safer to justify.

Worked solution

Let p and q both refer to the same integer cell initially containing three. The first load returns three. A store through q changes the cell to seven. The second original load must return seven, while reusing the cached first value returns three. A proof that the store cannot affect the loaded location, together with the relevant memory and concurrency rules, is needed before reuse. For the conditional, x=0 skips the division in the original program but evaluating 10/x first can raise an exception or invoke another language-defined failure. Hoisting requires proof that the operation is safe on all newly executed paths, such as a dominating guarantee that x is nonzero, and that its effects and timing of observable behavior satisfy the language contract.

Check your understanding

Why can x*0→0 be invalid for floating-point x?

• Floating point has no zero.
• Infinity or NaN can produce a NaN result under the original multiplication.
• Multiplication always prints output.
• All floating-point values are integers.

Explanation

Special values make real-number algebra insufficient as a rewrite justification.

Two pointer variables have different names. What follows about aliasing?

• They necessarily point to different objects.
• Nothing sufficient by name alone; their values may identify the same location.
• They must point to adjacent bytes.
• Only one can ever be loaded.

Explanation

A memory-dependence proof requires more than distinct source names.

Primary reading

• LLVM Language Reference: LLVM Project

Open the study and save your work →