Mazurkiewicz trace

独立字母的同余 ​

给定有限字母表 $\mathrm{\Sigma }$ 与独立关系

$$I\subseteq \mathrm{\Sigma }\times \mathrm{\Sigma },$$

要求 $I$ 对称且反自反。依赖关系为 $D=(\mathrm{\Sigma }\times \mathrm{\Sigma })\setminus I$。若 $(a,b)\in I$，允许相邻交换

$$uabv{\equiv }_{I}ubav.$$

由这些交换生成的最小同余 ${\equiv }_I$ 把有限词分成等价类。一个 Mazurkiewicz trace 是类 $[w{]}_I$，trace monoid 为

$$M(\mathrm{\Sigma },I)={\mathrm{\Sigma }}^{\ast }/{\equiv }_I.$$

这里的 trace 不是普通动作序列公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。本身，而是许多序列的商类；同一个类保留依赖事件次序，遗忘独立事件的任意线性排列。

三事件实例 ​

设 $a$ 属于线程 P，$b$ 属于线程 Q，二者独立；$c$ 读取两者共同结果，故依赖于 $a,b$。词

$$abc,bac$$

通过交换相邻独立的 $a,b$ 等价。$acb$ 不等价，因为把 $c$ 越过 $b$ 会交换依赖动作。

该 trace 的因果偏序有 $a<c$、$b<c$，而 $a,b$ 不可比。两个等价词正是这个偏序的两个线性扩展。

若实现中 $a,b$ 实际竞争同一锁，它们不应列入 $I$；错误独立关系会把可能产生不同状态的执行合并。

交换序列不仅保持最终状态，还需保持沿途动作使能。若 $a$ 执行后使 $b$ 暂时失效，即使某个特殊初态两种完整次序偶然同终点，它们也不满足稳定独立关系。trace 理论的字母独立通常是全局静态假设；状态依赖交换需更精细 event structure 或动态 POR。

动作标签过粗也会制造假独立。两个 write 标签访问不同地址时可交换，访问同一地址时不可交换；只用操作名作字母表无法同时准确表达两种情况，可把地址纳入事件标签或保守视为依赖。

dependence graph 表示 ​

对词 $w=a_1\cdots a_n$，为每个事件位置建节点；若 $i<j$ 且 $(a_i,a_j)\in D$，加入次序边，再取传递约简可得 dependence graph。

两个词属于同一 trace，当且仅当其带标签依赖偏序同构。图表示避免枚举等价类中可能阶乘多的线性词，并直接展示哪些事件必须先后。

相同字母的不同出现是不同事件节点。由于 $I$ 反自反，同一动作标签的两次出现彼此依赖，原先顺序不会被商掉。

trace prefix 可定义为偏序的下闭事件集（ideal）：若事件被保留，它的全部因果前驱也必须保留。随意从 dependence graph 中删除一个中间原因、保留后继，不对应合法执行前缀。

两个线性词的普通字符串前缀可能不同，却代表同一 trace prefix。例如 $ab$ 与 $ba$ 在 $aIb$ 时都完成同一两个事件 ideal；基于字面前缀缓存会重复探索它们。

Foata normal form ​

一个 trace 可分成并发层

$$C_1{C}_2\cdots C_k,$$

每层 $C_i$ 内动作两两独立，且后层每个动作与前一层至少一个动作依赖。这给出 Foata normal form 的一种规范并行表示。

对上例，第一层可为 $\{a,b\}$，第二层为 $\{c\}$。层数反映在无限处理器和单位动作时间假设下的关键路径深度，不等于真实运行时间。

若动作带不同持续时间、资源限制或概率，简单并发层不再给出调度成本；trace monoid 只编码交换关系。

与偏序约简的接口 ​

偏序约简公理库偏序约简Partial-order reduction · POR · Ample-set reduction利用独立并发动作的可交换性只探索等价交错代表，并以 proviso 保存死锁与时序性质。尝试从每个相关 Mazurkiewicz trace 中探索至少一个代表。sleep set、persistent set 和 DPOR 用不同方式避免重复线性化。

保存终态对独立确定动作较直接，保存中间可见状态、死锁和 liveness 还需附加条件。商类相同不自动表示所有时序公式都无法区分其中线性化。

动态执行中独立性可能依地址和状态变化，需用 event-specific dependence；固定字母关系是干净理论模型，但可能过粗或不可靠。

trace language 与闭包 ​

若一个词语言 $L\subseteq {\mathrm{\Sigma }}^{\ast }$ 在 ${\equiv }_I$ 下闭合，即 $w\in L$ 且 $w{\equiv }_{I}v$ 推出 $v\in L$，它才能被视为 trace 集合的良定义性质。只接受某个线性化、拒绝同类其他线性化的监控条件显然观察了独立动作顺序，不应在商空间上判断。

例如“$a$ 必须在 $b$ 前”若 $(a,b)\in I$ 就不是 trace-closed；把它当并发性质会与独立关系自相矛盾。要么把 $a,b$ 改为依赖，要么承认性质需要更细观察。

无限 Mazurkiewicz traces 还需处理事件偏序的局部有限性和无限线性化。有限词商的结论不能无条件覆盖 fairness 或无限发散路径。

局部有限性要求每个事件只有有限多个因果前驱，使某个线性执行能在有限位置安排它。允许一个事件依赖无限过去却仍声称“最终发生”，会得到没有实际线性化见证的偏序对象。

公平性也不是 trace 类自动属性：有限事件交换保持偏序，但无限执行中某个持续可用事件是否永远被推迟，需要额外的无限行为条件。

算法表示边界 ​

dependence graph 的传递约简在并发度高时紧凑，但构造仍需为每个新事件连接最近的依赖前驱。若简单给所有早先依赖事件加边，语义正确却可能产生二次空间；若只按相同线程连边，又会漏跨线程冲突。

规范形比较可判定两个有限词是否同 trace，但若独立关系来自求解器动态判断，规范化结果还需绑定当时的地址与状态条件，不能跨执行无条件复用。

参考资料

• Antoni Mazurkiewicz, “Trace Theory,” in Petri Nets: Applications and Relationships to Other Models of Concurrency, Springer, 1987, pp. 278–324。
• Volker Diekert and Grzegorz Rozenberg, eds., The Book of Traces, World Scientific, 1995, Chs. 1–3。
• Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems, Springer, 1996, Chs. 2–4。