Chase-Lev deque is a concurrent data structure designed for efficient load balancing in multiprocessor scheduling. It employs a work-stealing strategy, where each thread possesses its own work-stealing deque to store tasks, and idle threads steal tasks from other threads. However, given the inherent risk of bugs in software, particularly in a multiprocessor environment, it is crucial to formally establish the correctness of programs and data structures. To our knowledge, no formal verification work for the Chase-Lev deque has met three key criteria: (1) utilizing a minimal trusted computing base, (2) using a realistic and unrestricted implementation, and (3) proving a strong specification.
In this thesis, we address this gap by presenting the formal verification of the Chase-Lev deque using a concurrent separation logic. Our work is mechanized in the Coq proof assistant, and our verified implementation is both realistic and unbounded in terms of the number of tasks it can handle. Also, we adopt linearizability as the specification, as it is widely recognized as a strong specification for concurrent data structures. Consequently, our work satisfies all three aforementioned criteria for formal verification. Additionally, we extend our verification to support safe memory reclamation, and provide a basis for verifying the Chase-Lev deque in the relaxed memory model.
Chase-Lev 덱은 멀티프로세서 스케줄링에서 효율적으로 부하를 분산시키는 데 사용되는 동시성 자료 구조이다. 이는 다음과 같은 작업 훔치기 기법을 지원한다. 각 스레드는 작업 저장소로서 Chase-Lev 덱을 하나씩 소유하고, 할 작업이 없어진 스레드는 다른 스레드의 작업 저장소로부터 작업을 훔쳐 대신 실행한다. 하지만 멀티프로세서 환경을 비롯한 모든 소프트웨어에서 버그의 위험이 내재되어 있기 때문에, 프로그램이나 자료 구조가 올바르게 동작함을 엄밀하게 증명하는 것이 중요하다. 현재까지 알려진 바로는 Chase-Lev 덱의 엄밀한 검증 연구 중 (1) 증명에서 믿고 넘어가야 하는 요소가 가능한 한 작고, (2) 현실적이면서 제약이 없는 구현을 사용하며, (3) 강한 명세를 증명한 사례는 없었다.
본 논문에서는 이러한 한계를 해결하기 위해 동시성 분리 논리를 사용하여 Chase-Lev 덱의 엄밀한 검증을 제시한다. 이 검증은 Coq 증명 보조 도구를 사용하여 작성되었으며, 검증된 구현은 현실적이면서 작업의 수에 제약이 없다. 또한 동시성 자료 구조의 강한 명세로 흔히 인정되는 선형화가능성(linearizability)을 명세로 사용한다. 따라서 본 연구의 검증은 위의 세 조건을 모두 충족한다. 추가로, 검증 작업을 확장하여 메모리 재활용 기법을 사용하는 구현을 검증하고, 느슨한 메모리 모델에서 Chase-Lev 덱을 검증하기 위한 토대를 마련하였다.
