CS4910: Verified Compilers and Multi-Language Software (Fall 2019)

Motivation

“Can you trust your compiler?” — Xavier Leroy, developer of the Compcert verified C compiler

Software is written in a variety of languages, and in most cases, in order to run, it must be compiled down to some lower-level target. But what if that compiler isn’t correct? Compilers are some of the trickier pieces of software we build, and yet bugs in them are insidious: bugs in compilers mean that one of our most basic debugging strategies, reading source code, may not be helpful, since what actually ran may not correspond to that source code!

In the presence of buggy compilers, we must worry about what the compiler does and how our programs are translated to the target, possibly looking at compiler output or stepping through with low-level debuggers. Much better if the compiler were, essentially, invisible — if the source code fully specified what would happen. But a compiler can only truly be invisible if we can be sure that it does exactly what we expect: if we are sure it is correct. To be absolutely sure, we must prove it correct, and build a verified compiler.

Course structure

The course will be highly collaborative, and light on lectures. An average class will involve some time to collectively work on questions that are brought up (before or at the beginning of class), a brief introduction to a problem (usually a proof), time to work on the problem in small groups, one group presenting their solution with feedback, and a brief summary of highlights, or any points missed. Please bring your laptop to class every day. (If you do not have a laptop, we’ll figure something out, contact me: [email protected]).

Texts

We will draw reading from multiple texts, all available online for free. The abbreviations here are used in the syllabus (this list may be extended throughout the semester):

Schedule

Communication

We will use three methods:

1. in-person:
   • class: 11:45-1:25 M/Th
   • office hours XX:XX outside WVH 308 or scheduled with me
2. email:
   • contact me with questions ([email protected]), though technical questions are hard via email, so I may direct you to either come to office hours, or bring the question up (anonymized by default) at the beginning of class.
   • I will send messages to you via our course mailing list ([email protected]), which you should be on. If you are not enrolled in the class, but are participating (auditing, or something), please let me know and I’ll add you.
3. slack:
   • verifcomp19.slack.com: this is primarily a tool for you to communicate amongst yourselves. I may check it, but will not participate. As with other collaboration, feel free to use it for technical questions. As with the mailing list, I’ll sign everyone who is enrolled up, but other people can ask and I’ll get you on.

Grading

Grades will be assigned as follows:

Turning in assignments

All assignments should be committed to your private github repository (e.g., github.ccs.neu.edu/you/verifcomp) (see Github setup for notes about setup; we will go over this in the first class). When you are ready to submit the assignment, make a comment in the corresponding assignment issue in the shared repository (github.ccs.neu.edu/verifcomp/19) with just the user/repo@sha that corresponds to your submission (sha is the commit hash of the revision with your submission. If you do work afterwards, for example on the next assignment, that’s fine, don’t worry about pushing because I will grade that particular revision). Comments have timestamps, so you can be sure that you have “turned the assignment in” before the deadline provided the timestamp is before the deadline. I will review and give you your grades via github on your private repository (it’ll happen via a pull request, as that’s the only mechanism that allows easy commenting on entire files, regardless of how many commits you made).

Late policy

Assignments will have 10% deducted from the maximum total for every hour they are late, rounded up to the nearest hour. You will still get the same percentage of points, just against the smaller total. For example, if you got 80% of the points on an assignment, but you were 1hr late, you would get .8 * .9 = .72 of the points (not .8 - .1 = .7 total). However, you will be given 72 free late hours over the entire semester, which will be automatically optimally assigned (which means we will rank the hours late by how many points they lost you, and remove the top 72 of them). If you have an exceptional situation, please let me know – this policy is not set in stone, but is intended to balance progressing steadily through the course (and timely grading) with the inevitable minor things that come up.

Bonus points

Throughout the semester, there may be opportunities for earning bonus points. For any assignments that are turned in with Admitted lemmas, I will anonymize the assignment, remove anything that is unnecessary for the lemma, and add it to the bonus directory of the course repository. Each lemma will be given a point value – this is how many bonus points you will earn if you either prove the lemma or if you disprove it (i.e., if you can prove that assuming the lemma allows you to prove False). If you have proved (or disproved) a lemma, open a pull request with the proof filled in. You might want to communicate on slack before starting on something to be sure someone else isn’t working on a lemma. Note that there is no reason why you can’t solve lemmas that you Admitted yourself!

Collaboration policy

Collaboration on all aspects of the course (including assignments) is encouraged. However, if you do get help on an assignment, you must:

1. Disclose the help, in written form, as a comment in the assignment (e.g., had trouble with an induction hypothesis not helping, and Alex suggested generalizing before elim).
2. The overall solution must be yours. It is not collaboration if you go to someone for help before you have even started working on a problem, or to ask for help every 30 seconds. The assignments are individual for a reason: I want you to understand the overall structure on your own.

Auditing

If you would like to audit the course, you are welcome to. Just let me know and I’ll get you on the course mailing list, slack, etc. You will be able to participate fully in the course, with two caveats:

1. I may not be able to do as thorough grading on your assignments as on students who are enrolled for credit. I will do my best, though.
2. In class, especially if you are more experienced, I will expect you to give others a chance to speak up. Obviously, you should still contribute, but please be conscious of the space you take up. This applies, of course, to all members of the course, but I anticipate it may be more likely to occur with advanced student auditing the course.

Anticipated questions

1. What is class participation grading for?

   The course is, by design, collaborative. This means, it needs everyone to participate. That means presenting solutions to in-class problems, contributing thoughts to questions that are brought up, sending in places you got stuck for us to work on in class, etc.

2. If I miss a class, can I still get a full class participation grade?

   Missing a single class (or even two) won’t hurt your grade, provided you are participating the rest of the time. The grade is not about attendance. And indeed, if you attend every class but never speak, you will get a 0 (attending is not the same as participating).

3. Why are the early assignments worth so much less?

   These assignments are about learning Coq, and a lot of the exercises are (unfortunately) easy to google for solutions to. Doing so will only hurt you (in addition to obviously being an academic code violation), as you won’t actually learn how to use Coq, but in an attempt to disincentivize doing so, I’m making the assignments not count that much towards your grade.

4. How will assignments be graded? What if I can’t figure a proof out? Will I get a zero?

   Partial credit and partial proofs are completely accepted, and expected. The magnitude of what is Admitted, will determine, of course, the extent of the partial credit, but certainly don’t think that just because you aren’t able to get everything to go through that you will get no credit. Also, as noted above, anything you admit you can potentially solve later for bonus points (but so, of course, can your classmates).

5. Will there be a final exam?

   There will be no final exam. There will be no in-class exams, at all.

Other question? Something not clear?

Please reach out to the instructor: Daniel Patterson ([email protected])