Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
This addresses a foundational issue in concurrency semantics for C/Pthread programs, offering a more accurate model for lock-based synchronization.
The paper tackles the problem that standard lock set constructions incorrectly assume critical sections are confined to a single thread, showing this is invalid for general C/Pthread executions. It provides a trace-based characterization that allows critical sections to span multiple threads, closing a semantic gap in existing models.
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. The commonly used notion of a critical section implicitly assumes that protected events belong to the same thread. We show that this assumption is not valid 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.