Memory Models: Hardware-Software Concurrency Interface

Purpose: Formal specifications of how concurrent reads and writes to shared memory interact, defining legal reorderings and visibility guarantees at the hardware and programming language level.

Core Insight: Modern processors and compilers reorder operations for performance. Memory models define which reorderings are allowed, enabling both optimization and correct concurrent programming.

Foundational Concepts
Hardware Memory Models
Programming Language Memory Models
Progress Guarantees
Synchronization Primitives
Practical Patterns
Stack-Specific Implementations
Integration Points

Foundational Concepts

What is a Memory Model?

Memory Model: Contract specifying:

Which operation reorderings are legal (loads, stores)
When writes become visible to other threads
Guarantees provided by synchronization operations

Why Needed:

Compiler Optimizations: Reorder instructions, eliminate redundant loads
CPU Optimizations: Out-of-order execution, store buffers, cache coherence
Performance: Sequential consistency too restrictive, weak models enable speed

Sequential Consistency (SC)

Definition (Lamport, 1979): “Result of any execution is the same as if operations of all processors were executed in some sequential order, and operations of each processor appear in program order.”

Intuition: Interleaving of threads as if single-threaded execution.

Example (SC):

Thread 1:        Thread 2:
x = 1            y = 1
r1 = y           r2 = x

Possible outcomes with SC:
- r1=0, r2=1  (T1 then T2)
- r1=1, r2=0  (T2 then T1)
- r1=1, r2=1  (interleaving)
Impossible: r1=0, r2=0 (would require reordering)

Cost: Requires memory fences after every store → slow on modern hardware.

Happens-Before Relation

Happens-Before (→): Foundation for reasoning about concurrent execution.

Rules:

Program Order: If A before B in thread, A → B
Synchronization Order: Release → Acquire on same variable
Transitivity: A → B and B → C ⇒ A → C

Data Race: Concurrent accesses where at least one is write and not ordered by →.

Data-Race-Free (DRF): Program with no data races behaves as if sequentially consistent.

Reordering Categories

LoadLoad: Load followed by load LoadStore: Load followed by store StoreStore: Store followed by store StoreLoad: Store followed by load (hardest to prevent)

Example:

// Original
x = 1        // Store
r = y        // Load

// Reordered (StoreLoad reordering)
r = y        // Load
x = 1        // Store

Impact: Other threads may observe loads before preceding stores.

Hardware Memory Models

x86-64: Total Store Order (TSO)

Model: Strong, close to sequential consistency.

Guarantees:

LoadLoad: Not reordered
LoadStore: Not reordered
StoreStore: Not reordered
StoreLoad: CAN be reordered (store buffer)

Store Buffer: Stores go to buffer before memory, loads bypass buffer if hit, otherwise read memory.

Example (TSO allows):

Thread 1:        Thread 2:
x = 1            y = 1
r1 = y           r2 = x

Outcome r1=0, r2=0 POSSIBLE on TSO:
- Both stores in buffers
- Both loads read memory (old values)
- Stores later drain to memory

Fence: mfence instruction ensures all prior stores visible before subsequent loads.

ARM/RISC-V: Weak Memory Model

Model: Very weak, aggressive reordering.

Allows:

All types of reordering (LoadLoad, LoadStore, StoreStore, StoreLoad)
Stores from same thread observed in different orders by different threads
Dependent loads can be reordered (speculation)

Example (ARM allows):

Thread 1:        Thread 2:
x = 1            y = 1
y = 1            r1 = y
                 r2 = x

Outcome r1=1, r2=0 POSSIBLE on ARM:
- T2 sees y=1 but not x=1 (stores reordered from T2's view)

Barriers:

dmb (Data Memory Barrier): Order memory accesses
dsb (Data Synchronization Barrier): Complete before subsequent
isb (Instruction Synchronization Barrier): Flush pipeline

Power: Even Weaker

Model: Allows more reorderings than ARM.

Additional Permissions:

Load-Store reordering even with address dependency
Requires sync or lwsync barriers

Programming Language Memory Models

C++11 Memory Model

Atomics: std::atomic<T> with memory ordering.

Memory Orders:

memory_order_relaxed: No ordering constraints
memory_order_acquire: Prevents reordering of subsequent loads/stores before acquire
memory_order_release: Prevents reordering of prior loads/stores after release
memory_order_acq_rel: Both acquire and release
memory_order_seq_cst: Sequential consistency (default)

Acquire-Release Semantics:

std::atomic<int> x{0}, y{0};

// Thread 1
y.store(1, std::memory_order_relaxed);
x.store(1, std::memory_order_release);  // Release

// Thread 2
while (x.load(std::memory_order_acquire) == 0);  // Acquire
assert(y.load(std::memory_order_relaxed) == 1);  // Always true!

Explanation: Release-acquire pair creates happens-before edge. All writes before release visible after acquire.

Relaxed Ordering:

std::atomic<int> counter{0};

// Multiple threads
counter.fetch_add(1, std::memory_order_relaxed);

Use Case: Counters, statistics (when only final value matters).

Java Memory Model (JMM)

Happens-Before Rules:

Program Order: Within thread
Monitor Lock: Unlock → Lock on same object
Volatile: Write → Read of same volatile
Thread Start: start() → first action in new thread
Thread Join: Last action in thread → join() returns
Transitivity

Volatile Variables:

class Example {
    private volatile boolean flag = false;
    private int data = 0;

    // Thread 1
    void writer() {
        data = 42;             // 1
        flag = true;           // 2 (volatile write)
    }

    // Thread 2
    void reader() {
        if (flag) {            // 3 (volatile read)
            assert data == 42; // 4 - Always true!
        }
    }
}

Guarantee: Volatile write (2) happens-before volatile read (3). By transitivity, (1) happens-before (4).

Rust Memory Model

Based on C++11: Similar atomic operations and orderings.

Ownership and Borrowing: Prevents many data races at compile time.

Atomics:

use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};

static FLAG: AtomicBool = AtomicBool::new(false);
static DATA: AtomicUsize = AtomicUsize::new(0);

// Thread 1
DATA.store(42, Ordering::Relaxed);
FLAG.store(true, Ordering::Release);

// Thread 2
while !FLAG.load(Ordering::Acquire) {}
assert_eq!(DATA.load(Ordering::Relaxed), 42);

Send and Sync Traits:

Send: Type can be transferred across threads
Sync: Type can be shared across threads (&T is Send)

Compiler Enforcement: Prevents sharing non-Sync types without synchronization.

Progress Guarantees

Classifications

Wait-Free: Every operation completes in bounded steps.

Strongest guarantee: No starvation possible
Example: Atomic fetch-and-add
Hard to implement: Complex algorithms

Lock-Free: Some operation completes in bounded steps (system-wide progress).

Guarantee: System makes progress even if threads stall
Example: Michael-Scott queue, Treiber stack
Weaker than wait-free: Individual thread may starve

Obstruction-Free: Operation completes in bounded steps if runs in isolation.

Guarantee: Progress when no contention
Example: Some transactional memory implementations
Weakest non-blocking

Blocking: No progress guarantee.

Example: Locks, mutexes
Vulnerable: To deadlock, priority inversion, convoying

Wait-Free Example: Fetch-And-Add

use std::sync::atomic::{AtomicUsize, Ordering};

fn wait_free_increment(counter: &AtomicUsize) -> usize {
    // Guaranteed to complete in one atomic operation
    counter.fetch_add(1, Ordering::SeqCst)
}

Bounded: One atomic operation, always completes.

Lock-Free Example: Treiber Stack

use std::sync::atomic::{AtomicPtr, Ordering};
use std::ptr;

struct Node<T> {
    data: T,
    next: *mut Node<T>,
}

struct TreiberStack<T> {
    head: AtomicPtr<Node<T>>,
}

impl<T> TreiberStack<T> {
    fn new() -> Self {
        TreiberStack {
            head: AtomicPtr::new(ptr::null_mut()),
        }
    }

    fn push(&self, data: T) {
        let new_node = Box::into_raw(Box::new(Node {
            data,
            next: ptr::null_mut(),
        }));

        loop {
            let head = self.head.load(Ordering::Acquire);
            unsafe { (*new_node).next = head; }

            // CAS: if head unchanged, swap it with new_node
            if self.head.compare_exchange(
                head,
                new_node,
                Ordering::Release,
                Ordering::Acquire,
            ).is_ok() {
                return; // Success
            }
            // Retry on CAS failure
        }
    }

    fn pop(&self) -> Option<T> {
        loop {
            let head = self.head.load(Ordering::Acquire);
            if head.is_null() {
                return None; // Empty
            }

            let next = unsafe { (*head).next };

            // CAS: if head unchanged, swap with next
            if self.head.compare_exchange(
                head,
                next,
                Ordering::Release,
                Ordering::Acquire,
            ).is_ok() {
                // Success: extract data and free node
                unsafe {
                    let node = Box::from_raw(head);
                    return Some(node.data);
                }
            }
            // Retry on CAS failure
        }
    }
}

Lock-Free: At least one thread makes progress per iteration (CAS succeeds).

Synchronization Primitives

Compare-And-Swap (CAS)

Atomic Operation:

CAS(addr, expected, new):
  atomic {
    old = *addr
    if old == expected:
      *addr = new
      return (true, old)
    else:
      return (false, old)
  }

Use: Foundation for lock-free data structures.

ABA Problem:

Thread 1: CAS(ptr, A, B)  // Read A
Thread 2: CAS(ptr, A, C)  // Change to C
Thread 3: CAS(ptr, C, A)  // Change back to A
Thread 1: CAS succeeds!   // But missed C interlude

Solution: Tagged pointers, version numbers

Load-Link/Store-Conditional (LL/SC)

ARM/RISC-V: Alternative to CAS.

LL(addr):  // Load-linked
  return *addr, reserve(addr)

SC(addr, value):  // Store-conditional
  if reservation valid:
    *addr = value
    return true
  else:
    return false

Advantage: No ABA problem (reservation invalidated by any write).

Fetch-And-Add (FAA)

FAA(addr, delta):
  atomic {
    old = *addr
    *addr = old + delta
    return old
  }

Use: Counters, indices, wait-free operations.

Practical Patterns

Double-Checked Locking (Correct Version)

use std::sync::{Mutex, Once};
use std::sync::atomic::{AtomicPtr, Ordering};

static INSTANCE: AtomicPtr<Singleton> = AtomicPtr::new(std::ptr::null_mut());
static ONCE: Once = Once::new();

struct Singleton {
    data: i32,
}

fn get_instance() -> &'static Singleton {
    // Fast path: already initialized
    let ptr = INSTANCE.load(Ordering::Acquire);
    if !ptr.is_null() {
        return unsafe { &*ptr };
    }

    // Slow path: initialize
    ONCE.call_once(|| {
        let instance = Box::new(Singleton { data: 42 });
        INSTANCE.store(Box::into_raw(instance), Ordering::Release);
    });

    unsafe { &*INSTANCE.load(Ordering::Relaxed) }
}

Key: Acquire-release ensures initialization visible.

Seqlock (Read-Side Scalable)

use std::sync::atomic::{AtomicUsize, Ordering};

struct Seqlock<T> {
    seq: AtomicUsize,
    data: std::cell::UnsafeCell<T>,
}

impl<T: Copy> Seqlock<T> {
    fn read(&self) -> T {
        loop {
            let seq1 = self.seq.load(Ordering::Acquire);
            if seq1 & 1 != 0 {
                // Writer active, retry
                std::hint::spin_loop();
                continue;
            }

            let data = unsafe { *self.data.get() };
            let seq2 = self.seq.load(Ordering::Acquire);

            if seq1 == seq2 {
                return data; // Consistent read
            }
            // Retry if seq changed
        }
    }

    fn write(&self, value: T) {
        // Increment seq (make odd)
        let seq = self.seq.fetch_add(1, Ordering::Release);
        unsafe { *self.data.get() = value; }
        // Increment seq (make even)
        self.seq.store(seq + 2, Ordering::Release);
    }
}

Use Case: Rarely-written, frequently-read data (e.g., time-of-day).

RCU (Read-Copy-Update)

Concept: Readers never block, writers create new version.

use std::sync::Arc;
use std::sync::atomic::{AtomicPtr, Ordering};

struct RCU<T> {
    data: AtomicPtr<T>,
}

impl<T> RCU<T> {
    fn read(&self) -> *mut T {
        self.data.load(Ordering::Acquire)
    }

    fn update(&self, new_data: T) {
        let new_ptr = Box::into_raw(Box::new(new_data));
        let old_ptr = self.data.swap(new_ptr, Ordering::Release);

        // Defer freeing old_ptr until readers done
        // (grace period, epoch-based reclamation, etc.)
        unsafe {
            // Simplified: immediate free (unsafe!)
            drop(Box::from_raw(old_ptr));
        }
    }
}

Use Case: Linux kernel (read-mostly data structures).

Stack-Specific Implementations

Rust: Atomic Operations

use std::sync::atomic::{AtomicI32, AtomicBool, Ordering};
use std::sync::Arc;
use std::thread;

/// Lock-free counter
struct Counter {
    value: AtomicI32,
}

impl Counter {
    fn new() -> Self {
        Counter {
            value: AtomicI32::new(0),
        }
    }

    fn increment(&self) -> i32 {
        self.value.fetch_add(1, Ordering::SeqCst)
    }

    fn get(&self) -> i32 {
        self.value.load(Ordering::SeqCst)
    }
}

/// Spinlock implementation
struct Spinlock {
    locked: AtomicBool,
}

impl Spinlock {
    fn new() -> Self {
        Spinlock {
            locked: AtomicBool::new(false),
        }
    }

    fn lock(&self) {
        while self.locked.swap(true, Ordering::Acquire) {
            // Spin with hint
            while self.locked.load(Ordering::Relaxed) {
                std::hint::spin_loop();
            }
        }
    }

    fn unlock(&self) {
        self.locked.store(false, Ordering::Release);
    }
}

/// Example: Parallel increment
fn parallel_counter_example() {
    let counter = Arc::new(Counter::new());
    let mut handles = vec![];

    for _ in 0..10 {
        let counter_clone = Arc::clone(&counter);
        let handle = thread::spawn(move || {
            for _ in 0..1000 {
                counter_clone.increment();
            }
        });
        handles.push(handle);
    }

    for handle in handles {
        handle.join().unwrap();
    }

    println!("Final count: {}", counter.get());
    // Always 10000 (correct!)
}

TypeScript: Atomics and SharedArrayBuffer

/**
 * TypeScript/JavaScript atomics (for SharedArrayBuffer)
 */

// Create shared memory
const sab = new SharedArrayBuffer(Int32Array.BYTES_PER_ELEMENT * 2);
const sharedArray = new Int32Array(sab);

/**
 * Atomic operations on shared memory
 */
function atomicIncrement(
  array: Int32Array,
  index: number
): number {
  // Atomic fetch-and-add
  return Atomics.add(array, index, 1);
}

function atomicCompareExchange(
  array: Int32Array,
  index: number,
  expected: number,
  replacement: number
): number {
  // Returns old value
  return Atomics.compareExchange(
    array,
    index,
    expected,
    replacement
  );
}

/**
 * Lock-free stack using CAS
 */
class LockFreeStack {
  private head: number = 0;
  private nodes: Array<{ value: any; next: number }> = [];

  push(value: any): void {
    const nodeIndex = this.nodes.length;
    this.nodes.push({ value, next: -1 });

    // CAS loop
    while (true) {
      const currentHead = this.head;
      this.nodes[nodeIndex].next = currentHead;

      // Attempt CAS (simplified, no actual atomic)
      const success = this.compareAndSwapHead(
        currentHead,
        nodeIndex
      );

      if (success) {
        break;
      }
    }
  }

  pop(): any | null {
    while (true) {
      const currentHead = this.head;

      if (currentHead === 0) {
        return null; // Empty
      }

      const headNode = this.nodes[currentHead];
      const nextHead = headNode.next;

      const success = this.compareAndSwapHead(
        currentHead,
        nextHead
      );

      if (success) {
        return headNode.value;
      }
    }
  }

  private compareAndSwapHead(
    expected: number,
    newValue: number
  ): boolean {
    // Simplified CAS (not truly atomic in JS)
    if (this.head === expected) {
      this.head = newValue;
      return true;
    }
    return false;
  }
}

/**
 * Futex-like wait/wake
 */
function waitExample() {
  const sab = new SharedArrayBuffer(4);
  const view = new Int32Array(sab);

  // Worker thread
  const worker = new Worker('worker.js');
  worker.postMessage(sab);

  // Wait for value to change
  Atomics.wait(view, 0, 0);  // Wait if view[0] == 0
  console.log('Woken up!');
}

// In worker.js:
// Atomics.store(view, 0, 1);
// Atomics.notify(view, 0, 1);  // Wake one waiter

PHP: Mutex-Based Concurrency (No Native Atomics)

<?php

namespace Memory;

use Illuminate\Support\Facades\Cache;
use Illuminate\Support\Facades\Redis;

/**
 * Distributed lock using Redis
 */
class DistributedLock
{
    private string $key;
    private int $ttl;

    public function __construct(string $key, int $ttl = 10)
    {
        $this->key = "lock:{$key}";
        $this->ttl = $ttl;
    }

    public function acquire(): bool
    {
        // Redis SET with NX (only if not exists)
        return (bool) Redis::set(
            $this->key,
            getmypid(),
            'NX',
            'EX',
            $this->ttl
        );
    }

    public function release(): bool
    {
        // Only release if we own the lock
        $script = <<<'LUA'
            if redis.call("get", KEYS[1]) == ARGV[1] then
                return redis.call("del", KEYS[1])
            else
                return 0
            end
LUA;

        return (bool) Redis::eval(
            $script,
            1,
            $this->key,
            getmypid()
        );
    }

    public function withLock(callable $callback): mixed
    {
        $maxAttempts = 10;
        $attempt = 0;

        while (!$this->acquire()) {
            if (++$attempt >= $maxAttempts) {
                throw new \RuntimeException('Failed to acquire lock');
            }
            usleep(100000); // 100ms
        }

        try {
            return $callback();
        } finally {
            $this->release();
        }
    }
}

/**
 * Atomic counter using Redis
 */
class AtomicCounter
{
    private string $key;

    public function __construct(string $key)
    {
        $this->key = "counter:{$key}";
    }

    public function increment(): int
    {
        return Redis::incr($this->key);
    }

    public function decrement(): int
    {
        return Redis::decr($this->key);
    }

    public function add(int $delta): int
    {
        return Redis::incrby($this->key, $delta);
    }

    public function get(): int
    {
        return (int) Redis::get($this->key);
    }

    public function compareAndSet(int $expected, int $new): bool
    {
        $script = <<<'LUA'
            local current = tonumber(redis.call("get", KEYS[1]))
            if current == tonumber(ARGV[1]) then
                redis.call("set", KEYS[1], ARGV[2])
                return 1
            else
                return 0
            end
LUA;

        return (bool) Redis::eval(
            $script,
            1,
            $this->key,
            $expected,
            $new
        );
    }
}

/**
 * Read-write lock using Redis
 */
class ReadWriteLock
{
    private string $key;

    public function __construct(string $key)
    {
        $this->key = "rwlock:{$key}";
    }

    public function readLock(): bool
    {
        // Increment reader count
        return Redis::hincrby($this->key, 'readers', 1) > 0;
    }

    public function readUnlock(): void
    {
        Redis::hincrby($this->key, 'readers', -1);
    }

    public function writeLock(): bool
    {
        $maxAttempts = 100;

        for ($i = 0; $i < $maxAttempts; $i++) {
            $script = <<<'LUA'
                local readers = tonumber(redis.call("hget", KEYS[1], "readers") or "0")
                local writer = redis.call("hget", KEYS[1], "writer")

                if readers == 0 and not writer then
                    redis.call("hset", KEYS[1], "writer", ARGV[1])
                    return 1
                else
                    return 0
                end
LUA;

            $acquired = Redis::eval(
                $script,
                1,
                $this->key,
                getmypid()
            );

            if ($acquired) {
                return true;
            }

            usleep(10000); // 10ms
        }

        return false;
    }

    public function writeUnlock(): void
    {
        Redis::hdel($this->key, 'writer');
    }
}

Integration Points

With Consistency Models

Memory model ⊆ Consistency model: Memory model for shared memory, consistency for distributed
SC memory model = Linearizability: Both require total order

With Concurrency Primitives

Locks use memory barriers: Ensure critical section visibility
Lock-free uses atomics: Build on memory model guarantees

With Formal Verification

Model check memory models: Verify absence of data races
Litmus tests: Small programs testing memory model behaviors