Chapter 6.5 — Threading & GIL

Verified concurrent Python — locks, data races, and the GIL

Python's Global Interpreter Lock

The GIL is a mutex held by the CPython interpreter that allows only one thread to execute Python bytecode at a time. Understanding precisely what the GIL guarantees — and what it does not — is essential for verified concurrent Python.

What the GIL Guarantees

• Single bytecode atomicity: Each individual bytecode instruction executes atomically. LOAD_FAST, STORE_FAST, BINARY_ADD — each completes without interruption.
• Interpreter integrity: Internal CPython data structures (refcounts, object headers, the GC) are never corrupted by concurrent access.
• No segfaults: Concurrent Python threads cannot crash the interpreter.

What the GIL Does NOT Guarantee

• Compound operation atomicity: x += 1 compiles to LOAD_FAST → BINARY_ADD → STORE_FAST. A thread switch can occur between any two of these bytecodes.
• Logical consistency: Two threads can read and write the same variable in an interleaved order that violates application invariants.
• Dictionary safety: While individual dict operations are atomic under the GIL, sequences like "check-then-act" are not.

# ✗ NOT THREAD-SAFE despite the GIL
def unsafe_increment():
    global counter
    counter += 1
    # Bytecodes:              Thread A      Thread B
    # LOAD_FAST counter        → 5
    #                                        LOAD_FAST counter → 5
    # BINARY_ADD 1             → 6
    #                                        BINARY_ADD 1      → 6
    # STORE_FAST counter       ← 6
    #                                        STORE_FAST counter ← 6  ← LOST UPDATE!

Lock Verification

In Deppy's separation logic, a lock owns a piece of the heap described by an SLProp called the lock invariant. When you acquire the lock, you gain ownership of that heap region. When you release it, you give it back.

from deppy.concurrency import Lock, lock_inv
from deppy.separation import pts_to, exists

# Create a lock that protects a counter reference
counter: Ref[int] = Ref(0)
# Lock invariant: "the counter exists and holds some integer"
lock = Lock(invariant=exists('n', pts_to(counter, 'n')))

Acquire and Release

# Acquiring the lock gives you the invariant
@requires(lock_inv(lock))  # must know the lock exists
@ensures(lambda _:
    lock_inv(lock) **            # lock still exists
    exists('n', pts_to(counter, 'n')))  # now own the counter!
def acquire_example(lock: Lock):
    lock.acquire()

# Releasing returns the invariant to the lock
@requires(
    lock_inv(lock) **
    exists('n', pts_to(counter, 'n')))
@ensures(lambda _: lock_inv(lock))  # gave back ownership
def release_example(lock: Lock):
    lock.release()

Spin Lock Implementation

A spin lock is the simplest lock: a boolean flag that threads poll in a loop. We implement and verify one using separation logic:

from deppy.concurrency import atomic_cas

class SpinLock:
    def __init__(self, invariant: SLProp):
        self._locked = Ref(False)
        self._invariant = invariant

    @requires(spin_lock_inv(self))
    @ensures(lambda _: spin_lock_inv(self) ** self._invariant)
    def acquire(self):
        """Spin until lock is acquired."""
        while True:
            # atomic compare-and-swap: if _locked is False, set True
            if atomic_cas(self._locked, expected=False, desired=True):
                break
        # Now own the invariant

    @requires(spin_lock_inv(self) ** self._invariant)
    @ensures(lambda _: spin_lock_inv(self))
    def release(self):
        """Release the lock, returning the invariant."""
        self._locked.value = False

Parallel Increment

The canonical concurrent verification problem: multiple threads increment a shared counter, and we prove the final value equals the initial value plus the number of increments.

from deppy.concurrency import Lock, parallel_safe, spawn, join_all
from deppy.ghost import ghost_var, ghost_pts_to

counter = Ref(0)
contributions = ghost_var(0)  # ghost: total increments performed

lock = Lock(invariant=
    exists('n', 'g',
        pts_to(counter, 'n') **
        ghost_pts_to(contributions, 'g') **
        pure('n == g')  # counter == total contributions
    ))

@parallel_safe
@requires(lock_inv(lock))
@ensures(lambda _: lock_inv(lock))
def parallel_incr(lock: Lock, counter: Ref[int]):
    """Thread-safe increment with proof."""
    with lock:
        # Inside lock: we own pts_to(counter, n) ** ghost_pts_to(contributions, g)
        # and we know n == g
        counter.value += 1
        ghost_update(contributions, lambda g: g + 1)
        # Now: counter = n+1, contributions = g+1, n+1 == g+1 ✓

Proving the Final Value

@requires(lock_inv(lock) ** pure('counter.value == 0'))
@ensures(lambda _: pure('counter.value == num_threads'))
def run_parallel_incr(num_threads: int):
    """Spawn num_threads threads, each incrementing once."""
    threads = []
    for _ in range(num_threads):
        t = spawn(parallel_incr, args=(lock, counter))
        threads.append(t)
    join_all(threads)
    # After all joins: contributions == num_threads
    # Lock invariant: counter == contributions
    # Therefore: counter == num_threads ✓

Condition Variables

Condition variables let threads wait for a predicate to become true. Deppy verifies that the predicate actually holds when the thread wakes up:

from deppy.concurrency import Condition

class BoundedBuffer:
    def __init__(self, capacity: int):
        self.buf: list = []
        self.capacity = capacity
        self.lock = Lock()
        self.not_full = Condition(self.lock)
        self.not_empty = Condition(self.lock)

    @requires(lock_inv(self.lock))
    @ensures(lambda _:
        lock_inv(self.lock) and
        pure('item in self.buf'))
    def put(self, item):
        with self.lock:
            while len(self.buf) >= self.capacity:
                self.not_full.wait()
            # post-wait: len(self.buf) < self.capacity
            self.buf.append(item)
            self.not_empty.notify()

    @requires(lock_inv(self.lock))
    @ensures(lambda result:
        lock_inv(self.lock) and
        pure('result was in self.buf'))
    def get(self):
        with self.lock:
            while len(self.buf) == 0:
                self.not_empty.wait()
            # post-wait: len(self.buf) > 0
            item = self.buf.pop(0)
            self.not_full.notify()
            return item

Data Race Detection

A data race occurs when two threads access the same memory location concurrently and at least one access is a write, without synchronisation. Deppy detects races as ownership violations:

# ✗ DATA RACE: both threads write counter without a lock
counter = Ref(0)

@parallel_safe
def thread_a():
    counter.value += 1  # needs pts_to(counter, _) — but who owns it?

@parallel_safe
def thread_b():
    counter.value += 1  # also needs pts_to(counter, _) — conflict!

Semaphores

from deppy.concurrency import Semaphore

# A semaphore with count n owns n copies of a resource
pool = Semaphore(
    count=3,
    invariant=connection_resource()  # each permit owns a DB connection
)

@requires(sem_inv(pool))
@ensures(lambda _: sem_inv(pool))
def use_connection():
    with pool:
        # Own one connection_resource() here
        db.execute("SELECT 1")
    # Released: connection returned to pool

Thread-Safe Data Structures

Verified Thread-Safe Queue

from deppy.concurrency import Lock, Condition
from deppy.ghost import ghost_var

class VerifiedQueue:
    """Thread-safe queue with verified properties:
    1. No data races
    2. FIFO ordering preserved
    3. No lost items
    """
    def __init__(self):
        self._items: list = []
        self._lock = Lock()
        self._not_empty = Condition(self._lock)
        self._enqueued = ghost_var(0)  # total items ever enqueued
        self._dequeued = ghost_var(0)  # total items ever dequeued

    @parallel_safe
    @requires(lock_inv(self._lock))
    @ensures(lambda _: lock_inv(self._lock))
    def put(self, item):
        with self._lock:
            self._items.append(item)
            ghost_update(self._enqueued, lambda n: n + 1)
            self._not_empty.notify()
            # invariant: len(_items) == _enqueued - _dequeued

    @parallel_safe
    @requires(lock_inv(self._lock))
    @ensures(lambda result: lock_inv(self._lock))
    def get(self):
        with self._lock:
            while not self._items:
                self._not_empty.wait()
            item = self._items.pop(0)
            ghost_update(self._dequeued, lambda n: n + 1)
            return item

Verified Thread-Safe Dictionary

class VerifiedDict:
    """Thread-safe dictionary wrapper."""
    def __init__(self):
        self._data = {}
        self._lock = Lock()

    @parallel_safe
    @requires(lock_inv(self._lock))
    @ensures(lambda _:
        lock_inv(self._lock) and
        pure('key in self._data and self._data[key] == value'))
    def put(self, key, value):
        with self._lock:
            self._data[key] = value

    @parallel_safe
    @requires(lock_inv(self._lock))
    @ensures(lambda result: lock_inv(self._lock))
    def get(self, key, default=None):
        with self._lock:
            return self._data.get(key, default)

    @parallel_safe
    @requires(lock_inv(self._lock))
    @ensures(lambda _: lock_inv(self._lock))
    def setdefault(self, key, value):
        """Atomic check-then-set — no TOCTOU race."""
        with self._lock:
            if key not in self._data:
                self._data[key] = value
            return self._data[key]

Comparison with Pulse

(* Pulse parallel incr *)
fn incr
  (l: lock (exists n. pts_to c n))
  requires lock_alive l
  ensures  lock_alive l
{
  acquire l;
  let v = !c;
  c := v + 1;
  release l;
}

@parallel_safe
@requires(lock_inv(lock))
@ensures(lambda _: lock_inv(lock))
def incr(lock, counter):
    with lock:
        counter.value += 1

# Python's `with` handles
# acquire + release

Key differences:

• with statement — Python's context manager makes acquire/release implicit and exception-safe. Deppy verifies both the happy path and exception paths.
• GIL modelling — Deppy's prover knows about the GIL and can use it to simplify proofs for single-bytecode operations.
• No extraction — Pulse extracts to C; Deppy verifies Python directly.

if key not in shared_dict:
    shared_dict[key] = expensive_compute(key)