Rust 비동기 런타임의 모듈형 응답성 검증

비동기(async) 프로그래밍은 동시성을 관리하는 인기 있는 패러다임입니다. 비동기 지원을 제공하는 언어들은 일반적으로 비동기 실행을 관리하기 위한 런타임을 갖습니다. 이러한 런타임은 핵심 인프라스트럭처이지만, 이를 검증하는 것은 상대적으로 주목받지 못했습니다. 한 가지 이유는 사용자들이 비동기 런타임에서 가장 중요하게 생각하는 속성이 '활성(liveness)' 속성이라는 점입니다. 즉, 런타임에 제출된 작업들이 결국 진전한다는 것입니다. 활성을 검증하는 것은 동시적이고 고도로 최적화된 라이브러리에게는 어려운 일입니다. 본 논문에서는 Rust 비동기 런타임의 궁극적인 진행 보장(eventual progression guarantees)을 검증하기 위한 경량의 모듈형 증명 기법을 제시합니다. 우리는 이 기술을 Rust와 Rust의 비동기 모델에 기반한 간단한 언어의 맥락에서 설명합니다. 그런 다음, 이 증명 기술을 Rust를 위한 일련의 정적 분석(static analyses)으로 구현하고, 이를 사용하여 여러 Rust 비동기 런타임 구현의 몇 가지 핵심 구성 요소들의 궁극적인 진행을 검증합니다.