Concurrent sets are a fundamental building block of various programs running on multithreaded systems. The most important concurrent set is Harris's list, a lock-free linked list that introduced many key ideas in concurrent set design. Such concurrency allows for highly performant programs, but it also introduces a much higher risk of bugs. Hence, it is important to formally verify the correctness of concurrent sets, in particular of Harris's list. However, there is no work on proving Harris's list that proved a strong specification, is foundational with a minimal trusted computing base, and properly handles memory reclamation at the same time. In this thesis, we present a formal verification of Harris's list in the concurrent separation logic Iris. We prove the linearizability of Harris's list, the de facto correctness criterion for concurrent data structures. All of our work is mechanized in the Coq proof assistant, providing a proof that is done with a minimal trusted computing base. Our implementation handles memory reclamation by utilizing RCU, a safe memory reclamation scheme that is widely used in concurrent data structures. Thus, this thesis presents the first proof of Harris's list that satisfied all of the aforementioned properties.
동시성 집합 자료 구조는 다양한 멀티프로세스 프로그램의 필수 요소이다. 이 중 대표격은 Harris 리스트로, 집합 디자인에 핵심적인 아이디어들을 여럿 제시했다. 동시성 집합을 사용하면 높은 성능을 보장받지만, 구현을 잘못하기 쉬워 버그 위험성이 커진다. 따라서 구현에 대한 엄밀한 검증이 필요하고, Harris 리스트 또한 검증 대상이다. 그러나, Harris 리스트의 증명 중, 강력한 명세를 증명하고, 믿고 넘어가는 요소가 최소한되고, 메모리 관리를 고려하는 증명을 모두 한 증명은 없었다. 본 논문은, 동시성 분리 논리를 사용한 Harris 리스트의 엄밀한 검증을 제시한다. 동시성 자료 구조의 강한 명세인 선형화가능성(linearizability)을 증명하고, Coq 증명 보조 도구를 사용을 해서 믿고 넘어가는 요소를 최소화한다. 또한, 검증한 구현은 메모리 관리를 위해 RCU 기법을 사용한다. 따라서 우리는 위 세 조건을 만족하는 Harris 리스트의 첫 검증을 완료했다.
