arxiv: 2603.13142 · v4 · submitted 2026-03-13 · 💻 cs.PL · cs.LO

Recognition: no theorem link

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

Martin Sulzmann

Authors on Pith no claims yet

Pith reviewed 2026-05-15 11:12 UTC · model grok-4.3

classification 💻 cs.PL cs.LO

keywords critical sectionstrace semanticslock-based concurrencyC/Pthreadsmulti-thread critical sectionssynchronization analysisdata race detection

0 comments

The pith

Critical sections in C/Pthread programs are not confined to single threads but can span multiple threads under a trace semantics.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that the usual assumption in lock-based concurrency analysis—that critical sections protected by locks stay inside one thread—fails for general C and Pthread executions. It builds a trace model that defines critical sections directly from observable lock operations and interleavings, without forcing events to belong to the same thread. This yields multi-thread critical sections that appear in actual programs. The change closes the semantic gap in how standard lock-set constructions identify protected regions. Readers should care because existing race detectors and synchronization tools rely on the old restriction and may therefore miss real protection patterns.

Core claim

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 multi-thread critical sections arise naturally in real programs and close a semantic gap in the standard lock set construction.

What carries the argument

Trace model of C/Pthread programs that characterizes critical sections from lock-acquire and lock-release events without requiring all events to belong to one thread.

If this is right

Lock-set constructions for data-race detection must now consider synchronization that crosses thread boundaries.
Standard per-thread critical-section definitions miss protection patterns that occur in ordinary C/Pthread code.
Concurrency analyses gain precision by treating multi-thread critical sections as first-class protected regions.
The semantic gap between lock usage in real programs and existing formal definitions is removed.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Static analyzers for other lock-based languages could adopt similar cross-thread characterizations to reduce false negatives.
Dynamic race detectors might improve coverage by replaying traces against the new multi-thread definition.
Verification tools for shared-memory concurrency may need revised notions of atomicity that permit protected events in different threads.

Load-bearing premise

The trace model accurately captures the observable behavior of real C/Pthread programs with respect to lock operations and thread interleaving.

What would settle it

A concrete C/Pthread execution trace containing a sequence of lock operations that the new characterization treats as a multi-thread critical section, yet the protected events are observed to race or violate atomicity in actual hardware runs.

Figures

Figures reproduced from arXiv: 2603.13142 by Martin Sulzmann.

**Figure 1.** Figure 1: C/Pthread program. traces of C/Pthread programs. Therefore, the standard lock set construction that computes the set of locks that are held (acquired) but not yet released at a certain point in the execution is incomplete as well. Contributions. The contributions of this paper are primarily conceptual: • We identify an implicit per-thread assumption in the standard definition of critical sections and lock … view at source ↗

**Figure 2.** Figure 2: Trace T1 resulting from execution of the program in [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

**Figure 1.** Figure 1: We assume that the main thread always has thread id [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗

read the original 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. 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper shows critical sections in C/Pthread executions can span threads and gives a trace semantics that drops the usual per-thread restriction.

read the letter

The core point is that the standard lock-set construction assumes critical sections stay inside one thread, but this does not match general C/Pthread programs where protected events can cross threads. The authors build a trace model that records lock acquire and release events without forcing intra-thread confinement, then characterize critical sections directly from those traces. This produces multi-thread critical sections as a natural outcome rather than an exception. The work identifies a concrete semantic gap in how synchronization is modeled for race detection and verification tools. It is useful because many existing analyses inherit the per-thread assumption from older lock-set papers, and relaxing it could reduce false positives or missed races in real code. The trace approach itself looks clean on the surface: it stays close to observable lock operations and interleavings without introducing new primitives. That keeps the model lightweight and potentially easier to integrate into existing analyzers. The main limitation is that the abstract gives no concrete traces, no worked examples of multi-thread sections, and no proof sketches. Without those, it is hard to judge whether the characterization covers all interleaving cases or whether it matches actual pthread behavior on edge cases like nested locks or signal handling. The claim that the model captures the essence of C/Pthread programs therefore rests on the full development, which is not visible here. Readers working on concurrency semantics, static analysis for systems code, or tool builders who rely on lock-set information would find this relevant. It is not a broad foundational result but a targeted correction to an implicit modeling choice. I would send it to peer review; the idea is clear enough and the gap it targets is real, so referees can check the details and examples.

Referee Report

0 major / 1 minor

Summary. The paper claims that the standard assumption in lock-set constructions—that critical sections are confined to a single thread—does not hold for general C/Pthread executions. Using a trace model capturing C/Pthread programs, it provides a trace-based characterization of critical sections without per-thread restriction, allowing them to span multiple threads, which occur naturally in real programs.

Significance. If the trace model is faithful, the result is significant for concurrency semantics and static analysis: it closes a modeling gap in lock-set constructions and supplies a more general foundation for reasoning about synchronization that can span threads. The formal trace characterization is a clear strength that could improve precision in race detection and related tools.

minor comments (1)

[Abstract] Abstract: a brief illustrative example of a multi-thread critical section (e.g., a short code fragment with lock operations across threads) would make the central claim more concrete and easier to follow.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment, accurate summary of our contribution, and recommendation for minor revision. The report correctly identifies the core claim: that standard lock-set constructions rest on an implicit per-thread restriction on critical sections that does not hold in general C/Pthread executions, and that our trace model supplies a faithful characterization without that restriction. No major comments appear in the report.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper introduces a trace model for C/Pthread lock operations and directly defines a trace-based characterization of critical sections from that model, without imposing per-thread restrictions. No equations, fitted parameters, or predictions are present that reduce by construction to inputs. No load-bearing self-citations, uniqueness theorems, or ansatzes imported from prior work are referenced in the derivation chain. The central claim—that critical sections may span multiple threads—follows immediately from the model definition itself, which is presented as an independent semantic capture of observable behavior. This is a standard, self-contained definitional construction with no internal reduction to prior fitted quantities or self-referential premises.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

The central claim rests on the assumption that the trace model faithfully represents C/Pthread lock behavior; no free parameters, axioms, or invented entities are explicitly introduced in the abstract.

pith-pipeline@v0.9.0 · 5407 in / 952 out tokens · 48127 ms · 2026-05-15T11:12:43.816040+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages · 1 internal anchor

[1]

Dynamic deadlock analysis of multi-threaded programs

[BH05] Saddek Bensalem and Klaus Havelund. Dynamic deadlock analysis of multi-threaded programs. In Shmuel Ur, Eyal Bin, and Yaron Wolfsthal, editors,Hardware and Software Verification and Testing, First International Haifa Verification Conference, Haifa, Israel, November 13-16, 2005, Revised Selected Papers, volume 3875 ofLecture Notes in Computer Scienc...

work page doi:10.1007/11678779 2005
[2]

[CMP20] Yan Cai, Ruijie Meng, and Jens Palsberg

doi:10.1109/TSE.2014.2301725. [CMP20] Yan Cai, Ruijie Meng, and Jens Palsberg. Low-overhead deadlock prediction. InProceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE ’20, page 1298–1309, New York, NY, USA,

work page doi:10.1109/tse.2014.2301725 2014
[3]

doi:10.1145/ 3377811.3380367

Association for Computing Machinery. doi:10.1145/ 3377811.3380367. [CYSZ22] Yuandao Cai, Chengfeng Ye, Qingkai Shi, and Charles Zhang. Peahen: fast and precise static deadlock detection via context reduction. InProceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022...

work page arXiv 2022
[4]

doi:10.1145/3540250.3549110

Association for Computing Machinery. doi:10.1145/3540250.3549110. [CYW+21] Yan Cai, Hao Yun, Jinqiu Wang, Lei Qiao, and Jens Palsberg. Sound and efficient concurrency bug prediction. In Diomidis Spinellis, Georgios Gousios, Marsha Chechik, and Massimiliano Di Penta, editors,ESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposiu...

work page doi:10.1145/3540250.3549110 2021
[5]

[Har00] Jerry J

doi: 10.1145/3360605. [Har00] Jerry J. Harrow. Runtime checking of multithreaded applications with visual threads. In Klaus Havelund, John Penix, and Willem Visser, editors,SPIN Model Checking and Software Verifi- cation, 7th International SPIN Workshop, Stanford, CA, USA, August 30 - September 1, 2000, Proceedings, volume 1885 ofLecture Notes in Computer...

work page doi:10.1145/3360605 2000
[6]

[Hav00] Klaus Havelund

doi:10.1007/10722468_20. [Hav00] Klaus Havelund. Using runtime analysis to guide model checking of Java programs. InProceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, page 245–264, Berlin, Heidelberg,

work page doi:10.1007/10722468_20
[7]

[JPSN09] Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik

Springer-Verlag. [JPSN09] Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. A randomized dynamic program analysis technique for detecting real deadlocks. In Michael Hind and Amer Diwan, editors, Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009, pages 11...

work page 2009
[8]

[KMV17] Dileep Kini, Umang Mathur, and Mahesh Viswanathan

doi:10.1145/1542476.1542489. [KMV17] Dileep Kini, Umang Mathur, and Mahesh Viswanathan. Dynamic race prediction in linear time. CoRR, abs/1704.02432,

work page doi:10.1145/1542476.1542489
[9]

Dynamic Race Prediction in Linear Time

URL:http://arxiv.org/abs/1704.02432,arXiv:1704.02432. [KP18] Christian Gram Kalhauge and Jens Palsberg. Sound deadlock prediction.Proc. ACM Program. Lang., 2(OOPSLA):146:1–146:29, 2018.doi:10.1145/3276516. [KPSW16] Daniel Kroening, Daniel Poetzl, Peter Schrammel, and Bj¨ orn Wachter. Sound static deadlock analysis for c/pthreads. InProceedings of the 31st...

work page internal anchor Pith review Pith/arXiv arXiv doi:10.1145/3276516 2018
[10]

CRITICAL SECTIONS ARE NOT PER-THREAD 11 [NPSG09] Mayur Naik, Chang-Seo Park, Koushik Sen, and David Gay

Association for Computing Machinery.doi:10.1145/2970276.2970309. CRITICAL SECTIONS ARE NOT PER-THREAD 11 [NPSG09] Mayur Naik, Chang-Seo Park, Koushik Sen, and David Gay. Effective static deadlock detection. InProceedings of the 31st International Conference on Software Engineering, ICSE ’09, page 386–396, USA,

work page doi:10.1145/2970276.2970309
[11]

[RGB18] Jake Roemer, Kaan Gen¸ c, and Michael D

IEEE Computer Society.doi:10.1109/ICSE.2009.5070538. [RGB18] Jake Roemer, Kaan Gen¸ c, and Michael D. Bond. High-coverage, unbounded sound predictive race detection.SIGPLAN Not., 53(4):374–389, June 2018.doi:10.1145/3192366.3192385. [SBN+97] Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race d...

work page doi:10.1109/icse.2009.5070538 2009
[12]

[Sha08] Vivek K

doi:10.1145/2103656.2103702. [Sha08] Vivek K. Shanbhag. Deadlock-detection in java-library using static-analysis. InProceedings of the 2008 15th Asia-Pacific Software Engineering Conference, APSEC ’08, page 361–368, USA,

work page doi:10.1145/2103656.2103702 2008
[13]

[SI09] Konstantin Serebryany and Timur Iskhodzhanov

IEEE Computer Society.doi:10.1109/APSEC.2008.68. [SI09] Konstantin Serebryany and Timur Iskhodzhanov. ThreadSanitizer: Data race detection in practice. InProc. of WBIA ’09, pages 62–71, New York, NY, USA,

work page doi:10.1109/apsec.2008.68 2008
[14]

doi:10.1145/1791194

ACM. doi:10.1145/1791194. 1791203. [SR14] Malavika Samak and Murali Krishna Ramanathan. Trace driven dynamic deadlock detection and reproduction. In Jos´ e E. Moreira and James R. Larus, editors,ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’14, Orlando, FL, USA, February 15-19, 2014, pages 29–42. ACM, 2014.doi:10.1145/25...

work page doi:10.1145/1791194 2014
[15]

[YB16] Misun Yu and Doo-Hwan Bae

doi:10.1109/CGO.2011.5764688. [YB16] Misun Yu and Doo-Hwan Bae. Simplelock+: fast and accurate hybrid data race detection.The Computer Journal, 59(6):793–809, 2016.doi:10.1109/PDCAT.2013.15. [ZSL+17] Jinpeng Zhou, Sam Silvestro, Hongyu Liu, Yan Cai, and Tongping Liu. UNDEAD: Detecting and preventing deadlocks in production software. In Grigore Rosu, Massi...

work page doi:10.1109/cgo.2011.5764688 2011