代码变更差异成本计算技术解析
修改计算机代码可能会对程序性能产生意外影响。例如,修改特定程序中的循环或数据结构可能导致执行时间、内存或磁盘使用量增加。我们将此类性能指标的变化称为代码修改的差异成本。这种分析代码变更成本的能力被称为差异成本分析。
差异成本分析以执行时间、内存或磁盘使用等性能指标来衡量代码变更的成本。但界定代码变更成本是一个不可判定问题,意味着没有算法能保证给出答案。先前的方法要么专注于估算单一版本代码的成本,要么假设能够以语法方式对齐代码变更。
在今年的ACM SIGPLAN编程语言设计与实现会议(PLDI 2022)上,我们提出了一种克服这些挑战的差异成本分析方法。该方法基于联合计算势函数和反势函数的思想,分别提供成本变化的上界和下界。
技术实现
与先前方法不同,我们的实现能够计算从文献中收集的程序版本对之间代码变更成本的严格边界。具体而言,在19个示例中的14个上提供了严格边界,这些示例既包含影响成本的变体,也包含不影响成本但需要复杂分析验证的变体。
我们重点研究具有整数变量和多项式运算的命令式程序(最熟悉的程序类型,明确指定每个计算步骤)。程序可能还包含非确定性元素,即相同输入可能产生不同输出。
反势函数(计算下界)捕获程序运行需"支付"的最小成本。如果用ϕ表示程序的势函数,用χ表示其反势函数,则程序新旧版本间成本变化的阈值可通过ϕ_new - χ_old近似。
约束求解
该方法的关键在于为新程序版本的势函数和旧程序版本的反势函数同时建立约束系统。通过将程序版本表示为转移系统(一种由程序状态集和状态间有效转移集组成的计算模型),并假设转移系统会终止(即不存在导致无限运行的输入),我们固定阈值t的符号变量,通过遍历两个转移系统获得可求解的约束系统。
最终约束系统因涉及全称量词和变量上的多项式约束而难以求解。我们利用Handelman定理的结果将这些约束转换为纯存在量化的线性约束系统,这种约束表示还能支持符号阈值的验证或具体阈值的优化,从而得到尽可能严格的阈值t。
验证结果
在19个C语言基准测试中,17个能够计算阈值,其中14个案例获得最优阈值,所有案例的阈值计算时间均低于5秒。该方法尤其适用于需要严格控制内存和处理能力的设备环境,可为开发者提供每次代码变更的自动化成本反馈。