如何通过模理论优化与程序语义的巧妙编码计算最坏情况执行时间

在具有硬实时约束的系统中，必须计算程序最坏情况执行时间（WCET）的上界；该上界越接近真实 WCET 越好。具有固定时钟的同步反应式控制回路尤其如此；回路体的 WCET 不得超过时钟周期。我们将 WCET（或至少是其接近的上界）作为优化模理论问题的解进行计算，该问题考虑了程序的语义，而其他方法则不论根据这些语义是否可行均计算最长路径。优化模理论将可满足性模理论（SMT）扩展至最大化问题。将 WCET 问题直接编码为 SMT 会产生对所有当前生产级求解器均难以处理的公式；这是这些求解器中实现的 SMT 的 DPLL(T) 方法所固有的。通过将这些公式与一些适当的“割”相结合，我们大幅减少了 SMT 求解器的计算时间。我们在多种控制程序上实验了我们的方法，将 OTAWA 分析器既作为基线又作为我们分析的底层微架构分析工具，并在多种基准测试和控制程序上展示了 WCET 界的显著改进。