Advanced Topics and Research Directions

This module is a guided tour of where concurrency research and advanced engineering are heading — and of the mathematical tools experts use to be *sure* a design is right.

Learning Objectives

Compare lock-free and wait-free algorithms; software and hardware transactional memory; RCU, epoch-based reclamation and hazard pointers.

Understand actors and supervision trees, CSP, dataflow and reactive programming, reactive streams and backpressure protocols, the evolution of structured concurrency, virtual threads and lightweight processes, fibers and user-mode scheduling, continuations and compiler transformations of async functions, work-stealing and NUMA-aware scheduling, GPU kernels and SIMD.

Survey distributed coordination and leases, CRDTs, deterministic parallelism, formal verification and model checking (TLA+/PlusCal, Petri nets, state-space exploration), linearizability proofs, memory-model litmus testing, real-time scheduling theory and mixed-criticality systems; read research papers critically.

Plain-Language Explanation

This module is a guided tour of where concurrency research and advanced engineering are heading — and of the mathematical tools experts use to be *sure* a design is right. A few ideas are demonstrated with small runnable models (a CRDT, a model checker, a scheduling comparison); the rest come with pointers to go deeper.

Precise Technical Explanation

Lock-free versus wait-free algorithms Wait-free algorithms bound every thread's steps (using helping mechanisms); they are complex and often slower on average but valuable for real-time and adversarial settings. Universal constructions show any object can be made wait-free with consensus objects (Herlihy's hierarchy: CAS has infinite consensus number).

Software transactional memory Group reads and writes into transactions that commit atomically or retry (Haskell STM, Clojure refs, ScalaSTM). Composable — no lock ordering — but costs logging/validation and cannot contain irreversible I/O.

Hardware transactional memory CPU support for speculative critical sections (Intel TSX — disabled on many CPUs after errata and security issues; IBM POWER/z HTM; Arm TME specification). Used for lock elision with a fallback lock.

Read-copy-update (RCU) Modules 18–19: readers without synchronization, grace periods for reclamation; pervasive in the Linux kernel.

Module 19; standardised in C++26.

Actors and supervision trees Erlang/OTP: processes supervised hierarchically; failures are handled by restarting subtrees ("let it crash") with restart strategies (one-for-one, one-for-all) and intensity limits.

CSP and communicating sequential processes Hoare's algebra of processes communicating over channels — the foundation of Go, occam, Clojure core.async; amenable to formal analysis (FDR refinement checker).

Dataflow and reactive programming Computation as a graph where nodes fire when inputs are available (TensorFlow graphs, Excel, build systems); reactive programming propagates changes through dependency graphs (Rx, signals in UI frameworks).

Reactive streams and demand A protocol where subscribers signal demand (request(n)) and publishers never send more — backpressure across asynchronous boundaries (Reactive Streams spec, Java Flow, Akka Streams, Project Reactor).

Credit-based flow control (HTTP/2 windows, AMQP credits, reactive request(n)), TCP windows, pull-based streams.

Structured concurrency evolution From Dijkstra's structured programming to Trio nurseries (2018), Kotlin scopes, Swift task groups, Python TaskGroup (3.11), Java StructuredTaskScope (previews since 19/21).

Virtual threads and lightweight processes Erlang processes, goroutines, Java virtual threads,.NET's experiments with green threads (2023, not shipped) — cheap blocking-style concurrency.

Fibers and user-mode scheduling Windows UMS (deprecated), Boost.Fiber, Ruby fibers with scheduler hooks; trade kernel scheduling for application control.

Continuations and async state machines Delimited continuations capture "the rest of the computation"; async/await compiles to state machines (stackless) or captured stacks (stackful); Java's virtual threads use internal continuations.

Compiler transformations for async functions CPS transformation, state-machine lowering (C#, Rust, Kotlin), coroutine frame allocation and heap-elision optimisations (C++20 HALO).

Cilk's provably efficient work stealing (expected time T₁/P + O(T∞)); Chase-Lev deques (Module 19); used by TBB, Tokio, Go, ForkJoinPool.

Keep tasks and their data on the same socket; hierarchical work stealing (steal locally first).

GPU kernels and parallel execution SIMT execution of thousands of threads in warps/wavefronts; divergence, memory coalescing and occupancy decide performance (CUDA, ROCm, SYCL, WebGPU).

Data parallelism within a core (Module 16); explicit (intrinsics, std::simd) or auto-vectorised.

Distributed coordination and leases Consensus (Paxos, Raft) for replicated state machines; leases and fencing (Module 20); ZooKeeper/etcd as coordination services.

CRDT overview as a concurrency-related distributed data model

Conflict-free replicated data types merge concurrent updates deterministically without coordination: state-based CRDTs merge with a join (commutative, associative, idempotent) — G-Counter, PN-Counter, OR-Set, LWW-Register, sequence CRDTs for collaborative editing (implemented below).

Programs whose parallel execution always gives the same result (deterministic reductions, Rust Rayon with pure functions, Deterministic Parallel Java, data-race freedom by construction).

Formal verification and model checking Exhaustively explore a model's state space (SPIN, TLC, CBMC) or prove properties (Coq, Isabelle, Dafny, Iris for concurrent separation logic).

TLA+ / PlusCal overview Leslie Lamport's specification language: describe system states and next-state actions; TLC model-checks invariants and liveness; PlusCal is an algorithm language that translates to TLA+. Used at AWS, Microsoft (Azure Cosmos DB), MongoDB. Specification excerpt below (not run).

Petri nets and state-space exploration Bipartite graphs of places and transitions with tokens model concurrency, synchronization and resource sharing; reachability analysis finds deadlocks.

Identify linearization points; prove abstraction relations; tools: refinement proofs, Iris, automated checkers for small bounds.

Memory-model litmus testing herd7/diy generate and evaluate litmus tests against formal models (x86-TSO, Arm, Power, C11); litmus7 runs them on hardware (Module 7 ran SB by hand).

Real-time scheduling theory Rate-monotonic (fixed priority, optimal among fixed-priority for implicit deadlines; utilisation bound n(2^{1/n} − 1)) and earliest-deadline-first (dynamic priority, schedulable iff U ≤ 1 for implicit deadlines on one core); response-time analysis; resource access protocols (PIP, PCP, SRP). Compared below.

Mixed-criticality systems overview Tasks of different safety levels share hardware; scheduling guarantees high-criticality deadlines under pessimistic WCET while running low-criticality tasks opportunistically (Vestal's model); partitioning (ARINC 653) in avionics.

Research papers and how to read them critically Check the assumptions (memory model, failure model, contention level), the workloads (micro-benchmarks vs real), the baselines (tuned or straw-man), the hardware, the variance reported, artefact availability and reproducibility, and whether correctness is proved, model-checked or only tested.

Why It Matters in Real Systems

Today's research becomes tomorrow's runtime: hazard pointers are entering C++, structured concurrency and virtual threads entered Java, CRDTs power collaborative editors, and TLA+ specs find design bugs before code exists.

Key Terms

Software / hardware transactional memory Hierarchy of supervisors restarting failed workers Communicating Sequential Processes

Asynchronous streams with demand-based backpressure Conflict-free replicated data type

Formal specification language with the TLC model checker Earliest-deadline-first / rate-monotonic scheduling

Syntax and API Overview

This is a concurrency concept, not a language construct. A PlusCal sketch of two processes incrementing a shared counter (not run — illustrates how model checkers express interleavings):

--algorithm Counter
variables counter = 0;
process Worker \in {1, 2}
variables tmp = 0;
begin
  Load:  tmp := counter;
  Store: counter := tmp + 1;
end process;
end algorithm;
\* Invariant checked by TLC at termination:  counter = 2   -> violated (lost update found)

Complete Code Example

A model checker for Peterson's mutual-exclusion algorithm (and a broken variant), a state-based CRDT counter, and rate-monotonic versus EDF scheduling of the same task set (CPython 3.13.1; exhaustive and deterministic — models, not real threads):

from collections import deque


def explore(algorithm):
    """Breadth-first search over every interleaving of two processes; report mutual-exclusion violations."""
    init = (0, 0, False, False, 0)            # pc0, pc1, flag0, flag1, turn
    seen, frontier, violations = {init}, deque([init]), 0
    while frontier:
        state = frontier.popleft()
        if state[0] == 3 and state[1] == 3:   # both in the critical section
            violations += 1
        for me in (0, 1):
            for nxt in algorithm(state, me):
                if nxt not in seen:
                    seen.add(nxt); frontier.append(nxt)
    return len(seen), violations


def peterson(state, me):
    pcs = list(state[:2]); flags = list(state[2:4]); turn = state[4]
    other = 1 - me
    pc = pcs[me]
    if pc == 0:   flags[me] = True; pcs[me] = 1                    # flag[me] = true
    elif pc == 1: turn = other; pcs[me] = 2                        # turn = other
    elif pc == 2:                                                   # wait while flag[other] and turn == other
        if flags[other] and turn == other:
            return []
        pcs[me] = 3
    elif pc == 3: pcs[me] = 4                    
…

Peterson              :  26 reachable states, 0 with both processes in the critical section
check-then-set flags  :  25 reachable states, 1 with both processes in the critical section
G-Counter replicas converge: 11 11 11
RM  U=0.971: missed deadlines ['B@7'] | AABBBAABBBAAB.BAABBBAABBBAABBBAABB.
EDF U=0.971: missed deadlines none | AABBBBAABBBBAABAABBBAABBBBAABBBBAA.

Line-by-Line Explanation

Model checking: each state is (program counters, flags, turn); every step of either process generates successor states; BFS visits every reachable state. Peterson's algorithm has no state with both processes at the critical-section step. The broken "check, then set my flag" version has reachable states where both are inside — the model checker finds the race that testing might miss. (The model assumes sequentially consistent memory; on real hardware Peterson's algorithm needs fences.)

CRDT: each replica increments only its own entry; merging takes the maximum per entry, which is commutative, associative and idempotent — so replicas converge to 11 regardless of gossip order or repetition.

Scheduling: with utilisation 0.971 (above the two-task RM bound of 0.828), rate-monotonic priorities miss a deadline of B, while EDF meets every deadline (EDF is optimal on one core when U ≤ 1).

Interleaving or State Trace

The model checker's counter-example for the broken algorithm: P0 checks flag1 = false → P1 checks flag0 = false → P0 sets flag0 → P1 sets flag1 → both enter.

Correctness and Safety Analysis

Exhaustive exploration gives a proof for the finite model (all interleavings under its assumptions); proofs about real code need models of the memory model, unbounded state or theorem proving.

Common Mistakes and Misconceptions

Treating model-checking results as covering assumptions the model did not include (weak memory, failures).

Believing STM removes all concurrency bugs (it removes lock-ordering issues, not logic errors or livelock).

Using CRDTs where invariants need coordination (e.g. "balance ≥ 0" cannot be maintained by a PN-Counter without coordination).

Using rate-monotonic analysis with deadlines shorter than periods without adjusting it.

Failure Modes and Debugging Steps

When a specification's invariant fails, the model checker provides a minimal trace — reproduce it in code with test hooks (Module 24).

Performance and Scalability Implications

STM/HTM trade abort overhead for composability; RCU trades write cost for read speed; CRDTs trade metadata size for coordination-free writes; EDF achieves full utilisation at the cost of dynamic priorities and harder overload behavior.

Security Considerations

Formal methods find design-level races that become vulnerabilities; HTM was disabled on many CPUs partly due to side-channel concerns (TAA, CVE-2019-11135).

Platform and Runtime Caveats

TLA+ tools (TLC, Apalache), SPIN, herd7 and CBMC are separate tools not used in this build; C++26 hazard pointers and RCU are not yet in mainstream standard libraries.

Real-World Applications

AWS's use of TLA+ for DynamoDB and S3; Erlang/OTP telecom systems; Figma/Automerge/Yjs collaborative editing with CRDTs; Linux RCU; real-time schedulers in avionics and automotive (ARINC 653, AUTOSAR).

Best Practices

Model-check tricky protocols before implementing them.

Prefer proven runtime features (virtual threads, structured concurrency, reclamation libraries) over home-grown versions.

Choose CRDTs for availability-first replicated data without strong invariants.

Apply schedulability analysis to real-time task sets.

Read research claims critically and reproduce before adopting.

Exercises

E1 · Beginner. Why does the G-Counter merge use max rather than addition?

Answer: Merges may repeat or arrive in any order; max is idempotent and order-independent, while addition would double-count repeated merges.

E2 · Intermediate. Why is Peterson's algorithm insufficient on real x86 hardware without fences?

Answer: x86 allows a store (setting the flag) to be delayed in the store buffer past the subsequent load of the other process's flag (store-load reordering, Module 7), so both processes can read the other's flag as false and enter. A full fence (or seq_cst atomics) after setting the flag fixes it.

E3 · Advanced challenge. Extend the model checker to check *starvation freedom* for Peterson's algorithm.

Answer: Liveness needs cycle detection under fairness: build the state graph, find strongly connected components reachable where a process waits (pc = 2) forever while the other is scheduled fairly; Peterson has none (bounded waiting), so every waiting process eventually enters. Tools such as TLC check this with fairness assumptions (WF_vars).

Quiz

? What property makes a state-based CRDT merge safe to repeat and reorder?
+ It is commutative, associative and idempotent. :: Convergence regardless of delivery order.
- It uses locks across replicas. :: CRDTs avoid coordination.
- It always takes the newest timestamp. :: That is one specific CRDT (LWW), not the general property.
- It runs only on the leader. :: There is no leader.

? Which scheduling policy is optimal on a single core for implicit-deadline periodic tasks with U <= 1?
+ Earliest Deadline First :: Dynamic priorities.
- Rate Monotonic :: Optimal only among fixed-priority policies, with a lower bound.
- FIFO :: Ignores deadlines.
- Round robin :: Ignores deadlines.

? Which are true? (select all that apply)
+ Model checkers explore all interleavings of a finite model. :: Exhaustive.
+ STM transactions should not contain irreversible I/O. :: They may be retried.
- Hardware transactional memory is enabled on all modern x86 CPUs. :: TSX was disabled on many.
+ Reactive streams use demand signals for backpressure. :: request(n).

Summary

Advanced concurrency spans progress guarantees (lock-/wait-free), composable atomicity (STM/HTM), safe reclamation (RCU, epochs, hazard pointers), process-oriented models (actors, CSP), dataflow and reactive streams, lightweight threads and scheduler design, coordination-free data (CRDTs), formal methods (TLA+, model checking, linearizability proofs, litmus testing) and real-time theory (RM, EDF, mixed criticality) — with critical reading of research as a core skill.