1 — Polyhedral model for loop nests
1 — Polyhedral model for loop nests
What it is (one-line): represent each dynamic statement instance as a point in an integer
vector space (iteration vector) and model iteration domains, memory accesses and
schedules as affine/polyhedral objects so complex loop transformations can be expressed
as affine maps.
Key concepts
● SCoP (Static Control Part) — loop nests/statements with affine bounds and affine
array subscripts; only these are modeled precisely.
● Iteration domain — the set of all dynamic instances of a statement; represented
as a parametric polyhedron.
● Affine schedule Θ: assigns an execution timestamp (scalar or vector) to each
instance; we restrict schedules to affine functions of iterators & parameters.
(Formula form used in theses: Θ_S(x) = T_S · [x; n; 1].)
● Dependence polyhedron — set of instance pairs (source,target) that access the
same memory location with at least one write; used to derive legality constraints on
schedules.
● Legal schedule — an affine schedule that lexicographically respects all
dependences (each dependence must be carried or satisfied in order).
Why it’s useful : expresses arbitrarily complex compositions (interchange, skewing, tiling,
fusion) as a single affine transform; enables formal legality checks and automated code
generation.
SHORT ANSWER:
The polyhedral model maps loop instances to integer points in polyhedra (iteration
domains) and uses affine schedules to reorder instances. Dependences are represented
as polyhedra; a schedule is legal iff it respects those dependences. This uniform
algebraic view allows automated, provably legal transformations such as tiling, skewing,
fusion and vectorization.
2 — Tiling, skewing, fusion, vectorization — concise definitions + how
they interact
Tiling (aka blocking)
● What: group close-by iteration points into tiles; in code terms this introduces
outer tile loops and inner intra-tile loops. Purpose: increase data locality /
reuse and reduce working set per tile.
● Legality in polyhedral model: a contiguous sequence of schedule
dimensions is tilable (a tilable band) if they weakly satisfy the same
dependences (permutability). If not tilable, enable with skewing.
Skewing
● What: change loop bounds by adding multiples of an outer iterator (shifting
iteration domain shape). Use: transform dependences’ direction vectors so
tiling becomes legal. Typical enabling step for parametric tiling.
Fusion & distribution
● Fusion: merge two loop nests into one (reduces data movement between
loops, increases locality but may change parallelism/vectorization
opportunities).
● Distribution: split a loop nest into several loops (can expose parallelism or
enable different tilings).
● In polyhedral terms, fusion/distribution choices are modelled as statement
interleavings / total preorders; Pouchet shows how to encode the set of legal
interleavings and prune it. This lets the optimizer search fusion choices while
preserving semantics.
Vectorization
● What: inner loop transformations (often innermost dimension) to use SIMD
instructions — requires regular memory access patterns and inner-loop
parallelism (no loop-carried dependence at that vector width).
● Interaction: tiling and fusion change the inner loop shape and dependencies
— they can enable or prevent vectorization. The best combination is target-
dependent. The thesis emphasises that vectorization and coarse-grain
parallelism trade off and must be considered jointly.
● What: change loop bounds by adding multiples of an outer iterator (shifting
iteration domain shape). Use: transform dependences’ direction vectors so
tiling becomes legal. Typical enabling step for parametric tiling.
Just-In-Time compilation
Just-In-Time compilation
Interpreted code has the attractive property that it can be totally independent of the
machine and operating system it runs on: the same program file can be used on any
system that has a working interpreter for it. However, interpreted code runs slower
than compiled code, so there is a clear trade-off here.
One way to largely avoid the overhead of interpretation is to let the interpreter
generate machine code for an interpreter code segment, right before that code is
needed. This is called Just-In-Time compilation (JIT compilation). Once the code
has been compiled, it is usually kept for the remainder of the run. The advantage of
this approach is that it hides much of the compilation process from the user, and that
the generated code can be adapted to a particular processor and even the particular
execution statistics of the program run. Although the technique has been popularized
by Java implementations, it is by no means restricted to that language. Many earlier
interpreters already did some form of compilation, and the techniques of Java JIT
implementations are now applied to interpreters for other languages.
Obviously the technique only works if the compilation process is fast enough to
be acceptable.
Modern JIT implementations use a number of techniques to achieve
this: Their compilers have been carefully tuned to be as fast as possible while still
producing fast code. They only compile those parts of the code that contribute significantly
to the execution time of the program (the “hot spots” of the program).
In some cases they even use multiple quality levels: a fast compiler yielding code
of moderate quality for the bulk of the code, and a more sophisticated but slower
compiler for important hot spots.
As an alternative, Jung, Moon, and Bae [139] evaluate the possibility of preloading
extremely optimized code for Java classes onto the embedded device, and then
use an interpreter for the actual program. They find this to be a very convenient
way of achieving considerable speed-ups. The rationale for this approach is that the
“variable” part of the program often consists almost exclusively of method calls.
UNIT 7 IN CD
security, verification, and future trends: secure compilation and type-safe intermediate
representations-Compiler fuzzing and formal verification (e.g., CompCert)-Quantum
compilers, multi-target compilers, and neuromorphic systems
Compiler security involves ensuring that the compilation process does not introduce
vulnerabilities into software and that the compiler itself is trustworthy. Key areas include
the use of secure compilation techniques and intermediate representations, rigorous
verification methods like fuzzing and formal verification, and adapting to emerging
hardware like quantum and neuromorphic systems.
Security and Verification in Compilation
Secure Compilation and Type-Safe Intermediate Representations (IRs)
Secure compilation aims to preserve the security properties of the source code in the
generated machine code, preventing the compiler's optimizations from inadvertently
introducing or exposing vulnerabilities (e.g., removing code that clears sensitive data
from memory).
● Type-safe intermediate representations (IRs) are a crucial component. An IR is a
representation of the program used internally by the compiler for analysis and
optimization. A type-safe IR has strong semantic guarantees and ensures that
operations are performed correctly according to their data types, reducing the risk
of memory errors (like buffer overflows) and other type-related vulnerabilities in the
final executable. This design choice increases the integrity and reliability of the
compilation process, especially for safety- or mission-critical software.
Compiler Fuzzing and Formal Verification
These are two primary methods for validating the correctness and security of a compiler:
● Compiler Fuzzing: This quality assurance technique involves feeding the compiler
a large volume of random or unexpected test cases (source code snippets) to
identify crashes, errors, or instances where the generated code is incorrect. Tools
like Csmith have been instrumental in finding hundreds of bugs in widely-used
compilers like GCC and Clang. Fuzzing is effective at uncovering a wide range of
coding errors and security vulnerabilities that developers might not anticipate.
● Formal Verification (e.g., CompCert): This method uses machine-assisted
mathematical proofs to guarantee, with high assurance, that the executable code
produced by a compiler behaves exactly as specified by the source program's
semantics. The CompCert C compiler is a pioneering example of a production
compiler that is formally verified to be exempt from miscompilation issues. This
provides an unprecedented level of confidence for safety-critical applications, as it
ensures that any safety properties verified at the source code level automatically
hold true for the generated machine code.
Future Trends in Compilers
The evolution of computer architectures is driving significant changes in compiler design:
● Quantum Compilers: As quantum computing matures, compilers are being
developed to translate high-level quantum programming languages into low-level
instructions (like specific quantum gates and qubit operations) for various
quantum hardware platforms. A key challenge is managing hardware constraints
like qubit connectivity and entanglement operations efficiently. The Quantum
Intermediate Representation (QIR) is an LLVM-based effort to create a versatile,
standardized IR for quantum compilers.
● Multi-target Compilers: The rise of heterogeneous computing environments
(systems combining CPUs, GPUs, TPUs, etc.) necessitates compilers that can
target diverse architectures and optimize code for parallel execution across them.
Compilers with modular designs and unified intermediate representations (like
LLVM IR and MLIR) are essential for ensuring portability and efficient code
generation for these varied targets.
● Neuromorphic Systems: Neuromorphic computing, inspired by the structure and
function of the human brain, requires specialized compilers that can efficiently
map neural network models onto this new type of hardware. These compilers need
to manage the unique data representations and processing paradigms of
neuromorphic chips to enable new edge AI applications.
Security, verification, and future trends —
detailed explanation
Below I break each requested topic into: what it is, why it matters, how it works (key techniques),
practical examples, limitations/attacks, and where research is heading. I’ll keep it technical but
clear — useful for study, exams, or quick reference.
Secure compilation & type-safe
intermediate representations (IRs)
What & why
Secure compilation aims to ensure that security properties proven about source code (or
assumed at the source level) remain valid after compilation — even in presence of adversarial
contexts at the target (e.g., native machine code running in a hostile OS or linked with untrusted
libraries). A type-safe IR is an intermediate language whose type system enforces invariants
(memory safety, control-flow integrity, capability discipline) so that backends and optimizations
cannot violate those invariants.
Security goals
● Preservation of safety properties: memory safety, control-flow integrity (CFI),
confidentiality/integrity guarantees.
● Robustness under linking: compiled module should not lose guarantees when linked with
arbitrary (possibly malicious) code.
● Compiler correctness: transformations should be semantics-preserving or preserve a
weaker, explicitly defined security semantics.
Key techniques
1. Formal compiler correctness: prove that the compiled [Link] the source
semantics (or observational equivalence) — often using mechanized theorem provers
(Coq, Isabelle). CompCert is a classical example (see below).
2. Typed IRs / proof-carrying code: IRs with strong type systems that capture capabilities
(e.g., linear types, region types, effect types). These types are checked/maintained
through transformations.
3. Capability machines & memory isolation: target abstractions (capability pointers,
tagged memory) implemented by hardware or runtime that prevent certain classes of
memory corruption.
4. Secure linking and compartmentalization: compile to multiple compartments (modules)
with well-defined interfaces (calls/returns), and enforce boundaries via sandboxing or CFI.
5. Micro-policies / tag-based enforcement: propagate metadata (tags) on words and
perform checks on access patterns (hardware-accelerated or via interpreter).
6. Control-flow integrity & stack safety: inserting checks, using shadow stacks, or using
typed-call/return checking in IR to prevent control-flow hijacks.
7. Whole-program vs. modular approaches: proofs can be whole-program (harder to
scale) or modular (prove per-component invariants that compose).
Example of a type-safe IR idea (sketch)
● IR values carry static types: Int, Ptr<T>, Func(sig).
● Pointer types are capability-annotated: Ptr<T,cap> meaning only certain operations
allowed.
● Transformations are required to preserve types; untyped lowering must insert checked
casts (or fail).
Practical tradeoffs
● Stronger guarantees require heavier proof effort and sometimes runtime checks
(performance cost).
● Modular verification is essential for large systems but needs careful interface
specifications.
● Hardware support (e.g., tags, capabilities) can dramatically reduce runtime overhead.
Attacks & failure modes
● Incorrect assumptions about the linking environment.
● Compiler bugs that invalidate invariants when optimizations are unsound.
● Side-channels (timing, cache) often outside the scope of standard safety proofs.
Compiler fuzzing and formal verification
(e.g., CompCert)
Compiler fuzzing — what & how
● Fuzzing of compilers aims to find compiler bugs (crashes, miscompilations). Two common
families:
○ Random program generation (mutation-based): generate random or slightly
mutated programs and feed to compiler to observe crashes or runtime differences.
○ Differential testing / cross-compiler testing: compile the same source with
multiple compilers/backends or different optimization levels and compare
semantics (e.g., run-time outputs). Discrepancies indicate potential miscompilation.
○ Metamorphic testing: apply semantics-preserving transformations to the source
and check that behavior is preserved after compilation.
● Instrumentation: fuzzers often instrument generated test cases to avoid undefined
behavior in the source (UB in C is a common pitfall) by restricting the generator to well-
defined subsets or inserting checks.
● Oracle problem: determining if a compiler output is semantically correct is nontrivial;
differential oracles and property-based checks are used.
Practical methods/defenses
● Use typed front-ends or intermediate-checks to avoid undefined behavior in generated
tests.
● Integrate sanitizers and runtime checks to catch miscompilation that leads to incorrect
behavior.
● Use compiler-verified transformations (see formal verification).
Formal verification (CompCert as exemplar)
● What it is: mechanized proofs that a compiler preserves program semantics. CompCert is
a full C compiler (subset of C) verified in Coq: each compilation pass is proved semantics-
preserving.
● Why it's powerful: eliminates a large class of bugs (miscompilations), gives extremely
strong confidence for critical systems (avionics, medical, crypto).
● How it’s done:
○ Define formal semantics for source language and target assembly.
○ For each transformation (optimization, lowering), prove a refinement relation:
compiled code simulates source behavior (no new behaviors).
○ Compose passes to get end-to-end correctness.
● Limitations:
○ Usually supports a subset of the source language (handling full C requires
nontrivial work due to UB, complex undefined behaviors).
○ Proving and maintaining proofs is expensive and hard to scale to aggressive,
heuristic optimizations.
○ Non-functional aspects (performance, side channels) are not typically verified.
Synergy between fuzzing and formal methods
● Fuzzing finds practical bugs in unverified compilers; formal methods provide a higher bar
but are expensive.
● Verified components (e.g., verified register allocator) can be obtained incrementally while
using fuzzing to test unverified parts.
Quantum compilers
What they do
Quantum compilers transform high-level quantum programs (quantum circuits, algorithms) into
low-level instructions suited to a specific quantum hardware backend (native gate set, qubit
topology, coherence constraints).
Key challenges
1. Qubit mapping / routing: map logical qubits to physical qubits on hardware with limited
connectivity; insert SWAPs or teleportation to realize required interactions.
2. Gate decomposition & synthesis: express high-level gates or rotations using the target
gate set (e.g., decompose arbitrary single-qubit rotations into U3, Rz + RX, or Clifford+T).
3. Noise-aware optimization: minimize circuit depth and noisy gates; reorder gates to
exploit idle times and reduce accumulated error.
4. Resource tradeoffs: gate count vs depth vs qubit count; sometimes increasing
parallelism reduces depth but increases CNOTs (which may be noisy).
5. Measurement scheduling & classical control: mix quantum operations and
measurement-driven classical branches.
6. Error mitigation & compilation-aware calibration: adapt compilation to current device
calibration (error rates, variability).
Typical passes
● High-level optimizations: algebraic simplification of gates, cancel adjacent inverse gates,
merge rotations.
● Synthesis into universal gate set: approximate arbitrary unitaries with a sequence from
the hardware-supported gate set, optimizing for T-count or fidelity.
● Placement & routing: find qubit placement and SWAP insertion to satisfy connectivity
with minimal overhead.
● Scheduling: order gates respecting dependencies and device constraints (timing,
parallelism).
● Noise-aware mapping: choose qubits and paths based on error rates and coherence
times.
Example metrics optimized
● Circuit depth (critical for decoherence).
● Two-qubit gate count, especially CNOT/Entangling gates (usually highest error).
● T-count (important in error-corrected logical circuits).
● Fidelity estimate (aggregate expected success probability given hardware noise model).
Future directions
● Integration with error-correction-aware compilation: compile to logical gates for fault-
tolerant codes.
● Machine-learning for routing and gate synthesis.
● Co-design with hardware to expose useful primitives (e.g., native multi-qubit gates).
Multi-target compilers
What & why
Multi-target (retargetable) compilers generate code for many different target architectures (ISAs,
accelerators) from a common frontend/IR. This is crucial for heterogenous systems (CPU + GPU
+ FPGA + accelerators).
Architectural patterns
1. Front-end / IR / back-end separation: one or multiple frontends (language parsers)
target a common IR; many backends lower IR to specific ISAs.
2. Pluggable backends & codegens: backends encapsulate register allocation, instruction
selection, scheduling for the target.
3. Target description languages: use declarative descriptions of instructions and
constraints to automatically generate parts of the backend (e.g., instruction-selection
DAGs).
4. Multi-level IRs: high-level IR for language semantics, mid-level IR for optimizations, low-
level IR closer to machine (with explicit registers).
Challenges
● Maintaining portability vs optimization: target-specific optimizations give performance
but hurt portability; need infrastructure to selectively apply passes.
● Heterogeneous code emission & scheduling: orchestrating kernels that run on different
targets, handling data movement and synchronization.
● Verification across targets: correctness of lowering for many targets is a large
verification burden.
● Hardware-specific features: vector units, different memory hierarchies, specialized
instructions (tensor cores), and their fast exploitation.
Practical techniques
● Tuning & autotuning: use profile-guided optimization and autotuning to specialize
generated code per target.
● Partitioning & offloading: decide which portions of program to run on which device
(compute offload decisions).
● Unified runtime & memory model: abstract device memory and transfers, or present
explicit APIs to manage them efficiently.
Trends
● Compilers increasingly provide end-to-end pipelines for heterogeneous dataflow (e.g., ML
compilers that target CPU/GPU/TPU/FPGA).
● Intermediate dialects for accelerators (tensor dialects, MLIR-like ideas) that can be
lowered to multiple hardware-specific backends.
Neuromorphic compilers and
neuromorphic systems
What neuromorphic systems are
Neuromorphic hardware is designed to mimic neural computation (spiking neural networks,
event-driven processing), often for energy-efficient inference of brain-like models. Examples are
event-driven chips that implement spiking neurons and synapses in hardware.
Neuromorphic compilation goals
● Map high-level neural networks (rate-based or spiking) to spiking hardware primitives.
● Translate dense/ANN models into SNNs (spiking neural networks) when needed.
● Optimize for event-driven execution, temporal coding, and hardware constraints (limited
synapse counts, weight precision, routing topology).
Key steps in neuromorphic compilers
1. Model conversion: convert an ANN (e.g., ReLU CNN) to an SNN, or express the model
as a collection of neuron/synapse parameters compatible with the hardware.
2. Temporal encoding: decide how to represent activations as spike trains (rate coding,
latency coding, population coding).
3. Resource mapping: assign neurons and synapses to physical cores/chips with limited
connectivity.
4. Routing and pruning: configure sparse connectivity and prune to fit memory and routing
constraints.
5. Calibration and quantization: map synaptic weights to hardware-supported levels and
compensate for device nonidealities.
6. Event scheduling & coalescing: pack events to reduce communication overhead and
latency.
Challenges
● Translating high accuracy ANNs into SNNs without large accuracy loss is difficult.
● Hardware imposes strict limits (fan-in/fan-out, weight precision, neuron models).
● Tools and standards are immature compared to mainstream ML stacks.
● Debugging and profiling is harder due to temporal/spiking nature.
Where neuromorphic compilers are useful
● Ultra-low-power sensing and always-on applications (IoT, edge sensors).
● Temporal pattern recognition (spike-based, low-latency tasks).
● Research into alternative computing paradigms and brain-inspired models.
Cross-cutting future trends & research
directions
1. Verified, modular compiler components
Instead of verifying whole monolithic compilers, focus on verifying critical transformation
components (IR passes, register allocator, code gen for security-critical kernels). Combine
formal proofs with empirical testing.
2. Hardware-assisted secure compilation
Co-design with hardware features (capabilities, tags, memory safety mechanisms) to
cheaply enforce invariants; compilers will target these hardware primitives.
3. Security as a compilation objective
Optimize not only for performance/size but also for confidentiality/integrity and side-
channel resistance — e.g., constant-time code generation and leakage-aware
optimizations.
4. Noise- and device-aware quantum compilation
Compilers that take live device calibration into account, adaptively optimizing circuits for
fidelity, and integrate error mitigation techniques.
5. Unified IRs and ecosystems for heterogenous targets
Middle layers (like MLIR-style) that expose target-agnostic dialects yet make it easy to
progressively lower for diverse accelerators.
6. AI-driven compiler heuristics
Use ML to predict good optimization sequences, register allocation strategies, and routing
for quantum and neuromorphic mapping.
7. Bridging classical and neuromorphic/quantum toolchains
Tooling that integrates classical pre/post-processing with specialized hardware
compilation (e.g., pretrain classical networks then compile to spiking hardware with
minimal loss).
8. Tooling for continuous verification & testing
Integrate fuzzing, property testing, and formal methods into CI for compilers to catch
regressions and semantic bugs early.
Study / exam checklist (concise)
● Define secure compilation and type-safe IR. Explain why linking with untrusted code
breaks naive guarantees.
● Be able to list and describe: typed IRs, capability machines, micro-policies, CFI, shadow
stacks.
● Explain CompCert style verification: semantics, refinement proofs per pass, end-to-end
composition, pros/cons.
● Describe compiler fuzzing methods: random generation, differential testing, metamorphic
testing; explain UB problem in C.
● For quantum compilers: know qubit mapping, gate decomposition, routing, metrics (depth,
two-qubit count).
● For multi-target compilers: describe frontend/IR/backend separation, target description,
autotuning, heterogeneous offload concerns.
● For neuromorphic: explain spike encoding, SNN mapping, hardware constraints, use
cases (low-power sensing).