Concurrency Models and Verifying Concurrent Code: Shared Memory, Actors, CSP and Model Checking
A concurrency model decides who owns the state and how parts communicate: with shared memory everyone takes turns through a lock, with actors and CSP the state has a single owner and communication is by message. We build Bookstore's stock reservation with a lock, an actor and a channel pipeline, show a read-then-write protocol selling 4,000 books from 1,000 in stock while the actor itself is bug-free, and model check the same check-then-act bug in TLA+ and read TLC's counterexample.
14 Nov 2026
·
13 min
·
14
