符号模型检测中静态变量排序的带宽与波前缩减

我们展示了带宽与波前缩减算法在静态变量排序中的适用性。在符号模型检测中，事件局部性在时间和内存使用方面起着重要作用。例如，在佩特里网中，事件局部性可通过依赖矩阵捕获，其中非零项指示一个变迁是否修改一个库所。事件局部性的质量已被表达为一个称为（加权）事件跨度（event span）的度量。矩阵的带宽是一个指示非零元素到对角线距离的度量。波前是一个指示矩阵对角线一端非零元素程度的度量。带宽和波前是稀疏矩阵求解器中使用的经过充分研究的度量。在这项工作中，我们证明跨度受限于矩阵带宽的两倍。这一观察使得带宽缩减算法可用于获取良好的变量序。我们解决的一个主要问题是，缩减算法只能应用于对称矩阵，而依赖矩阵是非对称的。我们展示了在邻接图的全图上执行的Sloan算法给出了最佳的变量序。实际上，我们展示了我们的工作允许调用Boost和ViennaCL中的标准稀疏矩阵操作，在毫秒内计算出非常好的静态变量序。未来的工作前景广阔，因为包括元启发式算法在内的全新范围的更多现成算法可用于变量排序。