Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency

Locks are a standard mechanism for synchronizing concurrent threads. The standard lock set construction assumes that critical sections are confined to a single thread, and therefore only accounts for locks acquired within that thread. Traditional definitions of critical sections implicitly assume that protected events belong to the same thread. We demonstrate that this assumption does not hold for general C/Pthread executions. Using a trace model that captures the essence of C/Pthread programs, we give a trace-based characterization of critical sections that does not impose a per-thread restriction. As a result, critical sections may span multiple threads. Such \emph{multi-thread} critical sections arise naturally in real programs and close a semantic gap in the standard lock set construction.