Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency (opens in new tab)

arXiv:2603.13142v1 Announce Type: new 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 ...