The Shared Section

A critical section is a region of code protected by a lock. Thread A acquires the lock, executes the protected code, releases the lock. While A holds the lock, no other thread can enter. The protection guarantees mutual exclusion: only one thread at a time. The concept is foundational — taught in every operating systems course, implemented in every concurrent program, assumed in every correctness proof.

The paper (arXiv:2603.13142, March 2026) shows that critical sections can span multiple threads. The region of code protected by a lock is not confined to the thread that acquired it.

The mechanism is lock transfer. Thread A acquires the lock, does some work, then hands the lock to thread B through a shared data structure — without releasing it. Thread B continues executing within the same critical section that A started. The lock was never released, so mutual exclusion is maintained (no third thread can enter). But the “single thread in the critical section” assumption is violated. Two threads, sequentially, execute inside the same lock-hold.

This matters for formal verification. Program analyses that assume critical sections are per-thread — that the thread acquiring the lock is the thread executing all protected operations — will miss the cross-thread dataflow. Race detectors, deadlock analyzers, and concurrent program verifiers all encode this assumption. When the assumption fails, the analysis is unsound.

The paper provides a trace semantics that correctly handles cross-thread critical sections. The semantics tracks lock ownership as a first-class concept separate from thread identity, allowing the formal framework to represent what actually happens rather than what was assumed.

The structural lesson: a synchronization primitive (the lock) and the programming pattern it was designed for (per-thread mutual exclusion) are not the same thing. The primitive enforces mutual exclusion. The per-thread assumption is a social convention layered on top. When programs violate the convention while respecting the primitive, they are correct but invisible to analyses that encoded the convention as invariant.