[Blog] Minor edits for readability

Author: Re-st

_posts/2025-06-29-geon-trip-pldi.md

@@ -49,15 +49,19 @@ Lean은 뉴로심볼릭 AI 개발의 핵심 도구로도 활용되고 있다. 
 # 우리 연구의 최전선: 정적 분석(Static Analysis) 분야 탐구
 정적 분석의 이론과 응용의 대가들이 한자리에 모인 SOAP (State Of the Art in Program Analysis) 워크샵에 간 건 큰 행운이었다. 개중 인공신경망의 안전성을 따지기 위한 정적 분석 (?)과, 실용적 정적 분석을 위한 기술 개발이 특히 인상적이었다.
 ## Static Analysis from Code Graphs to Neural Networks - Experiences and Opportunities<sup>[3](#static)</sup>
-신경망이 작은 입력 변화 (perturbation)에도 예기치 않게 반응하는 취약성을 해결하기 위한 수학적 검증 기법을 소개했다. 핵심은 주어진 입력 $$x$$에 대해, 그 근방 $$||x'-x||\le \epsilon$$의 모든 입력 $$x'$$에서도 출력 레이블이 항상 같음을 보장하고자 하는 것이다. 이 문제를 해결하기 위해, 전체 입력 공간을 잘게 나누는 branch-and-bound 방식이 사용되었다. 입력 공간을 나눈 (branch) 뒤, 각 부분공간의 출력 범위를 근사치로 계산 (bound)해, 이 범위가 모두 같은 라벨을 가리키면 해당 영역은 안전하다고 판정한다. 그렇지 않으면 반례를 찾거나 더 세분화해 더 정밀한 검사를 반복한다. 최근 발표에서는 이때 반례가 존재할 가능성이 높은 순서대로 공간을 탐색해 효율성을 높이는 전략도 제시되었다.
+신경망이 작은 입력 변화 (perturbation)에도 예기치 않게 반응하는 취약성을 해결하기 위한 수학적 검증 기법을 소개했다. 핵심은 주어진 입력 $$x$$에 대해, 그 근방 $$||x'-x||\le \epsilon$$의 모든 입력 $$x'$$에서도 출력 레이블이 항상 같음을 보장하고자 하는 것이다.
+
+여기에는 전체 입력 공간을 잘게 나누는 branch-and-bound 방식이 사용되었다. 입력 공간을 나눈 (branch) 뒤, 각 부분공간의 출력 범위를 근사치로 계산 (bound)해, 이 범위가 모두 같은 라벨을 가리키면 해당 영역은 안전하다고 판정한다. 그렇지 않으면 반례를 찾거나 더 세분화해 더 정밀한 검사를 반복한다. 최근 발표에서는 이때 반례가 존재할 가능성이 높은 순서대로 공간을 탐색해 효율성을 높이는 전략도 제시되었다.
 
 이미 알던 정적분석, 즉 요약 해석 (abstract interpretation)을 기반으로 하고 갈루아 연결 (Galois connection)을 이론적 바탕으로 가지던 정적분석이 아니라서 흥미를 끌었다. 반례의 위치를 찾아내는 기술은 실수 집합 내에서 유계 수열은 수렴하는 부분 수열을 가진다는 Bolzano-Weierstrass 정리의 증명 과정과 유사했다. 
 ## Building X-Ray for enterprise-scale software<sup>[4](#xray)</sup>
 Beacon을 개발한 홍콩과기대 Charles Zhang 교수님의 발표는, 대규모 기업용 (엔터프라이즈) 소프트웨어에 정적 분석을 적용하려는 다년간의 연구 성과를 집약한 세션이었다. 교수님은 안전성 (soundness)은 현실 환경에선 지나치게 보수적이고, 정확도 (precision)는 높이기 어려운 상황에서, 경량화된 경로 민감 (path-sensitive) 분석을 효율적으로 수행하는 방법을 모색해 왔다.
 
 특히 인상 깊었던 개념은 '경계 문제 (boundary problem)'였다. 이는 정적 분석이나 대형 언어 모델(LLM) 단독으로는 다루기 어려운, 불완전한 코드, 깊은 반복문, 불명확한 API 사용 등을 말한다. 교수님 연구팀은 이러한 문제를 정적 분석과 LLM의 역할 분담을 통해 해결하려고 한다. 예를 들어, 제어/데이터 흐름 추적과 도달성 분석은 정적 분석이 맡고, API 별명 (alias) 관계 추론이나 의미 기반 함수 해석은 LLM이 담당하는 식이다.
 
-사례로는, 공식 문서를 바탕으로 클래스 계층, 모듈타입 (signature), 설명, 값 이름 등을 비교해 API 간의 별명 관계를 추론하는 연구, 정적 분석으로 인터럽트 핸들러 (ISR) 함수를 식별한 뒤 LLM이 데드락 가능성을 검토하는 연구, 그리고 메모리 할당/해제 함수를 감싸 기능을 추가하는 메모리 감쌈 (wrapper) 함수를 찾는 구조가 소개되었다. 이 중 마지막은 함수 이름을 통한 추론을 LLM이, 도달성 분석 등을 정적 분석이 맡는 방식이다. 우리 연구실에서도 메모리 감쌈 함수를 찾거나, 공식 문서를 참고하는 유사한 주제를 생각하고 있었기에, 
+사례로는, 공식 문서를 바탕으로 클래스 계층, 모듈타입 (signature), 설명, 값 이름 등을 비교해 API 간의 별명 관계를 추론하는 연구, 정적 분석으로 인터럽트 핸들러 (ISR) 함수를 식별한 뒤 LLM이 데드락 가능성을 검토하는 연구, 그리고 메모리 할당/해제 함수를 감싸 기능을 추가하는 메모리 감쌈 (wrapper) 함수를 찾는 구조가 소개되었다. 이 중 마지막은 함수 이름을 통한 추론을 LLM이, 도달성 분석 등을 정적 분석이 맡는 방식이다.
+
+우리 연구실에서도 메모리 감쌈 함수를 찾거나, 공식 문서를 참고하는 유사한 주제를 생각하고 있었기에, 
 연사님께 해당 연구의 연구 목적을 여쭤보았다. 메모리 감쌈 함수를 찾는 이유는, sanitizing 과정에서 일어나는 실수나 double free 같은 결함이 자주 발생하는 지점이기 때문에 분석 우선순위를 높이기 위함이라고 한다. 
 우리 연구실의 접근 목적과는 다르지만, 연구 자체는 유사하며, 우리가 진행하는 논의가 세계적인 수준과 맞닿아 있다는 사실을 실감할 수 있었다.
 
@@ -72,7 +76,9 @@ KAT 세션이 따로 있을 만큼 이번 PLDI에서 주목받았지만, 세션
 
 이 오토마타의 핵심은 상태를 단순한 집합이 아니라 중복집합으로 표현한다는 점이다. 오토마타 위를 탐험하는 행위자 (agent)들은 확률 상태에서는 무작위로 다음 상태를 선택하고, 비결정 상태에서는 여러 행위자로 분기해 각각 독립적으로 실행되도록 한다. 동일한 확률 상태에 서로 다른 경로로 도달한 여러 행위자가 존재할 수 있는데, 이들을 집합의 한 원소로 표현하면 각각의 확률 선택이 독립적이지 않게 되어 문제가 된다. 중복집합을 사용하면 행위자들을 구분할 수 있어, 각기 다른 난수 (random bit)를 부여해 확률 선택의 독립성을 보장할 수 있다.
 
-이렇게 가능한 모든 실행 경로를 다 따져볼 수 있는 방식이 ‘천사적 비결정론 (angelic nondeterminism)’이다. 모든 실행 경로를 다 따져보기 때문에 `if`, `while` 같은 조건 분기를 모델링하는 데 적합하다. 다만 발표에서 아쉬웠던 점은, 천사적 비결정론을 이용해 KAT의 주요 활용 분야인 최적화 검증이나 프로그램 분석이 어떻게 가능한지를 잘 상상하기 어려웠다는 것이다. 또한 천사적 비결정론을 검색해 보면, 비결정론이 항상 원하는 결과에 도달하도록 눈치껏 작동하는 실행이라고 나오는데, 그것과 발표의 정의가 일치하는지도 궁금했다. 발표장에서도 '천사적 선택'이 위험하지 않은지, 어디에 쓰일 수 있는지 질문이 나왔지만, 아직 활용 분야를 개척하진 않았고 실제 프로그램에 적용하기 위해 개발 중이라는 답이 돌아왔다.
+이렇게 가능한 모든 실행 경로를 다 따져볼 수 있는 방식이 ‘천사적 비결정론 (angelic nondeterminism)’이다. 모든 실행 경로를 다 따져보기 때문에 `if`, `while` 같은 조건 분기를 모델링하는 데 적합하다.
+
+다만 발표에서 아쉬웠던 점은, 천사적 비결정론을 이용해 KAT의 주요 활용 분야인 최적화 검증이나 프로그램 분석이 어떻게 가능한지를 잘 상상하기 어려웠다는 것이다. 또한 천사적 비결정론을 검색해 보면, 비결정론이 항상 원하는 결과에 도달하도록 눈치껏 작동하는 실행이라고 나오는데, 그것과 발표의 정의가 일치하는지도 궁금했다. 발표장에서도 '천사적 선택'이 위험하지 않은지, 어디에 쓰일 수 있는지 질문이 나왔지만, 아직 활용 분야를 개척하진 않았고 실제 프로그램에 적용하기 위해 개발 중이라는 답이 돌아왔다.
 
 한편, 이 세션은 구문 중심 코드에 대해 어떤 대수적 접근이 가능한지를 알 수 있게 해주었고, 그 배경에 예상보다 높은 수학적 난도가 있다는 점을 체감할 좋은 기회였다. KAT는 함수 호출이 없는 절차적 프로그램에 적합하므로 일반적인 언어에는 적용이 어렵지만, 제어 흐름을 다루는 새로운 방식이 흥미로웠다.
 ## PL + HCI
@@ -105,11 +111,13 @@ KAT 세션이 따로 있을 만큼 이번 PLDI에서 주목받았지만, 세션
 ### Verifying Lock-Free Traversals in Relaxed Memory Separation Logic<sup>[8](#lockfree)</sup>
 느슨한 메모리 (relaxed memory), 다른 말로 약한 메모리 (weak memory)는 컴파일러 및 하드웨어의 최적화로 인해 명령어가 재배열되는 것을 허용하는 메모리 모델로, 동시성 프로그램에서 가능한 다양한 실행 순서를 모두 안전하게 포함해야 한다. 이 모델의 핵심 특징은, 메모리에서 값을 읽을 때 반드시 가장 최근 값이 아니라 예전에 기록된 값을 읽을 수 있다는 가능성을 허용하는 점이다.
 
-스킵리스트 (skiplist)는 기본적으로 인접 노드만 가리키는 연결 리스트 (linked list)에 여러 층의 도약 포인터를 추가해 탐색 속도를 높인 자료구조다. 특정 노드를 삭제하려면 그 노드를 가리키는 모든 포인터를 비활성화해야 하는데, 여기에 여러 스레드가 동시에 접근하고, 명령어 재배열까지 가능한 환경이라면 어떤 실행이 안전하며 어떤 실행이 오류를 유발할 수 있는지 정형적으로 검증하기가 매우 까다롭다. 이 연구는 스킵리스트 위에서의 락 안쓰는 (lock-free) 탐색 알고리즘을 약한 메모리 모델 위에서 최초로 각잡힌 검증 (formal verification)한 사례이다. 2024년 여름 SIGPL에서 "약한 메모리에서 동시성 탐색 알고리즘 검증하기"라는 이름으로 미리 소개된 바 있었는데, 이렇게 멋진 발표로 다시 볼 수 있어서 매우 좋았다.
+스킵리스트 (skiplist)는 기본적으로 인접 노드만 가리키는 연결 리스트 (linked list)에 여러 층의 도약 포인터를 추가해 탐색 속도를 높인 자료구조다. 특정 노드를 삭제하려면 그 노드를 가리키는 모든 포인터를 비활성화해야 하는데, 여기에 여러 스레드가 동시에 접근하고, 명령어 재배열까지 가능한 환경이라면 어떤 실행이 안전하며 어떤 실행이 오류를 유발할 수 있는지 정형적으로 검증하기가 매우 까다롭다.
+
+이 연구는 스킵리스트 위에서의 락 안쓰는 (lock-free) 탐색 알고리즘을 약한 메모리 모델 위에서 최초로 각잡힌 검증 (formal verification)한 사례이다. 2024년 여름 SIGPL에서 "약한 메모리에서 동시성 탐색 알고리즘 검증하기"라는 이름으로 미리 소개된 바 있었는데, 이렇게 멋진 발표로 다시 볼 수 있어서 매우 좋았다.
 ### Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic<sup>[9](#rcu)</sup>
 RCU (read-copy-update)는 동시성 환경에서 데이터를 읽을 때 락을 쓰지 않아, 읽기 성능이 최적화된 동기화 방식이다. 읽고 싶으면 그냥 읽으면 되고, 쓰고 싶을 때는 기존 데이터의 복사본을 만들어 수정한 뒤, 포인터만 한 번에 바꿔치면 된다. 다만 원본 데이터를 해제하기 전에, 이전 데이터를 아직 읽고 있는 스레드가 있다면 그게 끝날 때까지 기다려야 한다. 흡사 참조 횟수 (reference counter)처럼 자신을 참조하는 스레드를 추적하는 방식으로 메모리 안전성을 보장하는 연구들이 있었지만, 이는 순차적 메모리 (sequential memory) 모델에서만 가능했다.
 
-느슨한 메모리에서 RCU를 각잡힌 검증하기 위해, 다음 두 가지 가정을 도입했다. 첫째, 한 스레드가 메모리의 이전 값과 현재 값을 동시에 참조하고 있을 경우, 이전 값의 참조는 무시할 수 있다. 둘째, 뮤텍스와 같은 공유 자원을 한 스레드에서 쓰고 다른 스레드에서 읽는다면, 그 중간에 메모리 장벽 (fence)을 삽입해 접근 순서를 보장한다. 이 두 가정만으로도 느슨한 메모리에서의 RCU를 각잡힌 검증할 수 있다는 것이 이 연구의 핵심이다.
+이 연구는 느슨한 메모리에서 RCU를 각잡힌 검증하기 위해, 다음 두 가지 가정을 도입했다. 첫째, 한 스레드가 메모리의 이전 값과 현재 값을 동시에 참조하고 있을 경우, 이전 값의 참조는 무시할 수 있다. 둘째, 뮤텍스와 같은 공유 자원을 한 스레드에서 쓰고 다른 스레드에서 읽는다면, 그 중간에 메모리 장벽 (fence)을 삽입해 접근 순서를 보장한다. 이 두 가정만으로도 느슨한 메모리에서의 RCU를 각잡힌 검증할 수 있다는 것이 이 연구의 핵심이다.
 
 간단하고 명쾌한 아이디어처럼 보이지만, 실제로는 복잡한 사례 연구 (case study)에 기반해 가능함을 입증한 점에서 매우 잘 된 연구라고 느꼈다. 발표 중 누군가 "왜 이런 간단하고 중요한 아이디어를 그전까지 아무도 하지 않았던 거냐"고 묻자, 발표자는 "단순한 아이디어처럼 보이지만 그 아래엔 아주 복잡한 사례 분석이 있었다"고 답했던 게 정말 인상적이었다.
 
@@ -132,9 +140,12 @@ PL 학회였기 때문일까. 평소에 궁금했지만 멀게 느껴졌던 프
 그런 사용법이 너무 새로웠기에 이해를 못 해서 들어온 질문이 있었다. '악마적 선택은 뭔지 아는데, 연구에서 굳이 천사적
 선택을 쓸 이유는?' 내지는 '응용 분야가 있는지' 등, 주제가 많이 새로운 발표들에서는 잘 모르겠는 걸 거리낌없이 질문할 수 있는 분위기였다.
 
-모두들 자신의 분야를 전혀 모르는 남들에게 이해시키기 위해 많은 노력을 기울였다. 가장 놀랐던 점은 발표에서 나오는 핵심 예제 
-(motivating example)가 논문과 겹치지 않는 새로운 경우가 많았단 것이다. 논문에서는 상대적으로 길고 엄밀한 에제를 
-썼다면 발표에서는 그다지 엄밀하진 않지만 어떤 분야의 어느 내용을 바꾸었는지 이해하기 좋은 비유를 들고 왔다. 
+모두들 자신의 분야를 전혀 모르는 남들에게 이해시키기 위해 많은 노력을 기울였다.
+
+가장 놀랐던 점은 발표에서 나오는 핵심 예제 (motivating example)가 논문과 겹치지 않는 새로운 경우가 많았단 것이다. 
+논문에서는 상대적으로 길고 엄밀한 에제를 썼다면 
+발표에서는 그다지 엄밀하진 않지만 어떤 분야의 어느 내용을 바꾸었는지 이해하기 좋은 비유를 들고 왔다. 
+
 또한 소프트웨어 엔지니어링처럼 성능을 끌어올린 연구를 하더라도 그 결과를 앞에 놓지 않고, 최대한 자신의 연구 분야와 
 현황을 예제 등으로 주지시킨 다음에 결과를 실었다. 이건 아무래도 서로 어떤 연구를 하는지 쉽게 알기 어려운 학회의 특성상, 
 얻어갈 핵심 메시지를 어떻게든 가르치려 노력한 산물이었다. 
@@ -163,4 +174,4 @@ PL 학회였기 때문일까. 평소에 궁금했지만 멀게 느껴졌던 프
 
 <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
 <script id="MathJax-script" async
-  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
+  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>