닫기
Loading..

전자정보연구정보센터 ICT 융합 전문연구정보의 집대성

EIRIC 세미나

국내외의 전자정보 분야 연구자들이 학술정보 또는 연구와 관련된 교육 콘텐츠를 무료로 접할 수 있는 온라인 세미나입니다.

화상회의시스템을 활용하여 소규모 세미나, 워크숍 등 목적에 따라 다양하게 활용할 수 있습니다.

Webinar

홈 홈 > EIRIC 광장 > EIRIC 세미나
컴퓨터 전자/전기 통신 AI
LLVM 컴파일러 안정성 향상을 위한 이론 및 도구 개발
  • 일시2021년 11월 4일 (목) 오후 4시
  • 연사허충길 교수서울대학교 컴퓨터공학부
  • 약력PDF
개최완료
세미나 개요

산업계에서 가장 많이 쓰이는 컴파일러 중 하나인 LLVM 컴파일러의 안정성 향상을 위해 서울대 소프트웨어 원리 연구실에서 그동안 연구해온 내용을 전반적으로 소개한다.
첫번째는 LLVM 컴파일러의 중간 언어인 LLVM IR에 있는 undef 및 poison 값에 관한 문제를 발견하고 이를 해결하기 위해 freeze라는 명령어를 제안하여 공식적으로 LLVM에 채택되었다 (PLDI'17).
두번째는 정수와 포인터 간 변환에 숨어있던 문제를 해결하고 이에 기반하여 엄밀한 LLVM IR의 실행의미를 정의하였다 (OOPSLA'18).
마지막으로는 이렇게 개발한 이론에 기반하여 컴파일러 최적화 전후 프로그램의 오류가 있는지 자동으로 확인해주는 Alive2 번역 검증기를 개발하였다 (PLDI'21, CAV'21).

Alive2는 컴파일러 실행 중 생성된 최적화 전후 프로그램들의 실행의미 및 이들의 동등함을 수식으로 표현한 후, 마이크로소프트의 자동수식검증기(SMT solver)인 Z3를 사용해 최적화의 올바름을 보이거나, 그렇지 않으면 오류를 찾아낸다.
이때 핵심기술은 프로그램의 복잡한 실행의미를 SMT solver가 쉽게 풀 수 있는 형태로 효율적으로 표현하는 것이다.
SMT solver는 수학적으로 엄밀하게 수식의 참/거짓을 체크하기 때문에, Alive2는 오탐(False Alarm)이 거의 없고 테스팅으로는 찾을 수 없는 오류들을 찾아낼 수 있다.
Alive2의 온라인 서비스(https://alive2.llvm.org)는 현재 LLVM 커뮤니티의 코드 리뷰 단계에서 개발자들에 의해 활발하게 사용되고 있다.

우수성과 보기 >>

동영상

댓글(0)