Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913008986357760 |
|---|---|
| author | Sulzmann, Martin |
| author_facet | Sulzmann, Martin |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_13142 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency Sulzmann, Martin Programming Languages Logic in Computer Science 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. |
| title | Critical Sections Are Not Per-Thread: A Trace Semantics for Lock-Based Concurrency |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2603.13142 |