Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects
Putting Strong Linearizability in Context: Preserving Hyperproperties in Programs that Use Concurrent Objects
复制标题
将强线性化置于上下文中：在使用并发对象的程序中保留超属性
DOI：
10.4230/lipics.disc.2019.2
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
C. Enea
中科院分区：
文献类型：
--
作者：
H. Attiya;C. Enea
人们已经观察到，线性化，流行的一致性条件，实现并发对象，不保持一些概率分布。一个更强的条件，称为强线性化已经提出，但它的研究已经有点特设。本文研究了强线性化铸造它在观察细化的对象。我们提出了一个加强观测细化，概括强线性化，获得几个重要的影响。
当一个具体的并发对象细化另一个更抽象的对象时-通常是顺序的-使用具体对象的程序的正确性可以通过考虑它在使用更抽象对象时的行为来验证。这意味着使用具体对象的程序的跟踪特性可以通过考虑具有抽象对象的程序来证明。然而，这并不适用于超属性，包括许多安全属性和事件的概率分布。
我们定义强观测细化，加强细化，保持超性质，并证明它是等价的存在的前向模拟。我们发现，强观测细化推广强线性化。这意味着强线性化也等同于前向模拟，并且表明强线性化实现可以水平地（即，位置）和垂直（即，实例化）。
对于强线性实现不存在（或效率较低）的情况下，我们认为，推理程序的超属性可以简化的抽象对象，不一定是连续的强观测细化。
It has been observed that linearizability, the prevalent consistency condition for implementing concurrent objects, does not preserve some probability distributions. A stronger condition, called strong linearizability has been proposed, but its study has been somewhat ad-hoc. This paper investigates strong linearizability by casting it in the context of observational refinement of objects. We present a strengthening of observational refinement, which generalizes strong linearizability, obtaining several important implications.
When a concrete concurrent object refining another, more abstract object - often sequential - the correctness of a program employing the concrete object can be verified by considering its behaviors when using the more abstract object. This means that trace properties of a program using the concrete object can be proved by considering the program with the abstract object. This, however, does not hold for hyperproperties, including many security properties and probability distributions of events.
We define strong observational refinement, a strengthening of refinement that preserves hyperproperties, and prove that it is equivalent to the existence of forward simulations. We show that strong observational refinement generalizes strong linearizability. This implies that strong linearizability is also equivalent to forward simulation, and shows that strongly linearizable implementations can be composed both horizontally (i.e., locality) and vertically (i.e., with instantiation).
For situations where strongly linearizable implementations do not exist (or are less efficient), we argue that reasoning about hyperproperties of programs can be simplified by strong observational refinement of abstract objects that are not necessarily sequential.
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I