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.

Days

  

Time

  

Room

Mon. Wed. Fri.

  

15:00--16:00

  

ICCS 246

               

Instructor:

  

William J. Bowman

Office:

  

ICICS 389

Email:

  

wilbowma

Office Hours:

  

By appointment; check my calendar and email me.

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.

My goals with this course are:
  • Introduce students to reasoning about programs and program transformations.

  • Introduce students to space of compiler correctness.

  • Convince students to think about compilers in terms of judgments preserved.

References

For additional reading, I recommend the following freely available books

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.

To help you think about how to read, present, and critiques the papers, here are some things to ask yourself:
  • What motivation or background is missing?

  • Can you translate the papers’ formalisms into foramlism you already understand, such as the formalisms we used in class?

  • Can you implement this formalism?

  • Can you fill in missing definitions, lemmas, proofs, or proof cases?

  • Does this formalism match the English description, motivating problem, or conclusions?

  • How could you break this work, or break a more realistic variant of it?

  • How could you prove this work correct, or prove an even stronger result?

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

You should model a compiler, thus a source and target language with a translation from source to target, and show the translation is both "correct" and "incorrect". That is, show that the translation satisfies one of the correctness properties we discussed, but fails to satisfy another. For example, your translation might be:
  • Non-trivially type persevering but incorrect

  • Correct but insecure

  • Correct but not compositionally correct

  • Fully abstract but not correct

As a reminder, the compiler correctness theorems we covered are:
  1. Type Preservation

  2. Whole Program Correctness

  3. Correctness of Separate Compilation

  4. Compositional Correctness

  5. Full Abstraction

In detail, for your project you should:
  • Create a model of the source and target languages
    • Include the evaluation function, and linking. You may optionally include a type system.

  • Create a model of a compiler

  • Prove (the key cases) of one correctness property. You only be as precise as the papers we read in class. Which is to say, include definitions and key lemmas, but only include the key cases of the proof.

  • State another correctness property, but provide a counterexample

  • Write up the model on paper and submit it to me before Wed, Apr 3.

  • Prepare a 50 minute in-class presentation, with time for discussion

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.