Blog
Mert Özen's blog posts on software development, backend, frontend, and DevOps.
Concurrency vs Parallelism: Interleaving, Nondeterminism and Amdahl's Law
Concurrency is jobs overlapping in time, parallelism is jobs running at the same moment, and the serial part sets the speedup ceiling: with 10% serial work, 64 cores give at most 8.8 times. We show that an increment is lost in 18 of the 20 possible orders of two threads, that 99.6% of real runs follow a single order, and that the Bookstore report job falls short of Amdahl with 10 workers on ARM64.
Race Conditions vs Data Races: Check-Then-Act, Read-Modify-Write and Atomicity
A data race is concurrent, unsynchronized memory access where at least one access writes; a race condition is a result that depends on timing, and one can exist without the other. With real threads we show count++ losing 82% of increments, a stock check written with ConcurrentDictionary overselling in 1403 of two thousand rounds, and a 32-byte price struct read half old, half new on ARM64.
Mutual Exclusion Theory: Critical Sections, Peterson's Algorithm, Semaphores and Monitors
A correct critical section solution must provide mutual exclusion, progress and bounded waiting together; Peterson's algorithm does this with only reads and writes but assumes sequential consistency. We show Peterson written with volatile breaking 99 times in 40 million entries on ARM64 and fixed by a full fence, waiting with if producing 54,234 errors in a shipping queue, and where test-and-set, semaphores and monitors come from.
Deadlock, Livelock and Starvation: Coffman Conditions, Lock Ordering and Priority Inversion
Deadlock can only occur when mutual exclusion, hold and wait, no preemption and circular wait hold together; in practice circular wait is the easiest to break, by taking locks in a global order. We fix a stock transfer that really deadlocks between two Bookstore warehouses with Id ordering in 25 ms, measure a 1 ms timeout turning into a livelock with 621,187 timeouts in 5 seconds, and look at the Mars Pathfinder priority inversion case.
Hardware Memory Models: Reordering, Store Buffers, Cache Coherence and Sequential Consistency
Modern CPUs do not give sequential consistency: the store buffer lets a read overtake an earlier write, and ARM64 reorders even more. On ARM64 we measure both threads reading 0 in 5.3 million of 10 million rounds of the classic store buffering test and a flag becoming visible before the data in the message passing test, explain why cache coherence does not prevent this, and show from Intel's manual which outcomes x64 forbids.
The .NET Memory Model: Happens-Before, Acquire/Release, volatile and Safe Object Publication
In the .NET memory model ordinary accesses may be reordered; Volatile.Read is an acquire, Volatile.Write a release, and Interlocked and lock are the points that guarantee order. We show a non-volatile stop flag loop never stopping in a Release build because of the JIT, double-checked locking with a bool flag returning null 36 times in 20 million calls on ARM64, derive from the spec why checking the reference is correct, and compare with Java, C++ and Go.
Lock-Free and Wait-Free: CAS Loops, the ABA Problem and Linearizability
A lock-free algorithm guarantees that at least one thread makes progress even under contention, a wait-free one that every thread does. We write a counter and a Treiber stack with CAS loops, and measure on ARM64 that pooling nodes brings back the ABA problem and loses hundreds of thousands of 8 million ids, that a small checker finds non-linearizable histories in a broken stack, and that the CAS loop is 16 times slower than a lock on 8 threads.
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.