公理记忆模型的可移植性分析。PORTHOS：适用于所有型号的工具
Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models
摘要：
我们介绍Porthos，第一个发现性能关键代码中移植错误的工具。Porthos将一个程序和源架构的内存模型作为输入，该程序是为源架构开发的，目标模型是移植的。如果代码是不可移植的，Porthos会以意外执行的形式找到一个bug--一个与目标一致但与源内存模型不一致的执行。在技术上，Porthos实现了一个有界模型检验方法，将可移植性分析问题简化为可满足性模理论（SMT）。有两个主要的问题，我们提出了新的和有效的解决方案减少。首先，可移植性问题的表述包含一个量词交替（一致+不一致）。我们引入一个公式，编码在一个单一的存在查询。其次，支持的内存模型（例如，Power）包含递归定义。我们在SMT中有效地计算递归所需的最小不动点语义（在[47]中未解决的问题）。最后，我们提出了从TSO到Power的可移植性的第一个实验分析。
英文摘要：
We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, Porthos finds a bug in the form of an unexpected execution - an execution that is consistent with the target but inconsistent with the source memory model. Technically, Porthos implements a bounded model checking method that reduces the portability analysis problem to satisfiability modulo theories (SMT). There are two main problems in the reduction that we present novel and efficient solutions for. First, the formulation of the portability problem contains a quantifier alternation (consistent + inconsistent). We introduce a formula that encodes both in a single existential query. Second, the supported memory models (e.g., Power) contain recursive definitions. We compute the required least fixed point semantics for recursion (a problem that was left open in [47]) efficiently in SMT. Finally we present the first experimental analysis of portability from TSO to Power.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
