Commutativity of program code (the equivalence of two code fragments composed in alternate orders) is of ongoing interest in many settings such as program verification, scalable concurrency, and security analysis. While some recent works have explored static analysis for code commutativity, few have specifically catered to heap-manipulating programs. We introduce an abstract domain in which commutativity synthesis or verification techniques can safely be performed on abstract mathematical models and, from those results, one can directly obtain commutativity conditions for concrete heap programs. This approach offloads challenges of concrete heap reasoning into the simpler abstract space. We show this reasoning supports framing and composition, and conclude with commutativity analysis of programs operating on example heap data structures. Our work has been mechanized in Coq and is available in the supplement.

翻译：程序代码的可交换性（即两个代码片段以不同顺序组合的等价性）在程序验证、可扩展并发性和安全性分析等诸多场景中持续受到关注。尽管近期已有研究探索针对代码可交换性的静态分析，但专门面向堆操作程序的研究仍较为有限。本文提出一种抽象域，使得可交换性综合或验证技术能够在抽象数学模型上安全执行，并可直接从这些结果中推导出具体堆程序的可交换性条件。该方法将具体堆推理的复杂性转移至更简洁的抽象空间。我们证明该推理机制支持框架化与组合性，并通过在典型堆数据结构上运行的程序进行可交换性分析作为总结。本项工作已在Coq中实现机械化，相关资源详见补充材料。