BlockingQueues的历史
A History of BlockingQueues
摘要：
本文描述了一种形式化描述并发数据结构行为的方法。当指定并发数据结构时，主要的挑战是使规范稳定，即，以确保它们不会被其他线程无效。为此，我们建议使用基于历史的规范：而不是描述方法行为的对象的状态，我们指定它在对象的状态历史。历史被定义为状态更新的列表，它在所有点上都可以与实际对象的状态相关。我们在java.util.concurrent库中的BlockingQueue层次结构上演示了该方法。我们将展示如何指定接口BlockingQueue的行为，并将一些决定留给后代类。实现接口的类正确地继承了规范。作为一种规约语言，我们使用JML和基于权限的分离逻辑的组合，包括抽象谓词。这导致了一种抽象、模块化和自然的方式来指定并发队列的行为。这些规范可用于派生有关队列的高级属性，例如，显示元素的顺序被保留。此外，该方法可以很容易地适用于其他并发数据结构。
英文摘要：
This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
