COL731: Advanced Compiler Techniques
Sem I, 2023-24
Home
–
Administrivia
–
Labs
–
Lecture Videos
(start at Module 125)
Course contents
Vectorization algorithms (1-2 weeks)
Undefined behaviour in source and IR (1-2 weeks)
Polyhedral transformations for locality and parallelism (8-9 weeks)
Hoare logic and predicate transformers (1-2 weeks)
Automatic invariant inference (1-2 weeks)
Superoptimization (1-2 weeks)
Program equivalence checking (1-2 weeks)
References
Paper on
Superword-Level Parallelism
(for vectorization and superword-level parallelism).
Chapters 11, 12, and 13 of the
Dragon book (updated second edition)
(for polyhedral transformations and undefined behaviour).
Paper on
incorrectness logic
.
Paper on
automatic invariant inference
.
Papers on superoptimization (
Massalin's original paper
,
peephole superoptimization paper 1
,
peephole superoptimization paper 2
,
stochastic superoptimization
,
equality saturation
).
Papers on program equivalence checking (
data-driven
,
counterexample-guided
).
Lecture schedule
Week
Dates
Material
1
24-28 July
Background on Compiler Design
Intermediate Representation Design Considerations
Superword-Level Parallelism : Introduction
2
31 July-4 Aug
Superword-Level Parallelism
3
7-11 August
Youtube Video Lectures
Module 125: Need for Locality
Module 126: Introduction to Matrix Multiplication
Module 127: Blocking in Matrix Multiplication
Module 128: Introduction to the Polyhedral Framework
Module 129: Affine Transform Theory
Module 130: Fourier Motzkin Method for Polyhedron Projection
Meeting 2.1: Interaction Meeting on Compiler Design Modules 125-130
Summary Slides: Lecture Modules 125-130(pdf)
Summary Slides: Lecture Modules 125-130(PPT)
4
14-18 August
Youtube Video Lectures
Module 131: Changing Axes using Fourier Motzkin Method
Module 132: Affine Array Accesses
Module 133: Data Reuse
Module 134: Self Reuse
Module 135: Self Spatial ReUse
Meeting 3.1: Interaction Meeting on Compiler Design Modules 131-135 (Fourier Motzkin, Reuse)
Summary Slides: Lecture Modules 131-135(pdf)
Summary Slides: Lecture Modules 131-135(PPT)
5
21-25 August
Youtube video Lectures
Compiler Design Module 136 : Group Reuse
Compiler Design Module 137 : Comparing Different Types of Reuse
Compiler Design Module 138 : Array Data Dependencies
Compiler Design Module 139 : Solving Data Dependence Constraints
Compiler Design Module 140 : Synchronization Free Parallelism Example
Meeting 4.1: Interaction Meeting on Compiler Design Modules 136-140 (Data Dependence, Sync-Free Parallelism)
Summary Slides: Lecture Modules 136-140(pdf)
Summary Slides: Lecture Modules 136-140(PPT)
6
28 Aug-1 Sep
Youtube video Lectures
Compiler Design Module 141 : Affine Space Partitions
Compiler Design Module 142 : Space Partition Constraints
Compiler Design Module 143 : Space Partitioning Example
Compiler Design Module 144 : Space Partitioning Constraints Example
Compiler Design Module 145 : Solving Space Partitioning Constraints Example
Meeting 5.1: Interaction Meeting on Compiler Design Modules 141-145 (Space Partitioning Constraints)
Summary Slides: Lecture Modules 141-145(pdf)
Summary Slides: Lecture Modules 141-145(PPT)
7
4-8 September
Youtube video Lectures
Compiler Design Module 146 : Solving Space Partitioning Constraints in General
Compiler Design Module 147 : More on Solving Space Partitioning Constraints
Compiler Design Module 148 : Simple Code Generation Strategy for Synchronization Free Parallelism
Compiler Design Module 149 : Tightening the Loop Bounds for Synchronization Free Parallelism
Compiler Design Module 150 : Splitting Loops to Eliminate Tests for Synchronization Free Parallelis
Meeting 6.1: Interaction Meeting on Compiler Design Modules 146-150 (CodeGen after Solving SpacePart Constraints)
Summary Slides: Lecture Module 146-148(PPT)
Note: Slides do not contain Module 150
8
11-15 September
Youtube video Lectures
Compiler Design Module 151 : Primitive Affine Transforms
Compiler Design Module 152 : Affine Transform #3 - ReIndexing
Compiler Design Module 153 : Affine Transform #4 - Scaling
Compiler Design Module 154 : Affine Transform #5 - Loop Reversal
Compiler Design Module 155 : Affine Transform #6 - Loop Interchange
Compiler Design Module 156 : Affine Transform #7 - Loop Skewing
Meeting 7.1: Interaction Meeting on Modules 151-156 (Primitive Affine Transforms)
Summary Slides: Lecture Module 151-156(pdf)
9
18-22 September
Youtube video Lectures
Compiler Design Module 161 : Introduction to Pipelining
Compiler Design Module 162 : SOR Example
Compiler Design Module 163 : Fully Permutable Loops
Compiler Design Module 164 : Pipeline Code Generation
Compiler Design Module 165 : Blocking for Fully Permutable Loops
Meeting 8.1: Interaction Meeting on Modules 161-165 (Pipelining, Blocking)
Summary Slides: Lecture Module 161-165(pdf)
Summary Slides: Lecture Module 161-165(PPT)
10
25-29 September
Youtube video Lectures
Compiler Design Module 166 : Undefined Behaviour Semantics
Compiler Design Module 167 : Undefined Behaviour In IR
Compiler Design Module 168 : Introduction to Poison Values
Compiler Design Module 169 : Poison Value Operational Semantics
Compiler Design Module 170 : Immediate vs Deferred UB
Meeting 9.1: Interaction Meeting Modules 166-170 Undefined Behaviour, Poison Values
Summary Slides: Lecture Module 166-170(pdf)
Summary Slides: Lecture Module 166-170(PPT)
11
9-13 October
Youtube video Lectures
Compiler Design Module 171 : Undefined Values
Compiler Design Module 172 : Undef Value Operational Semantics
Compiler Design Module 173 : WHYs of Undef and Poison Value Semantics
Compiler Design Module 174 : Freeze Opcode in LLVM
Compiler Design Module 175 : Introduction to Static Analysis Approaches
Meeting 10.1: Interaction Meeting Modules 171-175 (Undef, Poison, Freeze, and their WHYs, Abstract Interpretation)
Summary Slides: Lecture Module 171-175(pdf)
12
16-20 October
Youtube video Lectures
Compiler Design Module 176 : Assertions
Compiler Design Module 177 : Invariants
Compiler Design Module 178 : Verification Conditions
Compiler Design Module 179 : Verification Conditions for If then else
Compiler Design Module 180 : Verification Conditions for the Sequence Operator
Meeting 11.1: Interaction Meeting Modules 176-180 (Assertions, Invariants, Verification Conditions)
Summary Slides: Lecture Module 176-180(pdf)
Summary Slides: Lecture Module 176-180(PPT)
13
23-27 October
Youtube video Lectures
Compiler Design Module 181 : Sequencing with If Then Else
Compiler Design Module 182 : Exponential Paths Problem
Compiler Design Module 183 : While Loop Verification Condition
Compiler Design Module 184 : Proof Method
Compiler Design Module 185 : Hoare Logic Rules
Meeting 12.1: Interaction Meeting Modules 181-185(Verification Conditions, Exponential Paths Problem, Hoare Logic)
Summary Slides: Lecture Module 181-185(pdf)
Summary Slides: Lecture Module 181-185(PPT)
14
30 Oct - 3 Nov
Youtube video Lectures
Compiler Design Module 186 : Hoare Logic Rule for While
Compiler Design Module 187 : Predicate Transformers
Compiler Design Module 188 : More Weakest Precondition Rules
Compiler Design Module 189 : Weakest Liberal Precondition
Compiler Design Module 190 : Weakest Liberal Precondition for a While Loop
Meeting 13.1: Interaction meeting on Modules 186-190 (Weakest Precondition, Verfication)
Summary Slides: Lecture Module 186-190(pdf)
15
6-10 Nov
Superoptimization: peephole superoptimization, stochastic superoptimization, equality saturation, program equivalence checking
16
13-17 Nov
Program equivalence checking