一句话：提出首个完全验证指令调度的机械化证明库，将证明负担降到交换相邻独立指令的语义保持。
CompCert 不支持完全验证的指令调度，已有工作多采用翻译验证，只能事后检查每次编译结果，无法证明调度算法本身正确，并带来编译期验证开销。本文利用拓扑排序列表的拓扑重排等价于交换相邻无序元素这一性质，结合语义模拟关系的传递性，将语义保持证明归结为证明块内交换相邻独立指令保持语义。由此，证明新调度算法正确只需证明其保持语法级依赖，而无需重复推理语义细节。作者基于 CompCert 库在 Coq 中实现该机械化证明框架，并以列表调度算法为案例完成正确性证明，且将外部调度启发式抽象为参数，修改启发式不影响证明。
CompCert project, the state-of-the-art compiler that achieves the first end-to-end formally verified C compiler, does not support fully verified instruction scheduling. Instead, existing research that works on such topics only implements translation validation. This means they do not have direct formal proof that the scheduling algorithm is correct, but only a posterior validation to check each compiling case. Using such a method, CompCert accepts a valid C program and compiles correctly only when the untrusted scheduler generates a correct result. However, it does not guarantee the complete correctness of the scheduler. It also causes compile-time validation overhead in the view of runtime performance. In this work, we present the first achievement in developing a mechanized library for fully verified instruction scheduling while keeping the proof workload acceptably lightweight. The idea to reduce the proof length is to exploit a simple property that the topological reordering of a topological sorted list is equal to a sequence of swapping adjacent unordered elements. Together with the transitivity of semantic simulation relation, the only burden will become proving the semantic preservation of a transition that only swaps two adjacent independent instructions inside one block. After successfully proving this result, proving the correctness of any new instruction scheduling algorithm only requires proof that it preserved the syntax-level dependence among instructions, instead of reasoning about semantics details every time. We implemented a mechanized library of such methods in the Coq proof assistant based on CompCert’s library as a framework and used the list scheduling algorithm as a case study to show the correctness can be formally proved using our theory. We show that with our method that abstracts away the semantics details, it is flexible to implement any scheduler that reorders instructions with little extra proof burden. Our scheduler in the case study also abstracts away the outside scheduling heuristic as a universal parameter so it is flexible to modify without touching any correctness proof.