Optimization And Program Rewriting

Author: Asher Wolfstein

Published under the auspices of the University of Neo-Transylvania Experimental Research

This is Part 7 of a proposed 18-part series titled Failed Abstractions: Interfaces Gone Wild.

Optimization involves replacing one program form or execution plan with a more optimal version, and it is based on the claim that the change preserves the relevant aspects of the given semantic contract. For example,

constant folding means that an operation performed on known inputs is substituted with its result;
dead-code elimination involves removing paths considered incapable of influencing the permitted observations;
inlining consists of replacing a call site with a customized version of the function body;
loop transformations involve modifying the loop iterations, perhaps unraveling it;
vectorization comprises formatting scalar instructions into vectors; and
scheduling involves rescheduling target actions based on dependencies.

These techniques are essential to much of contemporary performance engineering, and the validity of these methods can range from heuristic confidence based on testing to machine-checked proofs. Their relevance in terms of “failed abstractions” stems from the qualification in the phrase “relevant observations“: an optimization is very often, in one or more respects, not equivalent to the artifact it transforms.

Bottom-Driven Semantic Monotonicity is a proposed discipline for building Dominant machines (higher layers) in which the augmented state and its operations preserve a pre-established Submachine identity (lower layer) by virtue of the Submachine’s Dominance Condition. This identity is verified by the consistency of an abstract Projection onto the Submachine (lower-layer) state, and verification continues via the ability to provide traces thereof after each step along the line. For optimization, this means dealing with transformations of programs as versioned execution plans, bound by assumption and equivalence contracts. A translative change occurs, as the optimal plan becomes active while the original becomes operationally inactive, but the transformative process does not

acquire authority to erase its source,
conceal changed observations, or
present its contextual judgment as timeless program identity.

For more information regarding these terms, see Translation As A Transfer Of Semantic Authority.

Why Rewriting Is Reasonable

A typical program describes a generalized relationship in a way that is understood by the engineer and can be applied to different input values, whereas an implementation uses information that is not available or is difficult to obtain at the source level. For example,

constants can be determined after configuration;
type analysis could show that there is only one target for dynamic dispatch;
loop bounds and memory alignment could enable instruction vectorization;
profiling data can show which path is most frequently taken; and
the target hardware may offer fused instructions.

Through the elimination of redundant work, it is possible to reduce latency, code size, memory traffic, and energy consumption, while combining specialization enables the use of abstractions throughout a system at an “affordable” cost.

Contrary to how it might at first appear, the idea on which these changes are based is not inherently obscure.

When a program fragment $P$ is replaced by $P^{\prime}$ , the optimizer is claiming that $A \vdash P \approx_O P^{\prime}$ based on the observations $O$ and the premises $A$ . A proper transformation involves choosing the right source pattern, checking that the assumptions are correct, producing the right fragment, and making sure that the relation prescribed by the language is maintained through compilation.

The problem under examination appears, however, when both the subscript and the premises are omitted from the authoritative account, so that contextual equivalence is presented as identity and facts that were excluded from $O$ are then treated as if they had never been part of the execution.

A Floating-Point Loop Under Multiple Observation Contracts

Consider a function which performs scaling and addition of floating-point numbers in their original order:

scaled_sum(values, count):
    total = 0.0
    for i from 0 to count - 1:
        total = total + values[i] * 2.0
    return total
Code language: JavaScript (javascript)

A scalar approach would involve loading one element, multiplying it, adding it to the running total, and then repeating this process. However, if the optimizer knows that values refers to a contiguous and aligned area of at least count elements, that the target offers vector operations, and that the language or compilation mode allows reassociation of floating-point additions, it can create a plan which deals with multiple elements at the same time.

vector_total = [0.0, 0.0, 0.0, 0.0]
i = 0
while i + 4 <= count:
    lane = load4(values + i)
    vector_total = vector_total + lane * [2.0, 2.0, 2.0, 2.0]
    i = i + 4
total = horizontal_sum(vector_total)
while i < count:
    total = total + values[i] * 2.0
    i = i + 1
return total
Code language: JavaScript (javascript)

You see, for real-number arithmetic, the two expressions are equivalent. But for finite floating-point arithmetic,

grouping can lead to differences, such as in rounding;
treatments of NaN or signed zero may differ under some rules;
vector loads might fail at a different place than scalar loads, such as when a page boundary is crossed;
speculative load may not be desirable if the counter is, again, protecting a boundary;
subnormals may be treated differently based on different modes for the target; and
while the bit representations remain the same, memory access patterns and energy consumption can be different.

If another thread modifies the array, the order in which the numbers are generated might change, and the language may treat such a race condition as undefined behavior. A debugger would step through fewer apparent iterations, while a profiler would attribute time to vector instructions; however, a side-channel observer could distinguish the plans.

The fact that there are such differences does not mean the vectorization is wrong; rather, it shows that it is correct under certain conditions.

In cases where the contract allows floating-point reassociations, ensures that padding is available, avoids concurrent mutations, and is concerned only with the result being within the allowed range of effects, the vectorization strategy is legitimate and beneficial.

However, in cases where the contract places an absolute restriction on the source order or where a memory safety model disallows widening access, the vectorization strategy may not work. A system that records only “loop vectorized” leaves the most important part of the semantic claim, at least in regard to the proposed framework, unstated.

The optimization rules depend on the language in question. In some cases the deterministic trace is preserved; in others only the final values are kept; in some instances nondeterministic behavior is improved by selecting one of the behaviors which were already allowed; in some cases termination is preserved only on the basis of a given condition; and in still other cases the optimizations are valid only when the program contains no undefined behavior. Optimizations designed to preserve security may require constant-time or information-flow observations that are ignored by ordinary functional correctness checks. Optimizations intended to preserve debugging information may need to include mappings of variable availability and statement boundaries, since the optimizations need not provide them.

The optimizer may also make use of evidence obtained from other sources:

Alias analysis might show that two memory areas do not overlap.
Range analysis might prove that an index is safe.
Type information might reduce the known applicable number of possible dispatches.
Profile data could indicate the probability of a branch.
And the target description itself specifies the instruction’s behavior.

Once a rewrite has become authoritative (see Translation As A Transfer Of Semantic Authority), these evidential dependencies become part of the reason why it is entitled to be executed. If a profile is stale, an alignment assumption invalid, or a target rule inaccurate, the generated execution plan may still fail even though the rewrite algorithm is correct in a developmentally local sense.

A reliable explanation, therefore, needs to treat assumptions as first-class supports rather than regard them as temporary compiler state that disappears when the code is emitted.

Four Consequences Of Silent Substitution

For more information on the definitions of these consequences, see Translation As Transfer Of Semantic Authority: The Consequences.

Semantic Drift occurs when the optimizer retains fewer observations than users or downstream consumers need. As in the aforementioned examples,

numerical optimizations might alter the rounding mode;
dead code optimizations might eliminate a write that is no longer visible to the device or to someone operating under a different memory model;

And further, tail recursion might make it impossible to look at the stack at an inspection point; and common subexpression optimizations could combine two subexpressions whose separate failures were source-visible. A transformation may be semantically valid with respect to one contract and yet semantically unsound with respect to another, underscoring the importance of considering the specific context in which the transformation is evaluated.

Opaque Responsibility arises because an optimized effect is almost always the result of several analyses and transformations. In this case, it becomes unclear whether the invalid vector loop access is caused by

the source preconditions,
the range analysis,
the aliasing assumptions,
the vectorization phase,
the target legalization phase,
the allocator runtimes, or
the target description.

Even though reports on the compilation process may show what transformation was performed on a piece of code, there is often no clear chain of causality from the transformed instruction to its premises preserved long-term.

Epistemic Discontinuity occurs when the operations on sources are copied, combined, restructured, or deleted:

An inline body can have multiple target occurrences.
A folded expression may have zero target occurrences.
A scheduled instruction may be involved in multiple source expressions.
And a dead branch will remain only as a proof fact.

The debugger will often describe the source based on the optimization run and, in some cases, as experience shows, it may show the variable as unobservable or indicate that lines were executed out of order in a manner that cannot be anticipated at the source level.

This does not mean that the description provided by the debugger is incorrect but that the correspondence is not one-to-one.

Conceptual Dishonesty takes place in cases where the optimized version of the program is represented as the direct implementation of the source code, even though the observed results have been significantly altered without revealing this fact, or the representation of the source code contains operations which have actually taken place but without making any mention of the fact. The reader would do well to remember that the concept of Conceptual Dishonesty is not applicable merely because of structural differences in the target; it applies only if the system claims continuity beyond the proper level of the equivalence relation.

The Objectivist Diagnostic

The Objectivist analogy (see Translation As Transfer Of Semantic Authority: The Epistemology Of Abstraction) regarding optimization relies on the absence of measurements (**measurement omission**).

To prove equivalence, the optimizer selects observations that show which differences make sense: final values may be counted, but other aspects such as the order of instructions, allocations, timings, power, or fault locations need not be taken into account.

This is a legitimate approach within the framework where this happens.

The abstraction becomes ungrounded (”floating”) when omitted measurements are treated as irrelevant outside that context or effectively denied because the active plan no longer exposes them.

Similarly, the optimized configuration is a condensed self-contained operational system supported by analysis facts and source structure. The loss of these references means the design still holds in a computational sense but lacks traceability to the source representation.

Ayn Rand’s Objectivist epistemology alone does not guide what observations the language should conserve, or whether the internal workings of a compiler should last forever. What it demands is only that there should be proper contextualization and that any judgment made above the level of units and distinctions involved should be answerable to them.

A Versioned Plan With A Declared Contract

An optimizer oriented towards Bottom-Drive Semantic Monotonicity would add the plan, along with its warrant, to the machine’s artifact field. For example, a simplified record could be:

plan:scaled_sum.vector.v12
  predecessor: plan:scaled_sum.scalar.v3
  supports: source-loop:scaled_sum.4
  rule: vectorize-reduction/v8
  assumptions:
    - memory-range-proof:mr.771
    - alignment-proof:al.772
    - no-concurrent-write:effect.119
    - target-mode:fp-relaxed.v2
  preserves:
    - termination under source preconditions
    - memory safety under memory-range-proof
    - result relation fp-relaxed-reduction/v2
  does-not-preserve:
    - source-order rounding
    - scalar fault locality
    - instruction-trace shape
  validation: translation-check:tc.8841

Activation includes additional facts that specify the environment and the decision upon the basis of which the plan becomes current. When execution events occur, they refer to the currently active plan and the Submachine actions that are actually carried out. Upon detecting contradictory runtime evidence, the system stores the invalidation and selects an alternative successor or predecessor plan to work on, while all previous execution instances retain the version and assumptions valid during their execution. And if a defect in the compiler is found later on, the deployed artifacts can be queried using the rule and validation identity, rather than the inevitable reconstruction process having to infer solely from the compiler version.

This design interprets Semantic Monotonicity as expansion of the evidence and artifact field, rather than making the absurd assertion that the active execution plan never changes. The current state is mutable since a plan can be activated, deactivated, invalidated, or reclaimed. The history showing how it gained and lost authority is accumulated through explicit relationships. It is important to make this distinction since optimization is by its nature selective and revisable; an architecture based on monotonicity that prevented revision would make adaptive execution impossible, while one that silently overwrote plans would merely rephrase the epistemic issue under a different name.

For Projection consistency, it is necessary for the optimized state to produce an honest Submissive account. It can result in the same source-visible outcome under the declared contract without having to recreate the scalar instruction trace, since pretending that the scalar loop actually took place would render Submachine state a floating abstraction with no correspondence to reality. A proposed framework-bound Projection would specify that the vector operations implement the source loop via fp-relaxed-reduction/v2 and provide the observations on which this dependency is based. Interpretive closure requires that activities of the Dominant machine-level resolve to the required Submachine activities or services in runtime that preserve their observable effects.

What May Be Retained And What May Be Proven

There is no need to store all rejected optimizations and all solver steps across all executions. A pass can retain the rule identity, the commitments regarding the input and output artifacts, the assumptions, the equivalence contract, the validation result, and sufficient information to reconstruct or audit the transformation. Regarding high-assurance systems, keeping the proofs or full pass traces can make sense. Alternatively, if the emphasis is on performance during build, only the provenance could be retained, while some executions could be selected for storage. In both cases, the audibility claims have to be scaled according to the amount of evidence that is kept.

The traditional approaches still hold significance in this context.

The translation validation approach can be applied to each generated program.
The proof-carrying transformations can provide machine-readable proofs.
The differential testing approach can find bugs in the compiler.
And the optimization reports can take on the form of the provenance approach rather than continuing as merely temporary human-readable reports.

Bottom-Driven Semantic Monotonicity does not rule out any of these techniques because their provenance alone is allegedly sufficient to ensure their accuracy; rather, it provides a complementary framework for relating them to the plan they are meant to authorize.

Costs and limits

The establishment of fine-grained plan versioning, as always, increases storage and indexing overhead and adds to runtime overhead when tracing the target actions. It also requires a well-disciplined vocabulary of observations in equivalence contracts, produces proof artifacts that can be much larger than the optimized code, and involves provenance requirements which prevent the compiler from reusing data structures or making in-place mutations.

In a dynamic setting, the number of versions is high, whereas profile-based and Just-In-Time (JIT) compilation generate plans quickly, thus making it impossible to save all the plans. Also, security concerns might prevent the saving of profiles, memory locations, and input-specific traces.

A policy of reclamation would have to distinguish among

content and commitment;
hot and cold data;
reproducible and irreproducible data; and
public data and data that is inspectable.

Even then, cryptographic identity proves integrity rather than semantic truth; a successful outcome could rely on incorrect assumptions made by the optimizer, and an equivalence relation could miss an important point that becomes relevant later.

One should understand optimization as an accountable contextual replacement, and because of its contextual nature, $O$ remains a human and institutional judgment as well as a formal one.

A transformed plan may be better suited to a specific task and correct according to the given relation, while differing from the initial version in its trace, expense, and explanation. Preserving that qualified history does not diminish optimization; it makes the optimizer’s genuine achievement legible by showing exactly which right to execute the transformed artifact has earned.

A Personal Note

I said the age of distraction is over. All of you would do much better to simply, finally, take what I say at face value.

Accessibility

Display Settings