6 min read
On this page

Concurrency Semantics

Overview

Concurrency semantics provides formal frameworks for reasoning about systems with multiple interacting agents. Key concerns: communication, synchronization, nondeterminism, and equivalence of concurrent behaviors.

Process Algebra

Algebraic frameworks for modeling concurrent systems as compositions of communicating processes.

CCS (Calculus of Communicating Systems) - Milner, 1980

Syntax

P ::= 0             (inaction / nil)
    | a.P            (action prefix: perform a, then behave as P)
    | P1 + P2        (choice: nondeterministic)
    | P1 | P2        (parallel composition)
    | P \ L          (restriction: hide actions in set L)
    | P[f]           (relabeling: rename actions via f)
    | A              (process identifier / recursion)

Actions: a (input on channel a), ā (output on channel a), τ (internal/silent action).

Semantics

Defined via labeled transition system (LTS). Key rule for synchronization:

P --a-->  P'    Q --ā--> Q'
────────────────────────────
    P | Q --τ--> P' | Q'

Complementary actions synchronize, producing a silent transition.

Example

Buffer = in.out.Buffer        -- receive then send, repeat
System = (Producer | Buffer | Consumer) \ {in, out}

CSP (Communicating Sequential Processes) - Hoare, 1978

Key Differences from CCS

  • Events rather than input/output actions; synchronization is symmetric (handshake)
  • Richer operators: sequential composition, interrupt, hiding
  • Traces model, failures model, and failures-divergences model for semantic analysis

Syntax (Core)

P ::= STOP                    (deadlock)
    | SKIP                    (successful termination)
    | a -> P                  (prefix)
    | P □ Q                   (external choice: environment decides)
    | P ⊓ Q                   (internal choice: process decides)
    | P ||| Q                 (interleaving)
    | P [|A|] Q               (parallel: sync on events in A)
    | P \ A                   (hiding events in A)
    | P ; Q                   (sequential composition)

Semantic Models

  • Traces: set of possible event sequences. traces(P) ⊆ Σ*
  • Failures: (trace, refusal_set) pairs. A process can refuse a set of events after a trace
  • Failures-Divergences: adds divergence information (infinite internal activity)
  • Refinement: P ⊑ Q means Q has fewer behaviors than P (Q refines P)

Pi-Calculus - Milner, Parrow, Walker, 1992

Extends CCS with name passing: channels can be communicated over channels, enabling dynamic reconfiguration of communication topology.

Syntax

P ::= 0                       (inaction)
    | x̄⟨y⟩.P                  (output y on channel x)
    | x(z).P                   (input on x, bind to z)
    | P | Q                    (parallel)
    | (νx)P                    (restriction: create fresh name x)
    | !P                       (replication: infinite copies of P)
    | P + Q                    (choice)

Key Feature: Mobility

-- Pass a private channel:
(νc)(x̄⟨c⟩.P | x(z).Q)  -->  (νc)(P | Q[c/z])

After communication, Q knows the private channel c - the communication topology has changed.

Scope Extrusion

When a private name is sent outside its scope, the scope expands:

(νc)(x̄⟨c⟩.P) | x(z).Q  -->  (νc)(P | Q[c/z])

The restriction νc widens to cover Q.

Expressiveness

  • Encodes the lambda calculus (Milner's encoding)
  • Models mobile code, dynamic network topologies, object-oriented systems
  • Variants: asynchronous pi-calculus (no output prefix), polyadic pi-calculus (tuple passing), higher-order pi-calculus (process passing)

Bisimulation

The standard equivalence for concurrent processes: two processes are equivalent if they can simulate each other step by step.

Strong Bisimulation

A relation R between processes is a strong bisimulation if whenever P R Q:

  1. If P --a--> P', then there exists Q' such that Q --a--> Q' and P' R Q'
  2. If Q --a--> Q', then there exists P' such that P --a--> P' and P' R Q'

Strong bisimilarity ~ is the largest strong bisimulation.

Weak Bisimulation

Abstracts away from internal (τ) actions. Uses ==> for zero or more τ steps and --a==> for ==> --a--> ==>.

A relation R is a weak bisimulation if whenever P R Q:

  1. If P --a--> P' and a ≠ τ, then Q' exists with Q --a==> Q' and P' R Q'
  2. If P --τ--> P', then Q' exists with Q ==> Q' and P' R Q'
  3. Symmetric conditions for Q

Weak bisimilarity ≈ equates processes that differ only in internal behavior.

Congruence

Bisimilarity should be a congruence (preserved by all contexts). Strong bisimilarity is a congruence for CCS. Weak bisimilarity is NOT a congruence for CCS (fails under choice +). Observation congruence fixes this.

Coinductive Reasoning

Bisimulation is naturally coinductive. To prove P ~ Q, exhibit a bisimulation relation containing (P, Q). The bisimulation proof principle is the coinduction principle for the greatest fixed point.

Other Equivalences

  • Trace equivalence: same set of observable traces (weaker than bisimulation)
  • Testing equivalence (De Nicola, Hennessy): based on interaction with testers
  • Barbed congruence: based on observable barbs and closure under contexts

Session Types

Type systems for communication protocols. Ensure that communicating processes follow prescribed message patterns.

Binary Session Types

Types describe the communication behavior from one endpoint's perspective.

S ::= !T.S          (send value of type T, continue as S)
    | ?T.S           (receive value of type T, continue as S)
    | S1 ⊕ S2        (internal choice: select between S1 and S2)
    | S1 & S2         (external choice: offer S1 or S2)
    | μα. S          (recursive session)
    | end            (session termination)

Duality

For every session type, there is a dual type (the other endpoint's perspective):

dual(!T.S) = ?T.dual(S)
dual(?T.S) = !T.dual(S)
dual(S1 ⊕ S2) = dual(S1) & dual(S2)
dual(end) = end

If one endpoint has type S, the other must have type dual(S). This guarantees communication safety and deadlock freedom (for two-party sessions).

Example

-- ATM protocol from client's perspective:
ATM = !Card. !PIN. ?(Auth ⊕ Denied).
      (Auth: !Amount. ?(Dispense ⊕ Insufficient). end
      | Denied: end)

Multiparty Session Types (MPST)

Extend binary sessions to protocols with three or more participants.

Global Types

Describe the entire protocol from a bird's-eye view:

G = A -> B: Request.
    B -> C: Query.
    C -> B: Response.
    B -> A: Result.
    end

Projection

Each participant's local type is obtained by projecting the global type:

proj(G, A) = !B:Request. ?B:Result. end
proj(G, B) = ?A:Request. !C:Query. ?C:Response. !A:Result. end
proj(G, C) = ?B:Query. !B:Response. end

Properties

  • Well-formedness conditions on global types ensure projectability
  • Deadlock freedom for well-typed multiparty sessions
  • Progress: well-typed sessions always make progress (no stuck states)
  • Implementations: Scribble (protocol description language), session-typed APIs in various languages

Actor Model Formalization

Hewitt's Actor Model (1973)

Each actor is an autonomous entity with:

  • A mailbox (message queue)
  • Behavior (message handler)
  • Identity (address)

Upon receiving a message, an actor can:

  1. Send messages to known actors
  2. Create new actors
  3. Designate its replacement behavior (become)

Formal Semantics

Actor configurations: ⟨actors, messages_in_transit⟩

⟨{..., a ↦ (behavior, mailbox)}, msgs⟩

Transition: actor a processes message m from its mailbox:

⟨{a ↦ (beh, m::rest), ...}, msgs⟩
  -->
⟨{a ↦ (beh', rest), new_actors...}, msgs ∪ sent_msgs⟩

Properties

  • Fairness: every sent message is eventually delivered; every ready actor eventually processes a message
  • No shared state: communication only via asynchronous messages
  • Location transparency: actor addresses are abstract; actors may be local or remote
  • Nondeterminism: message delivery order is not guaranteed

Relationship to Other Models

  • Actors can encode pi-calculus (and vice versa) under suitable fairness assumptions
  • Erlang/OTP: practical realization with supervision trees, hot code swapping
  • Akka (Scala/Java): actor framework with typed actors using session-type-like protocols

Linearizability

The standard correctness condition for concurrent data structures.

Definition (Herlihy and Wing, 1990)

A concurrent execution history is linearizable if:

  1. Each operation can be assigned a linearization point within its execution interval
  2. The sequential history obtained by ordering operations by their linearization points is valid (satisfies the sequential specification)

Intuition

Every concurrent execution "appears" to happen atomically at some point between invocation and response.

Formal Framework

  • History: sequence of invoke/response events
  • Complete history: every invocation has a matching response
  • Sequential specification: set of valid sequential histories
  • Linearizability: for every concurrent history H, there exists a sequential history S such that S is in the specification and S preserves the real-time ordering of H

Properties

  • Composable (locality): a history is linearizable iff each object's sub-history is linearizable independently
  • Non-blocking: does not by itself require processes to wait
  • Strictly stronger than sequential consistency (which relaxes real-time ordering)

Verification Approaches

  • Identify linearization points (often the atomic instruction: CAS, load, store)
  • Prove a simulation relation between the concurrent implementation and the sequential specification
  • Automated tools: SPIN model checker, TLA+, Iris (Coq framework for concurrent separation logic)

Hierarchy of Consistency Conditions

Linearizability (strongest)
  ⊃ Sequential consistency
    ⊃ Causal consistency
      ⊃ Eventual consistency (weakest)

Summary

| Framework | Focus | Key Concept | |---|---|---| | CCS | Synchronous communication | Action prefix, parallel, restriction | | CSP | Synchronization, refinement | Traces, failures, refinement checking | | Pi-calculus | Mobility, name passing | Scope extrusion, dynamic topology | | Bisimulation | Process equivalence | Step-by-step matching | | Session types | Protocol conformance | Duality, projection | | Actor model | Asynchronous messaging | Mailbox, become, fairness | | Linearizability | Correctness of concurrent objects | Linearization points |

These frameworks provide complementary tools for specifying, verifying, and reasoning about concurrent and distributed systems.