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
- 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.
Read the paper
Armada: Low-Effort Verification of High-Performance Concurrent Programs
by Lorch et al.
You can also watch the video of the conference presentation of this
paper at PLDI 2020, here
Why are we reading this paper?
- Several ideas explained here: movers, refinement, stacked verification, having a sound extensibility story.
- Handles all the concerns down to C and TSO.
What to learn from this paper?
- What is the trust story in Armada?
- How do the strategies work together?
- What does it mean that Armada is extensible?
- What are the modularity limits of having levels?
Answer this question
What non-deterministic choices of a program's execution does Armada
encode in the "step object", shown in the paper as σi?