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 paper
Separation Logic
by Peter O'Hearn.
Why are we reading this paper?
-
Separation logic is perhaps the most important advance in program
verification of the last few decades, for the large class of programs
that have either pointer manipulation or shared-memory concurrency.
-
The paper is extremely well written and covers several
applications of separation logic.
What to learn from this paper?
-
How does separation logic work to make reasoning about pointers more tractable and "local"?
-
Learn to read proof outlines and separation logic assertions.
-
Appreciate how the same techniques scale to more sophisticated separation, including concurrency and automated verification.
Answer this question
Suppose we made the tree (described on p91, middle column) share nodes whenever
an inserted tree matched one already present, saving memory by storing a pointer
to the existing tree. With such an implementation what does tree(tau_1, root_1) *
tree(tau_2, root_2) mean? Does modifying root_1 affect just tau_1 (as before),
or also tau_2?
