BlockingQueues 的历史
计算机科学中的逻辑
2012-09-12 v1 软件工程
摘要
本文描述了一种形式化指定并发数据结构行为的方法。在指定并发数据结构时，主要挑战是使规约稳定，即确保它们不能被其他线程失效。为此，我们提出使用基于历史的规约：我们不根据对象的状态来描述方法行为，而是根据对象的状态历史来指定它。历史被定义为状态更新的列表，在所有时刻都可以与实际对象的状态相关联。我们在 java.util.concurrent 库中的 BlockingQueue 层次结构上说明了该方法。我们展示了如何指定 BlockingQueue 接口的行为，将一些决定留给后代类。实现该接口的类正确地继承了规约。作为规约语言，我们使用了 JML 和基于权限的分离逻辑（包括抽象谓词）的组合。这产生了一种抽象、模块化和自然的方式来指定并发队列的行为。这些规约可用于推导关于队列的高级属性，例如证明元素的顺序得到保留。此外，该方法可以很容易地适应其他并发数据结构。
引用
@article{arxiv.1209.2239,
title = {A History of BlockingQueues},
author = {Marina Zaharieva-Stojanovski and Marieke Huisman and Stefan Blom},
journal= {arXiv preprint arXiv:1209.2239},
year = {2012}
}
备注
In Proceedings FLACOS 2012, arXiv:1209.1699