Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes

Kevin Chalmers, Jan Bækgaard Pedersen

TL;DR

The paper presents a completely spin-free, CAS-based claim/release protocol for shared resource access in cooperatively scheduled runtimes, demonstrated within the ProcessJ context. It combines a lock-free queue and ownership/state CAS mechanisms to ensure mutual exclusion with FIFO fairness, without invoking kernel-level locks or busy-wait spinning. Using CSP and the FDR model checker, the authors develop a compositional mutex specification, verify linearizability and stability, and introduce a fairness oracle to separate fairness from the mutex core. The work provides a reusable CSP model framework, a Java reference implementation, and an inductive argument for scalability beyond the verified four processes, with clear implications for lock-free runtimes on the JVM and similar environments.

Abstract

We present the first spin-free, kernel-lock-free mutex that cooperates with user-mode schedulers and is formally proven FIFO-fair and linearizable using CSP/FDR. Our fairness oracle and stability-based proof method are reusable across coroutine runtime designs. We designed the claim/release protocol for a process-oriented language -- ProcessJ -- to manage the race for claiming shared inter-process communication channels. Internally, we use a lock-free queue to park waiting processes for gaining access to a shared object, such as exclusive access to a shared channel to read from or write to. The queue ensures control and fairness for processes wishing to access a shared resource, as the protocol handles claim requests in the order they are inserted into the queue. We produce CSP models of our protocol and a mutex specification, demonstrating with FDR that our protocol behaves as a locking mutex.

Fair Kernel-Lock-Free Claim/Release Protocol for Shared Object Access in Cooperatively Scheduled Runtimes

TL;DR

The paper presents a completely spin-free, CAS-based claim/release protocol for shared resource access in cooperatively scheduled runtimes, demonstrated within the ProcessJ context. It combines a lock-free queue and ownership/state CAS mechanisms to ensure mutual exclusion with FIFO fairness, without invoking kernel-level locks or busy-wait spinning. Using CSP and the FDR model checker, the authors develop a compositional mutex specification, verify linearizability and stability, and introduce a fairness oracle to separate fairness from the mutex core. The work provides a reusable CSP model framework, a Java reference implementation, and an inductive argument for scalability beyond the verified four processes, with clear implications for lock-free runtimes on the JVM and similar environments.

Abstract

We present the first spin-free, kernel-lock-free mutex that cooperates with user-mode schedulers and is formally proven FIFO-fair and linearizable using CSP/FDR. Our fairness oracle and stability-based proof method are reusable across coroutine runtime designs. We designed the claim/release protocol for a process-oriented language -- ProcessJ -- to manage the race for claiming shared inter-process communication channels. Internally, we use a lock-free queue to park waiting processes for gaining access to a shared object, such as exclusive access to a shared channel to read from or write to. The queue ensures control and fairness for processes wishing to access a shared resource, as the protocol handles claim requests in the order they are inserted into the queue. We produce CSP models of our protocol and a mutex specification, demonstrating with FDR that our protocol behaves as a locking mutex.

Paper Structure

This paper contains 79 sections, 1 theorem, 35 equations, 10 figures, 2 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Context and Motivation
  3. Contribution
  4. Breakdown of the Paper
  5. Background
  6. ProcessJ Runtime
  7. Processes in the ProcessJ Runtime
  8. The Runner
  9. Modelling Processes and Runners
  10. Shared Channels
  11. Communicating Sequential Processes
  12. Choice
  13. Pre-Guards
  14. Process Composition
  15. Traces and Hiding
  16. ...and 64 more sections

Key Result

Theorem 1

Demonstrate that $(S) + (O) + (F)$ for all cases.

Figures (10)

  • Figure 1: The ProcessJ Scheduler (Simplified).
  • Figure 2: Process State Automata.
  • Figure 3: Resolutions of (a) unclaimed and (b) claimed resource scenarios, and (c) just-in-time releasing.
  • Figure 4: Resolution of claim concurrently with release where (a) owner became null, (b) release transferred ownership but not scheduled, (c) release transferred ownership and scheduled, and (d) claim stole ownership.
  • Figure 5: Spurious Scheduling After Claim Resolution.
  • ...and 5 more figures

Theorems & Definitions (3)

  • Definition : Mutex invariant $INV(n)$
  • Theorem : $INV(n)$ holds $\forall n \geq 1 \implies$ mutual exclusion and FIFO fairness
  • proof