The intersection
Cars arrive on two perpendicular roads, A and B. The intersection is a shared resource. The safety invariant is simple: only one road can have the green light at a time, so crossing traffic never collides.
Modelling the lock
The green light is essentially a mutex over the intersection. A car crosses only while its road is green. When a car arrives on a road whose light is red, the controller may need to switch the light, which means waiting for the current road to clear.
Switching safely
A correct controller protects the shared light state under a lock:
- Check which road currently has green.
- If the arriving car is on the green road, it crosses.
- Otherwise flip the light to that road, but only after the previous direction has no car mid crossing.
Fairness
If road A is busy it can hold green forever and starve road B. A timer or alternating policy that flips the light after a bounded interval gives both roads a turn, trading throughput for fairness, much like a fair lock.
Key idea
The traffic light controller is a mutex over a shared intersection where only one road is green, and a timed switch keeps either road from starving.