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 \textbf{send} operations do not block, (2) have buffers in both directions so that both parties can send messages in parallel, and (3) feature a \textbf{link} operation (also called \textbf{forward}) to concisely write programs in \emph{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. $\pi$-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 from (unidirectional) queues and gradually build up to session channels with all of the aforementioned features. To enable a layered verification we develop two generic logical abstractions – \emph{queues with ghost linking} and \emph{pairing invariants} – to reason about the atomicity and changing endpoints due to linking, respectively. All our results are mechanized in the Coq proof assistant.