Lecture preparation

Before lecture, read the paper assigned below, and submit two items to the submission website:

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?

What to learn from this blog post?

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.