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
x86-TSO: A Rigorous and Usable Programmer's Model for x86 Multiprocessors
by Sewell et al.
Why are we reading this paper?
- Shared memory concurrency is an important area where specifications matter.
- Well-written, focused paper, exposing the field of memory models while giving one of the most concrete and well-motivated ones.
- Example of how specification clarifies thinking by focusing on the heart of the matter.
What to learn from this paper?
- Learn what a memory model is and why we need them.
- Understand what the x86-TSO model allows.
- Appreciate how this paper identifies what part of the architecture to focus on specifying.
Answer this question
The x86-TSO model described in the paper provides a memory model
for hardware threads (i.e., code running directly on physical CPUs).
Applications (user-level software) typically run on top of an OS kernel in
threads managed by the OS kernel ("kernel threads"), which are multiplexed
by the kernel across the available CPUs (and, in particular, the same
kernel thread might run on different hardware threads/CPUs over time).
To what extent does the x86-TSO memory model apply to applicaton software
running that uses kernel threads (if at all)?