检验对抗TSO的鲁棒性。
摘要：并发程序在总体存储排序(TSO)内存模型下的鲁棒性检查和强制执行算法。如果一个程序的所有TSO计算都对应于顺序一致性(SC)语义下的计算，则该程序具有鲁棒性。 我们提供了关于非鲁棒性的完整特征描述，即所谓的攻击：一种有限的(有害的)程序外执行顺序的形式。然后，我们展示了检测攻击的并行算法，并且可以通过SC语义下的状态可达性查询来解决，查询通过对线性规模的源到源转换的程序进行适当的仪表化获得。重要的是，该构造适用于任意数量的地址和并行线程，而且不依赖于数据域和TSO语义中存储缓冲区的大小。特别地，当数据域是有限的且地址数量是固定的时候，我们可以得到关于鲁棒性的可判定性和复杂性结果，即使线程数量是任意的。 作为第二个贡献，我们提供了一种计算优化的栅栏集合以实现鲁棒性的算法。我们考虑了两个最优性的标准：最小化程序大小和最大化性能。我们定义的算法已经实现，并且成功地应用于分析和修正多个并发算法。
作者：Ahmed Bouajjani, Egor Derevenetc, Roland Meyer
论文ID：1208.6152
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-10-30