We observe that the standard notion of thread fairness is insufficient for guaranteeing termination of even the simplest shared-memory programs under weak memory models. Guaranteeing termination requires additional model-specific fairness constraints, which we call memory fairness. In the case of acyclic declarative memory models, such as TSO and RA, we show that memory fairness can be equivalently expressed in a uniform fashion as prefix-finiteness of an extended coherence order. This uniform memory fairness representation yields the first effective way for proving termination of spinloops under weak memory consistency.
翻译:我们认为,标准线条公平概念不足以保证即使是最简单的共享记忆模式下最简单的共同记忆程序也终止。 保证终止要求额外的模式性公平约束,我们称之为记忆公平。 在诸如TSO和RA等循环声明性记忆模式中,我们表明记忆公平可以以统一的方式表示为扩展一致性命令的前缀。 这种统一的记忆公平性代表提供了证明在记忆一致性薄弱的情况下终止脊椎的第一个有效方法。