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

TL;DR

This paper introduces a trace semantics for lock-based concurrency that allows critical sections to span multiple threads, addressing limitations of traditional per-thread assumptions.

Contribution

It presents a novel trace-based model for critical sections that do not assume per-thread confinement, aligning better with real C/Pthread program behaviors.

Findings

Critical sections can span multiple threads in real programs.

The new model captures multi-thread critical sections.

Addresses semantic gaps in traditional lock set analysis.

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.