허충길 교수 연구진, 소프트웨어 검증 기술로 세계 선도
허충길 교수 연구진, 소프트웨어 검증 기술로 세계 선도
- LLVM 컴파일러 최적화 자동 검증기 Alive2 개발로 컴파일러 검증 기술 선도
- 최신 동시성 메모리모델 개발로 동시성 P/G 개발 및 검증 위한 기반기술 선도
허충길 교수 연구진이 마이크로소프트 연구소 및 유타 대학교와 공동으로 LLVM 컴파일러 최적화를 자동으로 검증하는 프레임워크인 Alive2를 개발하였다.
Alive2는 컴파일러 실행 중 생성된 최적화 전후 프로그램들의 실행의미 및 이들의 동등함을 수식으로 표현한 후, 마이크로소프트의 자동수식검증기(SMT solver)인 Z3를 사용해 최적화의 올바름을 보이거나, 그렇지 않으면 오류를 찾아낸다. 이때 핵심기술은 프로그램의 복잡한 실행의미를 SMT solver가 쉽게 풀 수 있는 형태로 효율적으로 표현하는 것이다. SMT solver는 수학적으로 엄밀하게 수식의 참/거짓을 체크하기 때문에, Alive2는 오탐(False Alarm)이 거의 없고 테스팅으로는 찾을 수 없는 오류들을 찾아낼 수 있다. 실제로 Alive2는 지금까지 테스팅으로서는 발견할 수 없었던 수십개의 컴파일러 버그를 발견하였으며, Alive2의 온라인 서비스(https://alive2.llvm.org) 는 현재 LLVM 커뮤니티의 코드 리뷰 단계에서 개발자들에 의해 활발하게 사용되고 있다.
"Alive2: Bounded Translation Validation for LLVM.", Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr.
허충길 교수 연구진이 이스라엘 Tel Aviv 대학과 공동으로, 기존의 동시성 메모리 모델들이 만족하지 못했지만 개발자들이 실질적으로 가정하고 있는 성질인 부분적 무경쟁 보장(Modular Data-Race-Freedom Guarantees)을 만족하는 메모리 모델을 최초로 개발하였다.
부분적 무경쟁 보장은 데이터 경쟁(Data Race)이 일어나지 않는 (부분적인) 메모리 영역에서는 동시성으로 인한 느슨한 행동(Relaxed behavior)이 나타나지 않음을 보장하는 것이다. 연구진은 우선 현실에서 그러한 보장을 깨는 특수한 반례를 찾아내어 엄밀하게는 그 보장이 성립하지 않음을 보인 후, 성능에 크게 영향을 미치지 않는 작은 컴파일러 최적화인 RMW-store reordering을 금지하는 것으로 이 문제를 해결할 수 있음을 보였다. 이를 엄밀하게 보이기 위해 허충길 교수 연구진에서 개발해오고 있는 메모리 모델인 Promising Semantics를 개선한 PS2.1을 개발하였고, 이 모델에서 RMW-store reordering은 성립하지 않지만 부분적 무경쟁 보장은 성립함을 Coq 증명보조도구를 사용해 컴퓨터로 증명하였다.
"Modular Data-Race-Freedom Guarantees in the Promising Semantics.", Minki Cho, Sung-Hwan Lee, Chung-Kil Hur, Ori Lahav.
위 논문 2편은 오는 6월 PLDI(Programming Language Design and Implementation) 2021에 발표될 예정이다.