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 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?