Operating systems: explain an interleaving before choosing a lock
Concurrency reasoning begins with the events an execution permits. This route separates an operating-system abstraction, the kernel mechanism implementing it and the language-level rules of a real program. A trace can refute a claim about all executions, while a synchronization argument must explain which traces it excludes.
Course topic: Operating Systems
Study route and exercise: University Reading List editorial project. How we curate · Sources checked:
On this page
Scope and responsibility
For systems learners who know C, pointers, stacks and basic computer organization. The original worksheet uses a fully stipulated sequentially consistent abstract machine. It is not a prediction for an unsynchronized C data race, which cannot be analyzed by silently assuming these rules.
Choose your starting point
I need a free conceptual spine
Use OSTEP’s virtualization, concurrency and persistence sequence. Begin with the question each mechanism solves, then relate its implementation to an invariant.
I want to see the mechanism in a kernel
Use the pinned xv 6 RISC-V revision 5 after C and architecture preparation. Match the booklet to the source revision before following code references.
My course needs a broad reference
Use Operating System Concepts for a wider topic map and practice questions. Select the assigned synchronization and process discussions rather than reading every platform case study at once.
Compare the three books
Operating Systems: Three Easy Pieces
Remzi H. Arpaci-Dusseau and Andrea C. Arpaci-Dusseau · Edition: 1.00 · 2018
Free concepts-and-experiments spine
- Choose it when
- You can trace C pointers and want a mechanism explained through a concrete systems problem.
- Use another route when
- You need a first programming course or expect the online chapters to be page-identical to a selected print copy.
- Selected reading
- OSTEP: Concurrency: An Introduction, Locks and condition-variable discussions, with process/address-space review first if needed.
- Limits and trade-offs
- The selected 2018 record is version 1.00; the author-hosted chapters are now 1.10. Free chapter PDFs and a paid combined convenience PDF are distinct products.
Try before choosing
Translate a shared-variable update into load, private calculation and store events, then list allowed orders.
Check your work: Identify what is atomic in the model before saying that a high-level statement is atomic.
xv6: a simple, Unix-like teaching operating system
Russ Cox; Frans Kaashoek; Robert Morris · Edition: RISC-V revision 5 · 2025
Free teaching-kernel companion
- Choose it when
- You want to connect processes, traps, memory and locking to a compact implementation.
- Use another route when
- You still need C/assembly basics or want the teaching kernel to represent every production-kernel tradeoff.
- Selected reading
- RISC-V revision 5, dated 2 September 2025: interfaces and organization, then the named locking and scheduling chapters alongside matching source.
- Limits and trade-offs
- Its small design makes code paths inspectable but omits much production complexity. Do not mix x 86 commentary, a current repository and old line references as one version.
Try before choosing
Choose one lock-protected kernel invariant and identify the state and code paths that can modify it.
Check your work: A lock name is insufficient: explain which invariant requires the same lock across all relevant paths.
Operating System Concepts
Abraham Silberschatz; Peter Baer Galvin; Greg Gagne · Edition: 10 · 2018
Broad commercial reference
- Choose it when
- You need the standard process, synchronization, memory and storage vocabulary for a syllabus.
- Use another route when
- You expect companion slides or selected practice solutions to be free access to the whole text or every instructor answer.
- Selected reading
- Tenth edition, 2018: named process/thread and synchronization discussions, with memory-management sections selected as the course requires.
- Limits and trade-offs
- The selected ISBN 9781119320913 is Wiley’s electronic product. Other tenth-edition bundles and print companions have different identifiers; match the assigned object.
Try before choosing
Compare mutual exclusion, ordering and progress as three different requirements for the worksheet.
Check your work: A mutex can exclude overlapping updates without specifying which update happens first or guaranteeing a scheduling policy.
Check your preparation
What is an interleaving?
An order of individually permitted events that preserves each thread’s own required order. A shared result must be calculated from the values actually read in that order.
What is the protected region?
The whole read-modify-write operation when the invariant depends on their combination. Locking a load and a store separately does not make the pair one indivisible update.
What does a model leave out?
Here all loads/stores are atomic and globally ordered; computation is private. Real language memory rules, compiler transformations, failures and fairness are not supplied by this abstract packet.
A six-step study plan
Steps completed: 0 / 6
These are your own study marks, not an assessment. They are not sent to this site.
-
Specify the machine
Selected reading: OSTEP concurrency introduction.
What to do: Write the shared state, private registers, atomic events and each thread’s event order.
Check your work: Do not smuggle in a programming language’s behavior without stating it.
-
Trace one execution
Selected reading: The same introduction and the main worksheet.
What to do: Record the value returned by each load and the value written by each store.
Check your work: A later store uses its own saved load, not necessarily the latest shared value.
-
Cover all orders
Selected reading: Selected synchronization reading.
What to do: List all six orders preserving two load-before-store constraints.
Check your work: Give a reason the list is complete, not just several interesting examples.
-
State the invariant
Selected reading: xv 6 locking and the relevant reference discussion.
What to do: Write what one whole update must observe and publish as a unit.
Check your work: The invariant determines the protected region, not the visual length of a source line.
-
Change synchronization
Selected reading: The solved follow-up.
What to do: Recompute results when one mutex protects both complete updates; then add an explicit order.
Check your work: Mutual exclusion and deterministic order are different conclusions.
-
Connect to a real implementation
Selected reading: One matching xv 6 locking path or a course exercise.
What to do: Explain which language and kernel mechanisms establish the assumed ordering.
Check your work: A correct abstract trace does not certify an unexamined production program.
Worked exercise
Original event machine: an atomic load is not an atomic update
Shared x starts at 10. Thread 1 loads x into private r1, then stores r1+3. Thread 2 loads x into private r2, then stores 2r2. Call their events R1, W1, R2, W2. List every order with R1 before W1 and R2 before W2, and find all final values.
Assumptions
Each load/store is indivisible; all four events have one sequentially consistent order; each load sees the latest preceding store or initial 10. Private arithmetic adds no shared event. Both threads finish, with no other access. This is an invented abstract machine, not unsynchronized C code.
- R1, W1, R2, W2: r1=10, W1=13, r2=13, W2=26. R2, W2, R1, W1: r2=10, W2=20, r1=20, W1=23.
- R1, R2, W1, W2 and R2, R1, W1, W2 both load 10 twice and finish with W2=20. R1, R2, W2, W1 and R2, R1, W2, W1 both load 10 twice and finish with W1=13.
- There are choose(4,2)=6 ways to place Thread 1’s ordered events among four slots; the other slots hold Thread 2’s events. The six cases above are complete.
- Final values are therefore {13,20,23,26}. The two serial orders produce 26 and 23; the other results lose an update because a saved earlier load is later written over the other thread’s result.
Answer and interpretation
All six legal interleavings yield exactly four possible final values: 13,20,23,26. Individual atomic events do not make the compound updates atomic.
Test the result
Keep a four-row state ledger for each order. Do not apply this finite result set to a language execution whose memory/data-race semantics differ from the packet.
Change an assumption
Changed synchronization: exclusion still leaves an order choice
Replace only the synchronization: one common mutex protects each entire load-and-store update, and both complete. What results remain? Then additionally stipulate a handoff requiring Thread 1’s complete update before Thread 2’s.
- The protected regions cannot overlap. If Thread 1 runs first, x goes 10→13→26; if Thread 2 runs first, it goes 10→20→23.
- Mutual exclusion removes final 13 and 20, but retains 23 and 26 because addition and doubling do not commute. No stated mutex rule selects an order.
- With the additional Thread 1-before-Thread 2 handoff, only 10→13→26 remains. That ordering requirement is extra; it is not inferred from merely using the same mutex.
Answer and interpretation
Mutex alone: {23,26}; mutex plus the specified handoff: {26}. Atomicity and deterministic ordering answer different questions.
Test the result
Compose the two update functions in both orders. Fairness, absence of deadlock and actual language correctness would require their own implementation argument.
Common mistakes
Atomic statement assumed
A source-level update can contain several observable memory events.
One lock label treated as proof
The same relevant lock must cover the whole state transition on every access path.
Exclusion confused with order
Two serialized noncommuting operations can still have two valid outcomes.
Before moving on
- I can enumerate the legal event orders and reproduce every loaded/stored value.
- I can explain precisely which results synchronization removes.
- I can distinguish the abstract machine from a real language and kernel implementation.
Sources and edition checks
Sources checked:
- OSTEP: free conceptual chapters and current online version
The three-piece organization supplies the conceptual spine and free chapter route.
- OSTEP: publication and revision history
Version 1.00 and the evolving 1.10 online chapters are distinct reading objects.
- OSTEP: concurrency introduction
The concurrency introduction supports event-level reasoning; all worksheet values and traces are original.
- MIT: xv 6 RISC-V revision 5, September 2025
The pinned 2025 RISC-V booklet supplies the inspectable kernel companion.
- Wiley: tenth-edition electronic product identity
The exact tenth-edition product and its companion materials are distinguished from other formats.
These are proposed study activities, not official course assignments or a claim that every book has been read cover to cover.