Lecture preparation
Before lecture, read the paper assigned below, and submit two items
to the
submission website:
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
beforehand.
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Assignment
Read the blog post
A brief introduction to Iris
by Tej Chajed.
Why are we reading this blog post?
-
Iris demonstrates how to extend the ideas of separation logic to reasoning
about concurrent software.
-
We want students to see Iris (since we believe in it), but any paper is
intimidating and doesn't get the ideas across.
-
The blog post aims to be a readable and concrete introduction to ghost variables.
What to learn from this blog post?
- Be able to sketch out the basic intuition behind the proof.
- Understand what the IPM contexts mean, in terms of separation logic.
Answer this question
Describe how you would change the proof to handle multiple accounts. No need
for precise mathematical syntax, but do describe in words the new ghost state,
new invariant that holds at all intermediate steps, and new lock invariants.
