| 이번 쇼앤텔 시간에서는 2020년 PLDI에 발표했던 동형암호 회로 최적화기 Lobster의 작동원리를 간단하게 소개하고, 이후에는 동일식 탐색(equality saturation)기술을 덧붙여 Lobster의 성능을 한단계 더 끌어올린 새로운 성과를 소개하고자 합니다. 기존의 전통적인 프로그램 최적화는 주로 수동으로 유용한 최적화 규칙들을 디자인한 뒤 프로그램에 적용하는 식으로 이루어집니다. 상식적인 방법이지만 사람이 유용한 최적화 규칙을 쉽사리 고안해내기 힘든 저수준 언어(예: 논리식 회로, 어셈블리 등등)를 전통적인 방식으로 최적화하려면 유용한 최적화 규칙을 고안해내기 힘든 단점이 있습니다. Lobster는 이러한 전통적인 틀에서 벗어나 최적화 규칙의 생성을 프로그램 합성 기술로 자동으로 해내는데, 저수준 언어에 대해 사람이 생각하기 힘든 복잡한 최적화 규칙들을 발굴해내는 경우가 많습니다. 이렇게 학습한 '좋은' 최적화 규칙들은 식 다시쓰기(term rewriting)기술을 통해 최적화에 유용하게 사용될 수 있었고, 25개의 벤치마크 동형암호 프로그램에 대해 2배 이상의 성능향상을 관측할 수 있었습니다. 또한 올해에는 식 다시쓰기 대신 동일식 탐색 기술을 도입하여 기존보다 더 큰 폭의 성능향상을 이끌어내는데 성공하였습니다. 이번 쇼앤텔 시간에 이 일련의 과정에 대해 보다 자세하게 소개하고자 합니다. |