CPSC 539B, Compiler Theory

Term 2 (Spring) 2019

This is the course website for the 2019 Term 2 CPSC 539B Topics in Programming Languages: Compiler Theory.

Announcements

Date		Description
Mon, Dec 31		Added initial draft of course calendar, homework 0.
Mon, Jan 7		Added reference book.
Tue, Jan 8		Updated course calendar, including HW1 dates and type systems dates.
Wed, Jan 9		Added homework 1.
Wed, Jan 9		Added announcement about office hours.
Wed, Jan 9		Added another reference book.
Mon, Jan 14		Updated calendar, references to book; started list of papers.
Mon, Jan 14		Extended hw1; added instructions for resolving ambiguities in homework.
Tue, Jan 15		Fixed a problem with is-zero? in hw1; is-zero? is not defined on booleans.
Wed, Jan 16		Added lecture notes; added paper critique instructions.
Wed, Jan 16		Added hw2.
Mon, Jan 21		Updated calendar, added hw3.
Thu, Jan 24		Extended HW2 deadline.
Thu, Jan 24		Added notes on paper critiques.
Fri, Jan 25		Moved reading/presentation dates to fit in another paper; double check your dates.
Tue, Jan 29		Expanded presentation descriptions.
Tue, Jan 29		Added remaining homeworks.
Tue, Jan 29		Added project description.
Mon, Feb 11		Updated lecture notes.
Mon, Feb 11		Updated reading dates.
Mon, Feb 25		Updated reading dates.

1  Come to Office Hours!

The first part of this course involves a crash-course in programming languages theory techniques, so we can get to reading compiler correctness papers. Students who lack theory or PL background find it going a fast. If you have a hard time keeping up, please email me. At the very least, we can schedule office hours. I may also slow down and cover some of the basics in more detail.

Description

Compilers are responsible for writing almost all of the programs that get executed. Like all programs, compilers have bugs. But unlike most programs, when compilers have bugs, they can insert bugs into other peoples’ code and give programmers little recourse.

All compilers have bugs, and this course will teach you what a compiler bug is, how to reason about compilers so you better understand where the bugs are and how to prevent bugs if you ever write a compiler. This course will introduce some techniques of formal reasoning about programs, programming languages, and compilers. The course will then review recent compiler correctness research, and study the different ways a compiler can be correct, or incorrect, and how to implement a correct compiler and prove that it’s correct.

References

The vocabulary and notation will diverge somewhat from what I use in class. Grant et al.’s book may be somewhat easier to follow, but Harper’s book makes a lot of important details very precise.

Calendar

It is well-known that the best laid plans often go awry. Therefore, this calendar subject to change.

Date		Subject		Homework		Reading
Wed, Jan 2.		Prelims		HW 0 Assigned
Fri, Jan 4.		Syntax and operational semantics		HW 0 Due		Harper Chp 4.1, 5.1,5.2; Grant et al. Chp 2, 3
Mon, Jan 7.		Syntax and semantics continued				Chapters 1,2,3; Grant et al. Chp 2, 3
Wed, Jan 9.		Syntax and semantics; Type systems		HW 1 Assign		Grant et al. Chp 4
Fri, Jan 11.		Type systems				Grant et al. Chp 6 (particularly 6.2)
Mon, Jan 14.		Type systems continued				Harper Chp 6, Chp 22
Wed, Jan 16.		Logical Relations		HW 1 Due; HW 2 Assigned		Harper Chp 46.2
Fri, Jan 18.		Modeling assembly; the standard model compiler				Harper Chp 46.2
Mon, Jan 21.		Modeling CPS				Paper 1, Section 4
Wed, Jan 23.		Modeling closure conversion		HW 2 Due		Grant et al. Chapter 8; Paper 1, Section 5
Fri, Jan 25.		Modeling heap allocation				Grant et al. Chapter 8, Paper 1, Section 6
Mon, Jan 28.		Modeling code gen				Paper 1, Section 7
Wed, Jan 30.		Read and discuss paper 1		HW 3 Due		From System F to Typed Assembly Language
Mon, Feb 6.		Read and discuss paper 2		HW 4 Due		TIL: A Typed-directed optimizing compiler for ML
Fri, Feb 11.		Read and discuss paper 3		HW 5 Due		Proof Carrying Code
Wed, Feb 15.		Read and discuss paper 4		HW 6 Due		Dependently Typed Assembly Language
Wed, Feb 27.		Read and discuss paper 5		HW 7 Due		Formal Certificaiton of a Compiler Back-end
Mon, Mar 4.		Read and discuss paper 6		HW 8 Due		Compositional CompCert
Mon, Mar 4		---Project Proposal Due---		Proposal Due
Fri, Mar 8.		Read and discuss paper 7		HW 9 Due		Lightweight Verification of Separate Compilation
Wed, Mar 13.		Read and discuss paper 8		HW 10 Due		Typed Closure Conversion Preserves Observational Equivalence
Mon, Mar 18.		Read and discuss paper 9		HW 11 Due		The Correctness-Security Gap in Compiler Optimization
Wed, Mar 20.		Read and discuss paper 10		HW 12 Due		Securing the .NET Programming Model
Mon, Mar 25		Project 1 Presentation
Wed, Mar 27		Project 2 Presentation
Fri, Mar 29		Project 3 Presentation
Mon, Apr 1		Project 4 Presentation
Wed, Apr 3		Project 5 Presentation		Project write-up due

Lecture Notes

Thanks to Chris for taking notes in a format that I can quickly convert to HTML, lecture notes are available here.

Homework

Ambiguities in homeworks can be resolved by "whatever interpretation makes your happy", but please make a note of which interpretation you chose.

HW 0

Bookmark this website and visit it every Monday this semester. Tell me your favorite programming language and compiler. Submit this homework via email at the above email address.

HW 1

Due by email 1:59 pm (before class) on Wed, Jan 16, or by Fri, Jan 18 if you need some extra time. Please use the subject line "[CPSC 539B] HW1". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is described hw1.html.

HW 2

Due by email 1:59 pm (before class) on Fri, Jan 25. Please use the subject line "[CPSC 539B] HW2". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is described hw2.html.

HW 3

Due by email 1:59 pm (1 hour before class) on Wed, Jan 30. Please use the subject line "[CPSC 539B] HW3". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 1, From System F to Typed Assembly Language, as described in the papers section below.

HW 4

Due by email 1:59 pm (1 hour before class) on Mon, Feb 6. Please use the subject line "[CPSC 539B] HW4". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 2, TIL: A Typed-directed optimizing compiler for ML, as described in the papers section below.

HW 5

Due by email 1:59 pm (1 hour before class) on Fri, Feb 11. Please use the subject line "[CPSC 539B] HW5". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 3, Proof Carrying Code, as described in the papers section below.

HW 6

Due by email 1:59 pm (1 hour before class) on Wed, Feb 15. Please use the subject line "[CPSC 539B] HW6". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 4, Dependently Typed Assembly Language, as described in the papers section below.

HW 7

Due by email 1:59 pm (1 hour before class) on Wed, Feb 27. Please use the subject line "[CPSC 539B] HW7". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 5, Formal Certificaiton of a Compiler Back-end, as described in the papers section below.

HW 8

Due by email 1:59 pm (1 hour before class) on Mon, Mar 4. Please use the subject line "[CPSC 539B] HW8". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 6, Compositional CompCert, as described in the papers section below.

HW 9

Due by email 1:59 pm (1 hour before class) on Fri, Mar 8. Please use the subject line "[CPSC 539B] HW9". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 7, Lightweight Verification of Separate Compilation, as described in the papers section below.

HW 10

Due by email 1:59 pm (1 hour before class) on Wed, Mar 13. Please use the subject line "[CPSC 539B] HW10". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 8, Typed Closure Conversion Preserves Observational Equivalence, as described in the papers section below.

HW 11

Due by email 1:59 pm (1 hour before class) on Mon, Mar 18. Please use the subject line "[CPSC 539B] HW11". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 9, The Correctness-Security Gap in Compiler Optimization, as described in the papers section below.

HW 12

Due by email 1:59 pm (1 hour before class) on Wed, Mar 20. Please use the subject line "[CPSC 539B] HW12". Please submit either in plaintext or structure plaintext (org-mode, markdown) or as a PDF.

The homework is a critique of paper 10, Securing the .NET Programming Model, as described in the papers section below.

Papers

Starting approximately Feb 1., we (you) will start presenting and discussing papers in class.

Sign up for a paper at: https://docs.google.com/spreadsheets/d/1LahxpGU7oUnYspRwIw_yLt8S33D0n5TrAw4UVHJuj4w/edit?usp=sharing

Everyone should sign up as the presenter and discussion lead for at least one paper.

Paper Critiques

For each paper, you should send me a short (~2 paragraph) critique. Start by briefly summarizing the paper, then describing its strengths and weaknesses. These are due before the first class in which we discuss the paper.

Format

I’m planning for each paper to take up 2-3 days to present and discuss. One person will lead the presentation of the paper, and one person will lead discussion. I want about half of the time spent on presentation, and half on discussion. It’s fine if we have interactive presentations, so feel free to interrupt and ask questions during the presentations. I’ll keep us on track.

The goal of the presenter is to essentially guide the class through the reading. The presentation should be on the whiteboard, and you should not worry about polish. Part of the goal for this is to help you get confortable just talking about technical material without much prep (a skill you will need as a researcher). You may not understand everything in the paper, and that’s fine. If you don’t understand part of the paper, or have questions, feel free to say that and ask the class what they thought. This will help us all understand the reading better.

The goal of the person leading discussion is to ensure everyone is following and engaging critically in the presented material— ask and encourage others to ask questions, and try to question implicit assumptions in the technical work. For instance, if the discussion lead thinks a particular section is confusing but no one is asking questions, they should ask probing and clarifying questions. If the class accepts claims, contributions, or theorems at face value, the discussion lead ask if the English statements match technical results, or match the stated goals. When discussion and questions are flowing naturally, then the discussion lead has little to do but engage normally.

Project

The models and proofs need to be precise enough to communicate to the class, but no more precise. You cannot use any translation specifically shown in class to be both correct and incorrect. For inspiration, you can use bugs in open source compilers, translations from research papers (except those excluded above), or come up with your own.

The presentation must be a whiteboard presentation; don’t worry about polish. Expect interactivity.

By Mon, Mar 4, send me a proposal with and outline of what your expect your model to be, including a description of the source, target, and translation, and a brief English statement about which correctness property holds and which does not and why.