We present a formal framework for proving the correctness of set implementations backed by binary-search-tree (BST) and linked lists, which are often difficult to prove correct using automation. This is because many concurrent set implementations admit non-local linearization points for their `contains' procedure. We demonstrate this framework by applying it to the Contention-Friendly Binary-Search Tree algorithm of Crain et al. We took care to structure our framework in a way that can be easily translated into input for model-checking tools such as TLA+, with the aim of using a computer to verify bounded versions of claims that we later proved manually. Although this approach does not provide complete proof (i.e., does not constitute full verification), it allows checking the reasonableness of the claims before spending effort constructing a complete proof. This is similar to the test-driven development methodology, that has proven very beneficial in the software engineering community. We used this approach and validated many of the invariants and properties of the Contention-Friendly algorithm using TLA+. It proved beneficial, as it helped us avoid spending time trying to prove incorrect claims. In one example, TLA+ flagged a fundamental error in one of our core definitions. We corrected the definition (and the dependant proofs), based on the problematic scenario TLA+ provided as a counter-example. Finally, we provide a complete, manual, proof of the correctness of the Contention-Friendly algorithm, based on the definitions and proofs of our two-tiered framework.

翻译：我们提出了一个形式化框架，用于验证由二叉搜索树（BST）和链表支持的集合实现的正确性，这类实现通常难以通过自动化方法证明其正确性。其原因在于许多并发集合实现的"包含"操作允许非局域线性化点。我们通过将该框架应用于Crain等人的竞争友好型二叉搜索树算法来展示其有效性。我们特别注重框架的结构设计，使其能够方便地转化为TLA+等模型检查工具的输入，旨在通过计算机验证后续手工证明的有界版本声明。尽管该方法不提供完备证明（即不构成完整验证），但能在投入精力构建完整证明前检验声明的合理性。这类似于软件工程领域已被证明卓有成效的测试驱动开发方法论。我们采用此方法，并利用TLA+验证了竞争友好型算法的众多不变性和性质。实践证明此方法卓有成效，帮助避免了将时间浪费在尝试证明错误声明上。例如，TLA+曾标记了我们核心定义中的一个根本性错误。基于TLA+作为反例提供的矛盾场景，我们修正了该定义（以及依赖该定义的证明）。最终，我们基于双层框架的定义与证明，提供了竞争友好型算法正确性的完整手工证明。