Sequentially consistent versus linearizable counting networks

We compare the impact of timing conditions on implementing sequentially consistent and linearizable counters using (uniform) counting networks in distributed systems. For counting problems in application domains which do not require linearizability but will run correctly if only sequential consistency is provided, the results of our investigation, and their potential payoffs, are threefold: First, we show that sequential consistency and linearizability cannot be distinguished by the timing conditions previously considered in the context of counting networks; thus, in contexts where these constraints apply, it is possible to rely on the stronger semantics of linearizability, which simplifies proofs and enhances compositionality. Second, we identify local timing conditions that support sequential consistency but not linearizability; thus, we suggest weaker, easily implementable timing conditions that are likely to be sufficient in many applications. Third, we show that any kind of synchronization that is too weak to support even sequential consistency may violate it significantly for some counting networks; hence, we identify timing conditions that are to be totally ruled out for specific applications that rely critically on either sequential consistency or linearizability. A preliminary version of this work appears in the Proceedings of the 18th annual ACM symposium on principles of distributed computing (PODC 1999), pp. 133–142, May 1999. This work has been partially supported by the IST Program of the European Union under projects DELIS (contract number 001907) and AEOLUS (contract number 15964).     

Decidability of linearizabilities for relaxed data structures

Many recent implementations of concurrent data structures relaxed their linearizability requirements for better performance and scalability. Quasi-linearizability, k-linearizability and regular-relaxed linearizability are three quantitative relaxation variants of linearizability that have been proposed as correctness conditions of relaxed data structures, yet preserving the intuition of linearizability. Quasi-linearizability has been proved undecidable. In this paper, we first show that k-linearizability is undecidable for a bounded number of processes, by reducing quasi-linearizability into it. We then show that regular-relaxed linearizability is decidable for a bounded number of processes. We also find that the number of the states of a relaxed specification is exponential to the number of the states of the underlying specification automaton (representing its relaxation strategy), and polynomial to the number of the states of the underlying quantitative sequential specification and the number of operations.     

Integrating Runtime Consistency Models for Distributed Computing

How should distributed systems preserve consistency in the presence of concurrency and failures? For systems designed as assemblies of independently developed components, concurrent access to data or data structures would normally arise within individual programs, and be controlled using mutual exclusion constructs, such as semaphores and monitors. Where data is persistent and/or sets of operations are related to one another, transactions or linearizability may be more appropriate. Systems that incorporate cooperative styles of distributed execution often replicate or distribute data within groups of components. In these cases, group-oriented consistency properties must be maintained, and tools based on the virtual synchrony execution model greatly simplify the task confronting an application developer. All three styles of distributed computing are likely to be seen in future systems-often, within the same application. This leads us to propose an integrated approach that permits applications that use virtual synchrony to interact with concurrent objects that respect a linearizability constraint, and vice versa. Transactional subsystems are treated as a special case of linearizability.     

TSO内存模型下限界可线性化的可判定性研究

TSO-to-TSO可线性化、TSO-to-SC可线性化和TSO可线性化是Total Store Order（简称TSO）内存模型下可线性化的三个变种。在本文中我们提出了?-限界TSO-to-TSO可线性化和?-限界TSO可线性化,考察了?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题。它们分别是这三种可线性化的限界版本,都使用?-扩展历史,这样的扩展历史对应的执行有着限界数目（不超过?个）的函数调用、函数返回、调用刷出和返回刷出动作。?-扩展历史对应执行中的写动作数目是不限界的,进而执行中使用的存储缓冲区的大小也是不限界的,对应的操作语义是无穷状态迁移系统,所以三个限界版本可线性化的验证问题是不平凡的。 我们将定义在并发数据结构与顺序规约之间的?-限界TSO-to-TSO可线性化、?-限界TSO-to-SC可线性化和?-限界TSO可线性化的验证问题归约到?-扩展历史集合之间的TSO-to-TSO可线性化问题,从而以统一的方式验证了TSO内存模型下可线性化的三个限界版本。验证方法的关键步骤是判定一个并发数据结构是否有一个特定的?-扩展历史。我们证明了这个问题是可判定的,证明方法是将这一问题归约为已知可判定的易失通道机器的控制状态可达问题。本质上,这一归约将每一个函数调用或函数返回动作转化为写、刷出或cas（compare-and-swap）动作。在TSO-to-TSO可线性化的定义中,一个函数调用或函数返回动作会同时影响存储缓冲区和控制状态。为了模拟函数调用或函数返回动作对存储缓冲区的影响,我们在每个函数调用或函数返回动作之后立刻执行一个特定的写动作。这个写动作及其对应的刷出动作模拟了函数调用或函数返回动作对存储缓冲区的影响。我们引入观察者进程,为每个函数调用或函数返回动作“绑定”一个观察者进程的cas动作,以这种方式模拟了函数调用或函数返回动作对控制状态的影响。因此,我们证明了TSO内存模型下可线性化的这三个限界版本都是可判定的。我们进而证明了在TSO内存模型下判定可线性化的这三个限界版本的复杂度都在递归函数的Fast-Growing层级中。我们通过证明已知对应复杂度的单通道简单通道机器的可达问题和TSO内存模型下可线性化的三个限界版本可以互相归约得到这个结论。     

Long-lived Rambo: Trading knowledge for communication

Shareable data services providing consistency guarantees, such as atomicity (linearizability), make building distributed systems easier. However, combining linearizability with efficiency in practical algorithms is difficult. A reconfigurable linearizable data service, called Rambo, was developed by Lynch and Shvartsman. This service guarantees consistency under dynamic conditions involving asynchrony, message loss, node crashes, and new node arrivals. The specification of the original algorithm is given at an abstract level aimed at concise presentation and formal reasoning about correctness. The algorithm propagates information by means of gossip messages. If the service is in use for a long time, the size and the number of gossip messages may grow without bound. This paper presents a consistent data service for long-lived objects that improves on Rambo in two ways: it includes an incremental communication protocol and a leave service. The new protocol takes advantage of the local knowledge, and carefully manages the size of messages by removing redundant information, while the leave service allows the nodes to leave the system gracefully. The new algorithm is formally proved correct by forward simulation using levels of abstraction. An experimental implementation of the system was developed for networks-of-workstations. The paper also includes selected analytical and preliminary empirical results that illustrate the advantages of the new algorithm.     

Using refinement calculus techniques to prove linearizability

Stepwise refinement is a method for systematically transforming a high-level program into an efficiently executable one. A sequence of successively refined programs can also serve as a correctness proof, which makes different mechanisms in the program explicit. We present rules for refinement of multi-threaded shared-variable concurrent programs. We apply our rules to the problem of verifying linearizability of concurrent objects, that are accessed by an unbounded number of concurrent threads. Linearizability is an established correctness criterion for concurrent objects, which states that the effect of each method execution can be considered to occur atomically at some point in time between its invocation and response. We show how linearizability can be expressed in terms of our refinement relation, and present rules for establishing this refinement relation between programs by a sequence of local transformations of method bodies. Contributions include strengthenings of previous techniques for atomicity refinement, as well as an absorption rule, which is particularly suitable for reasoning about concurrent algorithms that implement atomic operations. We illustrate the application of the refinement rules by proving linearizability of Treiber’s concurrent stack algorithm and Michael and Scott’s concurrent queue algorithm.     

Exploiting parallelism in deterministic shared memory multiprocessing

Multi-threaded programs on shared-memory hardware tend to be non-deterministic, which brings challenges to software debugging and testing. Current deterministic implementations eliminate nondeterminism of multi-threaded programs by trading much parallelism for determinism, which leads to low performance. Researchers typically improve parallelism by weakening determinism or introducing weak memory consistency models. However, weak determinism cannot deal with non-determinism caused by data races which are very common in multi-threaded programs. Weak memory consistency models impact the productivity of programming and may bring correctness problems of legacy programs. To address the problems, this paper presents a fully parallelized deterministic runtime, FPDet, which exploits parallelism of deterministic multi-threaded programs by preserving strong determinism and sequential memory consistency. FPDet creates a Working Set Memory (WSM) for each thread to make threads run independently for parallelism. FPDet guarantees determinism by redistributing memory blocks among threads’ WSMs in specified synchronization points. As a result, FPDet obtains parallelism and determinism simultaneously. To further exploit parallelism, we propose an Adaptive Budget Adjustment (ABA) mechanism to minimize wait time caused by thread synchronization.     

Data-race and concurrent-write freedom are undecidable

In a distributed shared memory system, sequential consistency is often assumed as the model for the memory, because it is a natural extension from multitasking in uniprocessor systems. Weaker consistency models allow greater concurrency, but programming is harder, because programs may produce unexpected results.Data-race-free (DRF) and concurrent-write-free (CWF) programs have the same set of possible executions both under a sequentially consistent memory and under some other, weaker model, memories. They can be written for a sequential memory and run unchanged under such a weaker-model memory. Since the sets of possible executions are the same, the run will only produce results that are possible under sequential consistency.This article proves the undecidability of both classes of concurrent programs in a language with if statements, loops, barriers, dynamic process creation, dynamic storage, and recursive data structures, under many models weaker than sequential consistency. Moreover, the article also proves that methods that only add synchronization statements to programs written for sequential consistency must produce some conservatively DRF or CWF programs.     

Implementing sequentially consistent programs on processor consistent platforms

Designers of distributed algorithms typically assume strong memory consistency guarantees, but system implementations provide weaker guarantees for better performance and scalability. This motivates the study of how to implement programs designed for sequential consistency on platforms with weaker consistency models. Typically, such implementations are impossible using only read and write operations to shared variables. One variant of processor consistency originally proposed by Goodman and called here PC-G is an exception because it provides just enough consistency to implement mutual exclusion using only reads and writes. This paper investigates the existence of compilers to convert arbitrary programs that use shared read/write variables with sequentially consistent memory semantics, to programs that use read/write variables with PC-G consistency semantics. We first provide a simple program transformation, and prove that it correctly compiles any 2-process program to a PC-G memory system, while preserving wait-freedom. We next prove that even a substantial generalization of this transformation cannot be a compiler for even a very restricted class of 3-process programs. Even though our program transformation is not a general compiler for three or more processes, it does correctly transform some specific n-process programs. In particular, for the special case of the (necessarily randomized) Test&Set algorithm of Tromp and Vitanyi, our transformation extends to any number of processes, thus providing the first algorithm for expected wait-free Test&Set on any weak memory system, using only read/write variables.     

Geometric properties of linearizable control systems

In this paper the distributions associated with a non-linear system of the form $$\frac{{dx}}{{dt}} = f(x) + \sum\limits_{\alpha = 1}^m {u_\alpha (t)g_\alpha (x)} ,f(0) = 0andx \in U_0 \subset R^n$$ are studied in relation to nonlinear state feedback $$u(x,v) = \hat a(x) + \hat S(x)v$$ withâ, u, v ∈ R ^m and ? a nonsingularm×m matrix withâ, ? functions ofx. Bothf andg are vector fields onU ₀, generally assumed to be real analytic. Two nested families of distributions {G ^j } and {M ^j } associated with the system are examined with emphasis on generic points ofU ₀, where it is shown that the usual conditions for feedback linearizability contain some redundancy. A characterization of state linearizability in terms of invariant factors of the equivalent linear form are given, and a criterion in terms of the distributions for a type of partial linearization is found.     

On the composability of consistency conditions

This paper presents a formal framework, which is based on the notion of a serialization set, that enables to compose a set of consistency conditions into a more restrictive one. To exemplify the utility of this framework, a list of very basic consistency conditions is identified, and it is shown that various compositions of the basic conditions yield some of the most commonly used consistency conditions, such as sequential consistency, causal memory, and Pipelined RAM. The paper also lists several applications that can benefit from even weaker semantics than Pipelined RAM that can be expressed as a composition of a small subset of the basic conditions.     

并发对象强可线性化性质的检测和验证研究

可线性化被公认为并发对象正确性标准,但其已被证明不能作为含有随机语句的并发对象的正确性标准。为此,Golab等人提出了强可线性化概念,它在可线性化的定义上增加了前缀保持性质,对并发对象具有更强的约束性。关于强可线性化的研究集中在使用特定的基本对象构造满足强可线性化性质的并发对象的可行性。对常见的并发对象的强可线性化性质的检测和验证方面的研究较为少见。     

A Loosely Coordinated Model for Heap-Based Priority Queues in Multicore Environments

Heap-based priority queues are very common dynamical data structures used in several fields, ranging from operating systems to scientific applications. However, the rise of new multicore CPUs introduced new challenges in the process of design of these data structures: in addition to traditional requirements like correctness and progress, the scalability is of paramount importance. It is a common opinion that these two demands are partially in conflict each other, so that in these computational environments it is necessary to relax the requirements of correctness and linearizability to achieve high performances. In this paper we introduce a loosely coordinated approach for the management of heap based priority queues on multicore CPUs, with the aim to realize a tradeoff between efficiency and sequential correctness. The approach is based on a sharing of information among only a small number of cores, so that to improve performance without completely losing the features of the data structure. The results obtained on a scientific problem show significant benefits both in terms of parallel efficiency, as well as in term of numerical accuracy.     

基于交互式定理证明的并发程序验证工作综述

并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用。但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果。同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难。在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证。本文对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性。交互式定理证明方法中常用程序逻辑对程序进行验证,本文分析了基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用了这些方法的程序验证工具和程序验证成果进行了总结。     

Mechanized proofs of opacity: a comparison of two techniques

Software transactional memory (STM) provides programmers with a high-level programming abstraction for synchronization of parallel processes, allowing blocks of codes that execute in an interleaved manner to be treated as atomic blocks. This atomicity property is captured by a correctness criterion called opacity, which relates the behaviour of an STM implementation to those of a sequential atomic specification. In this paper, we prove opacity of a recently proposed STM implementation: the Transactional Mutex Lock (TML) by Dalessandro et al. For this, we employ two different methods: the first method directly shows all histories of TML to be opaque (proof by induction), using a linearizability proof of TML as an assistance; the second method shows TML to be a refinement of an existing intermediate specification called TMS2 which is known to be opaque (proof by simulation). Both proofs are carried out within interactive provers, the first with KIV and the second with both Isabelle and KIV. This allows to compare not only the proof techniques in principle, but also their complexity in mechanization. It turns out that the second method, already leveraging an existing proof of opacity of TMS2, allows the proof to be decomposed into two independent proofs in the way that the linearizability proof does not.     

Linearization of discrete-time nonlinear systems and a canonicalstructure

Linearizable nonlinear discrete-time systems are described as a composition of diffeomorphisms. Linearizability of a general nonlinear system is obtained as an extension of linearizability of the system expressed in terms of the diffeomorphisms     

Application invariants: Design by Contract augmented with deployment correctness logic

Design by Contract is a method for the development of robust object‐oriented software, introducing class invariants as conditions corresponding to the design axioms that should be satisfied by every valid instance of a class. Additionally, the method states formally the way client programs should correctly utilize supplier classes, so that the composition of correct programs may be accomplished. However, the contextual correctness of supplier instances within client programs, only reflected in the client‐specific semantics for supplier‐class deployment, cannot be expressed through Design by Contract. For instance, supplier instances satisfying the supplier class invariant may not constitute plausible supplier instances in the context of a particular client program. In this context, we introduce application invariants as an extension to Design by Contract, for hosting the contextual‐correctness logic for supplier instances, as conditionally defined by client programs. This allows stronger validation of supplier instances, through the dynamic encapsulation of client‐specific acceptance filtering, enabling more intensive defect detection. Application invariants are implemented in the context of client classes as methods utilizing correctness condition expressions, are dynamically hosted within supplier instances, while always called by supplier instances when the basic supplier‐class invariant test is performed. Copyright © 2005 John Wiley & Sons, Ltd.     

An exploratory study of api changes and usages based on apache and eclipse ecosystems

Frameworks are widely used in modern software development to reduce development costs. They are accessed through their Application Programming Interfaces (APIs), which specify the contracts with client programs. When frameworks evolve, API backward-compatibility cannot always be guaranteed and client programs must upgrade to use the new releases. Because framework upgrades are not cost-free, observing API changes and usages together at fine-grained levels is necessary to help developers understand, assess, and forecast the cost of each framework upgrade. Whereas previous work studied API changes in frameworks and API usages in client programs separately, we analyse and classify API changes and usages together in 22 framework releases from the Apache and Eclipse ecosystems and their client programs. We find that (1) missing classes and methods happen more often in frameworks and affect client programs more often than the other API change types do, (2) missing interfaces occur rarely in frameworks but affect client programs often, (3) framework APIs are used on average in 35 % of client classes and interfaces, (4) most of such usages could be encapsulated locally and reduced in number, and (5) about 11 % of APIs usages could cause ripple effects in client programs when these APIs change. Based on these findings, we provide suggestions for developers and researchers to reduce the impact of API evolution through language mechanisms and design strategies.     

Runtime verification of concurrency-specific correctness criteria

We give an overview of correctness criteria specific to concurrent shared-memory programs and runtime verification techniques for verifying these criteria. We cover a spectrum of criteria, from ones focusing on low-level thread interference such as races to higher-level ones such as linearizability. We contrast these criteria in the context of runtime verification. We present the key ideas underlying the runtime verification techniques for these criteria and summarize the state of the art. Finally, we discuss the issue of coverage for runtime verification for concurrency and present techniques that improve the set of covered thread interleavings.     

基于金融交易的CICS中间件应用设计

论述了中间件在客户／服务器软件结构开发中的必要性，针对金融交易的联机事物特性，阐明了以CICS中间件为平台的3层软件体系结构应用设计思路。通过CICS客户端和服务器端的程序设计来调用CICS交易中间件的各种功能，避免了直接对通讯编程，方便地实现了程序间的参数传递，简化了应用程序设计，保障了应用程序数据的一致性和完整性。