동아시아 중세 논리로 동시성 불변식 재구성하기
Reconstructing Concurrency Invariants Through Medieval East Asian Logic
동시성 메모리 회수 문제를 11~14세기 동아시아의 구조적 논리로 재해석한다. 송·원대 수학의 배열 연산과 수송의 기계식 시계 장치에서 착안해, 포인터 가시성과 힙 자원 파괴를 분리하는 기호 체계를 제안한다. 공유 객체를 동시에 해제할 때 발생하는 이중 해제와 use-after-free를 막기 위한 네 가지 방법(건·곤·감·리)을 C11 atomic 코드로 구현하고, 건법이 정석임을 보인다.
건은 정법이고 곤은 측법이다. 대칭적 가시성 회수(건)는 동시 회수의 정석 불변식이다. 경로를 먼저 끊고, 동기화한 뒤, 해제하라.