Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
2026-03-13 • Programming Languages
Programming Languages
AI summaryⓘ
The authors explain that the usual way of understanding locks in multi-threaded programs assumes that the protected parts of the code (critical sections) happen within a single thread. They show this assumption is not always true for C/Pthread programs and introduce a new way to think about critical sections that can include multiple threads. This helps better represent how real programs work and fixes a limitation in existing lock analysis methods.
lockscritical sectionsthreadsconcurrencyC/Pthreadsynchronizationtrace modellock set constructionmulti-threading
Authors
Martin Sulzmann
Abstract
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.