Site Tools


trace-monoid

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
trace-monoid.md · Last modified: by 127.0.0.1