컴파일러의 부동소수점 최적화 검증을 위한 효율적인 SMT 인코딩

Abstract

부동소수점 값을 추상화한 비트벡터와 연산을 추상화한 SMT 수식을 이용해 컴파일러 최적화를 빠르고 정확하게 검증하는 방법을 소개하고, 실험을 통해 효용성을 확인한다. IEEE-754 부동소수점 표준에 정의된 다수의 부동소수점 연산을 머신러닝 애플리케이션 최적화 검증에 사용할 수 있을 정도로 정확하게 상위 근사 (overapproximation) 하는 방법을 고안하였다. 추상화된 연산은 표준 부동소수점 연산에 비해 절대적인 연산 횟수도 적고 SMT solver가 더욱 효율적으로 검증할 수 있다. 머신러닝 컴파일러 프레임워크인 MLIR에서 사용되는 최적화를 표준 부동소수점 연산을 그대로 재현하는 방법과 제시하는 방법으로 검증해 비교했다. 동일한 최적화를 약 14배 더 빠르게 검증했고 timeout이 줄어들며 더 많은 최적화를 검증하였다. 이 과정에서 잘못 구현된 MLIR 최적화를 발견해 제보하였고 현재는 제거되었다.

This paper introduces a novel method to encode the floating-point (FP) value as SMT bit-vector and the operations between them as SMT formulas, which allows efficient yet accurate verification of FP compiler optimizations, and checks its effectiveness by experiments. It is essentially an overapproximation scheme for FP operations, which is less complex and more SMT-friendly compared to the IEEE-754 standard but maintains enough representative power for verification. When verifying the optimization passes from MLIR compiler framework using both abstract and concrete FP encoding, the abstract encoding could verify the same optimizations more quickly, and even allowed more passes to be verified than the concrete encoding due to less timeouts. The new encoding played a crucial role in removing some faulty MLIR optimizations.