根据TSO检查稳健性
Checking Robustness against TSO
摘要：
我们提出的算法检查和执行的并发程序对总存储排序（TSO）内存模型的鲁棒性。一个程序是健壮的，如果它的所有TSO计算对应于顺序一致性（SC）语义下的计算。我们提供了一个完整的非鲁棒性的特征，在所谓的攻击：（有害的）程序的顺序执行的限制形式。然后，我们发现，检测攻击可以并行化，并可以解决SC语义下使用状态可达性查询在一个适当的仪表程序获得的线性大小的源到源的翻译。重要的是，该构造对于任意数量的地址和任意数量的并行线程都是有效的，并且它独立于数据域和TSO语义中的存储缓冲区的大小。特别是，当数据域是有限的，地址的数量是固定的，我们得到的鲁棒性的可判定性和复杂性的结果，即使是任意数量的线程。作为第二个贡献，我们提供了一个算法来计算一组最佳的围栏，执行鲁棒性。我们考虑两个标准的最优性：最小化的程序大小和最大化的性能。我们定义的算法被实现，并成功地应用于分析和纠正几个并发算法。
英文摘要：
We present algorithms for checking and enforcing robustness of concurrent programs against the Total Store Ordering (TSO) memory model. A program is robust if all its TSO computations correspond to computations under the Sequential Consistency (SC) semantics. We provide a complete characterization of non-robustness in terms of so-called attacks: a restricted form of (harmful) out-of-program-order executions. Then, we show that detecting attacks can be parallelized, and can be solved using state reachability queries under SC semantics in a suitably instrumented program obtained by a linear size source-to-source translation. Importantly, the construction is valid for an arbitrary number of addresses and an arbitrary number of parallel threads, and it is independent from the data domain and from the size of store buffers in the TSO semantics. In particular, when the data domain is finite and the number of addresses is fixed, we obtain decidability and complexity results for robustness, even for an arbitrary number of threads. As a second contribution, we provide an algorithm for computing an optimal set of fences that enforce robustness. We consider two criteria of optimality: minimization of program size and maximization of its performance. The algorithms we define are implemented, and we successfully applied them to analyzing and correcting several concurrent algorithms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
