Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Warning
Why is Concurrent Programming so Hard?
Time
Events
Threads
Example Thread Events
Threads are State Machines
States
Concurrency
Concurrency
Interleavings
Intervals
Intervals may Overlap
Intervals may be Disjoint
Precedence
Precedence
Precedence Ordering
Precedence Ordering
Partial Orders(review)
Total Orders(review)
Repeated Events
Implementing a Counter
Locks (Mutual Exclusion)
Locks (Mutual Exclusion)
Locks (Mutual Exclusion)
Using Locks
Using Locks
Using Locks
Using Locks
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Deadlock-Free
Starvation-Free
Two-Thread vs n-Thread Solutions
Two-Thread Conventions
Two-Thread Conventions
LockOne
LockOne
LockOne
LockOne
LockOne Satisfies Mutual Exclusion
From the Code
From the Assumption
Combining
Combining
Combining
Combining
Combining
Combining
Cycle!
Deadlock Freedom
LockTwo
LockTwo
LockTwo
LockTwo
LockTwo Claims
Peterson’s Algorithm
Peterson’s Algorithm
Peterson’s Algorithm
Peterson’s Algorithm
Peterson’s Algorithm
Mutual Exclusion
Also from the Code
Assumption
Combining Observations
Combining Observations
Combining Observations
Deadlock Free
Starvation Free
The Filter Algorithm for n Threads
Filter
Filter
Filter
Filter
Filter
Filter
Filter
Claim
Induction Hypothesis
Proof Structure
Just Like Peterson
From the Code
By Assumption
Combining Observations
Combining Observations
Combining Observations
No Starvation
Bounded Waiting
Bounded Waiting
First-Come-First-Served
Fairness Again
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
Bakery Algorithm
No Deadlock
First-Come-First-Served
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Mutual Exclusion
Bakery Y232K Bug
Bakery Y232K Bug
Does Overflow Actually Matter?
Timestamps
The Good News
The Good News
Instead …
Precedence Graphs
Unbounded Counter Precedence Graph
Unbounded Counter Precedence Graph
Unbounded Counter Precedence Graph
Two-Thread Bounded Precedence Graph
Two-Thread Bounded Precedence Graph
Two-Thread Bounded Precedence Graph
Two-Thread Bounded Precedence Graph
Two-Thread Bounded Precedence Graph T2
Three-Thread Bounded Precedence Graph?
Three-Thread Bounded Precedence Graph?
Graph Composition
Three-Thread Bounded Precedence Graph T3
Three-Thread Bounded Precedence Graph T3
Three-Thread Bounded Precedence Graph T3
In General
Deep Philosophical Question
Shared Memory
Theorem
Proving Algorithmic Impossibility
Proof: Need N-MRSW Registers
Upper Bound
Bad News Theorem
Theorem (For 2 Threads)
Two Thread Execution
Covering State for One Register Always Exists
Proof: Assume Cover of 1
Proof: Assume Cover of 1
Theorem
Proof: Assume Cover of 2
Run A Solo
Obliterate Traces of A
Mutual Exclusion Fails
Proof Strategy
Covering State for Two
Covering State for Two
Covering State for Two
Covering State for Two
Inductively We Can Show
Summary of Lecture
Summary of Lecture