Lean으로 Skia 2D 래스터화 형식 의미론 μSkia 구현, 크롬의 비효율 명령 패턴 4가지 최적화로 18.7% 속도 향상
- μSkia는 Skia 2D 그래픽 라이브러리의 형식 의미론으로, 캔버스 상태와 레이어 스택, 블렌딩, 컬러 필터를 다루며 의미론을 세 계층으로 나눠 확장 가능하게 만들고 Lean으로 기계화함
- 구글 크롬이 상위 100개 방문 사이트에서도 비효율적인 Skia 명령 시퀀스를 생성한다는 점을 확인하고 하위 최적화 패턴 4가지를 규명해 각 패턴의 대체 코드를 작성한 뒤 Lean으로 정확성을 검증함
- 상위 100개 사이트에서 모은 Skia 프로그램 99개에 최적화기를 적용해 Skia 최신 GPU 백엔드 대비 18.7% 속도 향상을 얻었고, 최적화에 걸리는 시간은 최대 32μs임
- 최적화기가 만든 트레이스를 다시 μSkia 의미론에 로드해 Lean에서 변환을 검증하는 종단 간 검증을 수행했으며, 여러 웹사이트와 Skia 백엔드, GPU에서 속도 향상이 유지됨
- 저자는 Bhargav Kulkarni, Henry Whiting, Pavel Panchekha이고 논문은 23페이지, 그림 15개임
Hacker News opinions
Skia에 기여했던 사람인데 이거 진짜 반갑다. 예전에 SkRecord 만들 때 노린 게 딱 이런 최적화였고 nanobench까지 써줘서 기쁘네. 그때는 불필요한 saveLayer() 호출 없애는 정도가 전부였는데, Lean으로 제대로 하는 걸 보니 좋다.
SkRecord 덕분에 가능했음. 그 시스템 없었으면 이 프로젝트 자체가 안 됐을 거다.
논문 1저자인데 좋게 봐줘서 고맙다. Skia 코드베이스가 빌드하기 쉬워서 정말 편했고, nanobench 소스 읽으면서 성능 벤치마킹을 많이 배웠음.
게임에도 같은 걸 할 수 있을까? 요즘 게임들이 GPU에 얼마나 쓸데없는 작업을 던지는지 궁금하다.
게임 쪽엔 괴담 같은 얘기가 많지. 모든 리벳마다 천 폴리곤짜리 나사 모델을 쓴다든가, 배 모형을 1%로 줄여서 병 안에 넣는다든가. 해결책은 보통 그냥 안 하는 거임.
게임에도 비슷한 형식 분석을 붙일 수 있다고 본다. 다만 깊이와 지각이 들어가서 훨씬 복잡함. 웹브라우저 2D 래스터화엔 없는 문제다. 대상은 씬 그래프가 될 텐데, 이걸 카메라 기준으로 2D로 줄이는 게 Skia 때보다 훨씬 어렵다.
DBus 역직렬화에 비슷한 걸 해본 적 있다. 배열에 고정점 루프 최적화를 적용한 셈인데 JVM이 한다는 얘기랑 비슷하더라. 과설계라는 소리도 들었지만 결과물은 꽤 쓸만했음. 공짜 성능 점심이 끝나면서 이런 작업이 더 늘어날 듯.
내 GPU 라이브러리에선 푸시 상수가 몇 프레임 안 바뀌면 백그라운드에서 전처리기로 그걸 걷어낸 셰이더를 컴파일한다. 분기 예측기 같은 느낌임. 파이프라인 전체를 그래프로 저장해서 커널 합치기와 쪼개기도 하려고 했는데 아직 못 했다. GPU 프로그램엔 전체 프로그램을 아는 런타임이 없어서 컴파일러식 최적화가 어렵다는 게 문제다.
맞는 말임. GPU 프로그램엔 컴파일러식 최적화에 필요한 정보가 없어서 추상화 수준을 잘 고르는 게 중요하다. 컴파일러도 어셈블리는 거의 안 건드리고, 최적화에 필요한 정보를 담도록 설계한 IR에서 작업한다.
DB 쿼리 최적화를 배우면서 왜 다른 계산 영역엔 이런 게 없나 싶었는데 진짜 흥미롭다. 앞뒤 상황을 많이 알수록 단계 순서를 더 잘 바꿀 수 있다. DB가 관계 대수 위에 서 있듯 형식 모델이 있어야 어떤 편집이 가능한지 알 수 있고, 그럼 수동 최적화는 AI로 넘어갈 듯. 옛날식 AI부터 말이다.
내 커리어 대부분이 이 주제다. browser.engineering 쓰면서 렌더링 명령 최적화 아이디어를 몇 년 전에 떠올렸는데, 어려운 부분은 Skia 의미론을 정확히 잡는 거였다. 그럴듯하지만 불투명하거나 블렌드 모드가 맞거나 두 개가 안 겹칠 때만 맞는 재작성 규칙을 쓰기란 아주 쉽다. 그래서 Lean으로 의미론을 잡았고, 안 그러면 올바른 규칙을 일관되게 못 썼다.
많은 계산 과정을 작은 프로그래밍 언어로 캐스팅할 수 있다는 말이 맞다. DB 쿼리 쪽은 논문이 많지만 그래픽은 드물어서 재밌었다. 논문 관련 연구 마지막 문단에 여러 그래픽과 제조 영역에서 같은 시도를 한 논문 목록이 있다. 여기선 옛날식 AI가 주역이다. Lean 증명 상당수는 grind라는 증명 탐색이 처리하고, 실패하면 LLM이 로그를 읽고 빠진 정리를 찾아낸다.
마지막 저자인데 HN에 뜬 걸 보고 놀랐다. 스키아 팀이 여러 번 만나서 설명해줄 만큼 많이 도와줬다. Chris Harrelson과 Web Browser Engineering을 쓰면서 몇 년 전에 아이디어를 냈고, 몇 년 전 Yuvaraj랑 한 번 시도했다가 별 성과 없이 접고 1년 전 Bhargav랑 다시 시작했다. 의미론에 집중하니 진도가 확 빨라지더라. 결과가 이렇게 좋을 줄은 솔직히 놀랐다.
크롬이 이걸 도입하거나 비효율적인 Skia 명령을 내보내는 C++ 코드를 고치면 크롬 성능이 어떻게 바뀔지 궁금하다.
크롬 쪽이랑 얘기했고 관심은 있는데 어려운 작업이다. 크롬이 너무 커서 명령 시퀀스를 바꾸려면 내부 추상화를 많이 손봐야 한다. Skia도 이런 최적화를 하고 싶어 하지만 팀이 작고 우선순위가 밀려 있다. 외부 코드 통합도 쉽지 않다.