Author: Asher Wolfstein
Published under the auspices of the University of Neo-Transylvania Experimental Research
This is Part 5 of a proposed 18-part series titled Failed Abstractions: Interfaces Gone Wild.
Compilation provides an expression defined in an abstract language with an executable form for another operational system, while lowering involves the (sometimes gradual) elimination, or breakdown, of features that the target system does not directly support.
Some examples include:
- A function invocation is decomposed into multiple discrete steps: argument transfer, control transfer, stack manipulation, and return;
- A checked array update is decomposed into index validation, address computation, loading, an arithmetic operation, storing, and handling of exceptional branches; and
- A tag and payload layout would represent the algebraic data constructor.
Such modifications represent engineering achievements that undeniably involve specifications for correctness and even, in some cases, proofs. Moreover, such changes represent shifts in semantic power because the Submission (lower-level artifact) makes the decision, while the Dominance (higher-level structure) is the main tool a programmer, specification, or reviewer uses to understand the task.
Bottom-Driven Semantic Monotonicity is a framework concerned with building a machine tower such that the Dominant (higher) state and actions (Dominances) maintain a defined Submachine (lower) identity, consistently project down to the Submachine state, and offer inspectable Submachine support for each novel operation introduced. When applied to compilation, the proposed framework treats an executable artifact as a plan or trace that has the authority to carry out a continuing Dominant action (Domination), while at the same time retaining the identities, the environmental premises, the rule applications, and the preservation contract upon the basis of which that authority was granted through the Dominance Condition of the Submachine. For more information on these terms, see the series introduction and its first post, Translation As A Transfer Of Semantic Authority.
The aim is neither to fashion a target code syntactically similar to the source code, no, that would be *shudder* highly unoptimized, nor is it to assume that a single representation will suffice for any analysis; the goal of monotonic extension, and semantic monotonicity in general, is to create abstractions that remain accountable to their underlying supports. See Translation As Transfer Of Semantic Authority: The Epistemology Of Abstraction.
Why Lowering Is Imperative In Conventional Systems
The design of source languages differs from that of target machines in several respects, and rightfully so. A source language can include features such as lexical scoping, exceptions, parametric functions, managed memory, pattern matching, coroutines, capabilities, and arithmetic rules that are independent of a specific processor. On the other hand, a physical or virtual target machine provides access to registers, memory operations, branches, calls, traps, and concurrency features.
Compilation allows the source language to present consistent, stable concepts while using different target machines. And it serves its role in the traditional translation-based abstraction well, by also enabling the hardware to remain fairly broad while supporting a variety of languages—a win-win.
The step-by-step lowering process also introduces intermediate stages at which complicated decisions become manageable:
- once the types are known, the data layout can be determined;
- once the target has been selected, the calling conventions can be established; and
- once the scheduling constraints are available, the instruction forms can be decided.
This manuscript most likely appears to many to regard lowering as invalid by some bizarro bias of the author, and if it doesn’t, then I implore you to humor me and pretend it does. A more reasonable criticism would concern the architectural status rather than the vocabulary, but who am I to tell you what to do? Either way, ‘lowering’ isn’t seen as invalid here.
A verified compiler can establish an exact and strong correctness relationship, while a more “consumer-friendly” compiler can still retain extensive provenance. The issue is whether the relationship which makes a target behavior an execution of a source operation remains an intrinsic part of the system’s usable identity, or whether the output becomes authoritative while the relationship continues as an external theorem, an implementation promise, a test history, and an incomplete debug mapping.
A Checked Update Across The Boundary
Consider a fictional source code evaluation system using left-to-right evaluation, checked indexing, checked integer arithmetic operations, and an out-of-bounds language exception.
items[index()] += increment()
The succinctness of its structure is deceptive, as this statement implies several promises.
First, items is evaluated to an array reference.
Second, the index() and increment() operations are invoked exactly once in the specified order.
Third, index is checked against the current length of the array.
Fourth, the item corresponding to index()’s evaluation is fetched.
Fifth, it is checked whether the addition-and-assignment operator would cause overflow.
Sixth… if *all* those prerequisites are met, only then is the new value assigned.
In different programming languages, arrays can be simultaneously modifiable, method invocations may throw exceptions, and modifications may be either atomic or non-atomic.
However, a simplified version of the plan may look as follows:
r_arr := load_binding itemsr_idx := call indexr_inc := call incrementif r_arr = null then trap NullReference(site_41)r_len := load_length r_arrif r_idx < 0 then trap Bounds(site_41, r_idx, r_len)if r_idx >= r_len then trap Bounds(site_41, r_idx, r_len)r_addr := element_address r_arr, r_idx, word_sizer_old := load_word r_addr(r_new, overflow) := add_checked r_old, r_incif overflow then trap NumericOverflow(site_41)store_word r_addr, r_new
As you can observe, this plan includes decisions that are not apparent in the source code; specifically, it has chosen an object layout with a length field, a representation for a word-sized element, a register convention, the order in which increment() is evaluated relative to the array reference being checked, certain trap points, and an address computation.
- If the source language demands that the null check be made before either of the calls, then the plan would be incorrect;
- if increment() is capable of mutating the array or of invalidating items, then additional rules are required for the address and length operations;
- if another thread can alter the array, then the plan must include a concurrency contract; and
- if a precise garbage collector can move the object, then r_arr must take part in runtime bookkeeping.
When lowering is carried out later, the plan will be divided into basic blocks, the values converted into Static Single Assignment (SSA) form, a redundant check might be eliminated based on a proven range fact, the target instructions will be selected, and the operations scheduled in an order that preserves only those observations which the language makes available.
The final result might be completely correct even though it has very little structural similarity with +=. More than one source operation can be reduced to a single target instruction, and one source operation can be spread out over code, runtime stubs, exception tables, allocator paths, and operating-system effects. It is precisely because of this many-to-many relationship that a simple source-position map cannot bear the full semantic weight. A position only states that an instruction is linked to a span; it doesn’t indicate which part of the source action the instruction carries out, what premises justified the order, what observations were retained, or which hidden runtime actions complete its behavior.
Equivalence Is Indexed By Observation
A compiler-correctness statement usually establishes a relationship between the behavior of the source code and that of the target by means of simulation, refinement, trace equivalence, or some other formally defined relation. The relevant point for this series is that equivalence is always indexed by observations and premises. In the case of a checked update,
- A contract could preserve termination, the values returned, the changes to memory visible in the source, the exception type, and the order of the calls, all while permitting differences in the allocation addresses, the number of internal instructions, and the contents of the registers.
- A contract oriented towards debugging could preserve statement boundaries and the ability to attribute faults.
- A real-time contract could impose latency constraints.
- A security contract could impose restrictions on memory-access patterns or on speculative effects which are not observed by the ordinary language semantics.
The same target plan can satisfy one relation and violate another without being inconsistent. For example,
- Bounds-check elimination can keep all the defined source results valid within the scope of a range proof even as it alters the fault produced from memory corruption;
- Instruction scheduling can maintain the sequential semantics while changing the way it interacts with memory-mapped devices; and
- A calling convention can preserve functional behavior even if it causes secret-dependent values to appear in locations accessible to an adversary.
Compilation fails epistemically when a qualified relationship is presented as an unqualified equality, so that facts left out of one proof context are regarded as not present at execution time.
The Characteristic Failures
Semantic Drift can occur when there is an interaction between lowering rules, target assumptions, undefined or implementation-defined behavior, runtime conventions, and hardware semantics.
For example,
- a high-level numeric operation might be implemented using a target operation with different overflow behavior,
- a source exception could become a target trap and thus alter the recovery procedure for resource cleanup, and
- an apparently immutable source value might depend on mutable runtime metadata.
Even if each choice is documented, a subsequent stage may silently strengthen or weaken the observation contract on which the earlier stage was justified.
Opaque Responsibility is especially pronounced because a source action can be realized jointly by compiler-generated instructions, linked runtime routines, loader relocations, operating-system services, and processor behavior. In case the actual output does not match the expected output, the compiler could cite target semantics, the runtime could quote compiler invariants, and the hardware could quote architectural permissions. Even though local agreements are required, in a world without actions for composition, responsibility remains distributed across the different documents and tools.
Epistemic Discontinuity occurs when the source, the compiler’s plan, the target artifact, and the execution trace all involve unrelated identities. Although debug tables can reconstruct variable ranges and locations, optimized values might not have a fixed location. A single instruction can correspond to several source constructs. A runtime stub may carry out effects on behalf of no directly visible instruction. The evidence in support of this remains in principle but is kept outside the normal state through which execution is observed.
The consequence of Conceptual Dishonesty arises when a highly-abstract conception is characterized as having an identity simpler or more fundamental than it deserves, given its actual realization. While it can be correct to treat items[index()] += increment() as a single step when reasoning about the contract of a sequential language, the use of such terminology is misleading if the atomicity, failure order, and side effects are assumed to derive from the syntactic simplicity of the expression, because, as you can see, a detailed analysis fails to confirm these features.
For more information on these consequences, see Translation As Transfer Of Semantic Authority: A Successive Convention.
The Objectivist Diagnostic
In the case of the epistemological analogy, the source operation represents a more general unit, the referents of which are a class of possible concrete instantiations defined by the source operation itself and its context. Authorization allows the Submissive behaviors to stand in for this more general unit. What usually goes wrong is that the referents of the operative are made external relative to the source concept in such a way that the source symbol still governs the claims even though the system can no longer tell how the claims were made true.
Measurement-omission is once again carrying out essential work. When a source-level addition omits the number of target steps and the position of the operands, it is so because these details are not relevant to the semantics of mathematical or ordinary language. It is not possible for such an addition to justify a claim regarding constant-time behavior while at the same time omitting the lower distinctions through which timing emerges. The validity of the abstraction depends on context, and the compilation procedure should neither force every context to retain all facts nor allow a weak context to support a stronger conclusion.
Compiled Plans As Extensions Of Machine Action
An account reoriented around Bottom-Driven Semantic Monotonicity might assign a stable action identity to the source update (for example, update:41) and then treat compilation as the addition of one or more realization plans. Each of these plans references the action, the versions of the compiler rule, the target context, the preservation contract, and the lower artifacts that it introduces:
source-action: update:41 contract: checked-update/v4 active-plan: plan:41.targetA.v7plan:41.targetA.v7 assumes: layout:array-i64/v3 assumes: calling-convention:targetA/v5 preserves: values, call-order, source-exceptions omits: exact timing, allocation addresses lower-actions: eval-index:41.1 eval-increment:41.2 bounds-check:41.3 checked-add:41.4 store:41.5
Even if instruction selection is performed later, it is still possible to obtain an even farther view into the Submachine stack. However, each generated instruction or trace interval still maintains a relationship with the plan action it supports. The support graph need not reflect the structure of the source in each instruction.
For example, a many-to-many support graph can show that several instructions jointly realize the bounds check (41.3), whereas a fused instruction is involved in both address calculation and data loading. The stubs represent the Dominant operation and the plan that created them, while the bounds exception represents the check operation, observed indices and lengths, and contract/source.
To achieve Projection consistency, a Dominant execution state must be able to recover an honest Submachine state when the machine’s boundaries are agreed on beforehand, whereas transition preservation means that instructions inherited from a Submachine behave in the same desirable way when observed from the Dominant machine. For interpretive closure to hold, the new source action has to provide either a finite Submachine trace or a declared resolver that can produce one. When dynamic inputs make it impossible for compilation to compute a trace in advance, closure can be relational: the plan specifies how each real Dominant transition leads to Submachine actions and records the resulting trace. Although the source operation remains semantically more rich than any individual path, its execution can be accounted for by referring to the path that was taken. We can only hope it was the one less taken.
The difference is that compilation metadata—either a support edge or an equivalence contract—is mandatory for the plan’s correctness. It is not an additional way to help a debugger determine whether a plan is valid; it is a prerequisite condition for plan validity. If a compiler was found to rely on an invalid assumption, it could include an invalidation record along with a new plan. The program that used the old plan still has its accurate history. Proof files and validation output from translations or tests can be added to the plan, allowing conventional compiler techniques to coexist with the continuity discipline.
Costs And Unresolved Problems
As always, there is a positive correlation between the granularity of the action sequence and the effects on code size, compilation time, trace size, and runtime bookkeeping, all generally known as overhead. In light of the fact that hardware typically does not store semantic information during transitions, there is a need for software to use additional means, such as side tables or tagged events, whose maintenance must be correct. Aggressive optimizations produce many-to-many mappings, which in turn require more storage space and increase query complexity.
Retention and access policies are needed because Submission traces might expose secrets, proprietary compiler decisions, memory layouts, or user data. In some configurations, only the commitments and identities of reproducible plans would be retained; in others, security-sensitive actions would be traced around; and in others, auditing would be weakened to improve performance. I know that the last is an option I have employed in my prototypes for “production” builds.
Because Bottom-Driven Semantic Monotonicity does not give an automatic answer to finding the Submissive boundary, a model that is built using a virtual instruction set would be unable to make qualified statements about what happens below that boundary.
Above all, being based on a lineage does not mean being correct. A compiler can accurately record the fact that an invalid lowering rule has produced a target artifact, and a commuting diagram can be constructed using a Projection that disregards the very observation in question. It is still necessary to have independent semantic specification, proof, testing, and adversarial review. The contribution put forward here is more limited in scope: compilation should produce accountable realizations whose authority is no greater than their stated preservation relation, and whose lower behavior remains traversable as the support for the higher actions they execute.