Verified Lock-Free Session Channels with Linking

Type systems and program logics based on session types provide powerful high-level reasoning principles for message-passing concurrency. Modern versions employ bidirectional session channels that (1) are asynchronous so that send operations do not block, (2) have buffers in both directions so that both parties can send messages in parallel, and (3) feature a link operation (also called forward ) to concisely write programs in process style . These features complicate a low-level lock-free implementation of channels and therefore increase the gap between the meta theory of prior work—which is verified w.r.t. a high-level semantics of channels ( e.g ., <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi>π</mml:mi> </mml:math> -calculus)—and the code that runs on an actual computer. We address this problem by verifying a low-level lock-free implementation of session channels w.r.t. a high-level specification based on session types. We carry out our verification in a layered manner by employing the Iris framework for concurrent separation logic. We start with an abstract specification of (unidirectional) queues—of which we provide a linked-list and array-segment based implementation—and gradually build up to session channels with all of the aforementioned features. To make a layered verification possible we develop two logical abstractions— queues with ghost linking and pairing invariants —to reason about the atomicity and changing endpoints due to linking, respectively. All our results are mechanized in the Coq proof assistant.