This is a summary of the group meeting on 31 March 2021

Semantic Program Alignment for Equivalence Checking

解决的问题：

对于同一个函数或程序，经过不同编译器或者手动，针对loop部分优化得到的代码，是否还是相同的。这里的相同（equivalence）是指：两个函数，在相同输入的情况下，能够有两种情况：1）都能够正常终止，并得到相同的输出；或2）都运行失败，即都无限循环/出现错误。

解决方法：

对于两个待验证其相等性的函数，将其在用户给定的test case中运行，得到相应的concrete execution trace，论文的主要思路就是寻找一种semantic 的方法，找到两个trace的相关关系，并对齐，得到pairs of traces，进而构建product program。

核心：

1. 首先获取alignment predicate（invariant），并运用这个predicate来获取两个函数execution trace的相关关系（pairs of traces），接着运用pairs of traces来构建product program。
2. 得到product program之后，利用一些现有的技术，对其进行learn candidate invariants，最后通过证明这个product program的proof obligations即可证明两个函数的相等性。

算法大致流程

实验：

1. 能够对论文提出的56个benchmarks（包含多个feature），验证其中的55个，最后一个不能被验证的原因是SMT solver超时。（论文中设定以assembly为输入）
2. 能够对经过手动优化的函数成功验证。

问题：

• 什么是CPU hour？ 程序跑满一个CPU的一个小时所用的CPU开销。
• 什么是Loop fusion？ 循环融合是一种将两个或多个循环组合成一个循环的编程技术，遵循编程效率或编译器优化的原则。
• 什么是Loop tiling？ Loop tiling是提高数据局部性最重要的优化之一，其本质是在外层循环挖掘内层的时间和空间复用性。Loop tiling可以将循环的迭代空间划分为更小的块，以帮助确保循环中使用的数据在重用之前一直保存在缓存中。循环迭代空间的划分导致将大数组划分为更小的块，从而将被访问的数组元素匹配到缓存大小中，增强缓存重用，消除缓存大小需求。

Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis

本文的主要目的是更有效率的验证基于ReLU的神经网络，方法是通过一种叫做依赖分析的技术。本文发现，神经网络中存在一种依赖关系，即若知道一个ReLU节点的激活状态，可以推导出另一个ReLU节点的激活状态。所以依据ReLU节点之间的依赖关系，从而可以修剪神经网络基于MILP的验证问题需要考虑的搜索树，提升验证效率。

Questions:

1）随着求解的进行，添加进求解器约束越来越多，且找到cut这个公式也需要时间，会对时间有什么影响吗？

作者文中提到因为找约束也会占用一定的时间，所以为了平衡，不是每个节点都会添加约束，而是选择性的在一些节点来进行添加约束。

2）这个依赖的效果怎么样？

文中的实验说明还是能提升一些效率的。