Table of Contents

Trace monoid

Trace monoid is an algebraic structure capturing concurrent computation—sequences of actions where swapping independent actions (those with no shared data) doesn't change the result. It's a partial order of instructions formalized as an equivalence class under commutativity of independent pairs, the algebraic foundation for analyzing concurrent program semantics.

Example

// Two independent instruction chains can commute:
// mov eax, 1      (a: write eax)
// mov ebx, 2      (b: write ebx) — independent of (a)
// add ecx, eax    (c: read eax written by a)
// add edx, ebx    (d: read ebx written by b) — independent of (c)
// Trace: {abcd, bacd, abdc, badc} all have same observable result