Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hindsight theory, our work brings the formal rigor and proof machinery of concurrent program logics. We substantiate the usefulness of our development by verifying the linearizability of the Logical Ordering (LO-)tree and RDCSS. Both of these involve complex proof arguments due to future-dependent linearization points. The LO-tree additionally features complex structure overlays. Our proof of the LO-tree is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.

翻译：并发数据结构线性化性质的证明仍然是验证领域的关键挑战。我们提出时间插值作为一种新的证明原则，通过后见推理在并发分离逻辑中开展此类证明。时间推理提供了比预言变量更易用的替代方案，其优势在于能将证明结构化为易于证实的假设。本研究为后见理论引入了并发程序逻辑的形式化严谨性与证明机制。我们通过验证逻辑排序树（LO-tree）和RDCSS的线性化性质，证实了本方法的有用性。由于存在依赖于未来的线性化点，这两者都需要复杂的证明论证。LO-tree同时还具有复杂的结构覆盖特性。我们给出的LO-tree证明是首个针对该数据结构的正式证明。值得关注的是，我们的形式化工作揭示了此前未知的缺陷，并指出现有非形式化证明存在谬误。