Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Martin Sulzmann

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 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.

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

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 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.
Paper Structure (11 sections, 4 theorems, 3 equations, 2 figures)

This paper contains 11 sections, 4 theorems, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Contributions
  3. Outline
  4. Events and Traces
  5. Critical Section and Lock Set
  6. Per-Thread Definition
  7. Trace-Based Characterization
  8. Related Work
  9. Deadlock detection
  10. Data race detection
  11. Conclusion

Key Result

Lemma 3.5

Let $T$ be a well-formed trace with some event $e=(\tau,op) \in T$ where $m \in LH_{T}^{\tau}(e)$. Then, $m \in LH_{T'}^{\tau}(e)$ for any reordering $T' \in \mathit{crp}(T)$ where $e \in T'$ and $T'$ additionally satisfies WF-Acq2.

Figures (2)

  • Figure 1: C/Pthread program.
  • Figure 2: Trace $T_1$ resulting from execution of the program in \ref{['fig:real']}.

Theorems & Definitions (18)

  • Definition 2.1: Events and Traces
  • Example 2.2
  • Definition 2.3: Well Formedness
  • Example 2.4
  • Example 2.5
  • Definition 2.6: Correctly Reordered Prefix
  • Definition 3.1: Matching Lock and Unlock Events
  • Definition 3.2: Per-Thread Critical Section
  • Definition 3.3: Per-Thread Locks Held
  • Example 3.4
  • ...and 8 more