Lecture preparation

Assignment

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