Runtime analysis of atomicity for multithreaded programs

Atomicity is a correctness condition for concurrent systems. Informally, atomicity is the property that every concurrent execution of a set of transactions is equivalent to some serial execution of the same transactions. In multithreaded programs, executions of procedures (or methods) can be regarded as transactions. Correctness in the presence of concurrency typically requires atomicity of these transactions. Tools that automatically detect atomicity violations can uncover subtle errors that are hard to find with traditional debugging and testing techniques. This paper describes two algorithms for runtime detection of atomicity violations and compares their cost and effectiveness. The reduction-based algorithm checks atomicity based on commutativity properties of events in a trace; the block-based algorithm efficiently represents the relevant information about a trace as a set of blocks (i.e., pairs of events plus associated synchronizations) and checks atomicity by comparing each block with other blocks. To improve the efficiency and accuracy of both algorithms, we incorporate a multilockset algorithm for checking data races, dynamic escape analysis, and happen-before analysis. Experiments show that both algorithms are effective in finding atomicity violations. The block-based algorithm is more accurate but more expensive than the reduction-based algorithm.     

Atomizer: A dynamic atomicity checker for multithreaded programs

Ensuring the correctness of multithreaded programs is difficult, due to the potential for unexpected interactions between concurrent threads. Much previous work has focused on detecting race conditions, but the absence of race conditions does not by itself prevent undesired interactions between threads.A more fundamental noninterference property is atomicity. A method is atomic if its execution is not affected by and does not interfere with concurrently-executing threads. Atomic methods can be understood according to their sequential semantics, which significantly simplifies both formal and informal correctness arguments.This paper presents a dynamic analysis for detecting atomicity violations. This analysis combines ideas from both Lipton’s theory of reduction and earlier dynamic race detectors. Experience with a prototype checker for multithreaded Java code demonstrates that this approach is effective for detecting errors due to unintended interactions between threads. In particular, our atomicity checker detects errors that would be missed by standard race detectors. Our experimental results also indicate that the majority of methods in our benchmarks are atomic, indicating that atomicity is a standard methodology in multithreaded programming.     

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.     

Generating effective tests for concurrent programs via AI automated planning techniques

Testing concurrent programs is a challenging problem due to interleaving explosion: even for a fixed set of inputs, there is a huge number of concurrent runs that need to be tested to account for scheduler behavior. Testing all possible schedules is not practical. Consequently, most effective testing algorithms only test a select subset of runs. For example, limiting testing to runs that contain data races or atomicity violations has been shown to capture a large proportion of concurrency bugs. In this paper we present a general approach to concurrent program testing that is based on techniques from artificial intelligence (AI) automated planning. We propose a framework for predicting concurrent program runs that violate a collection of generic correctness specifications for concurrent programs, namely runs that contain data races, atomicity violations, or null-pointer dereferences. Our prediction is based on observing an arbitrary run of the program, and using information collected from this run to model the behavior of the program, and to predict new runs that contain bugs with one of the above noted violation patterns. We characterize the problem of predicting such new runs as an AI sequential planning problem with the temporally extended goal of achieving a particular violation pattern. In contrast to many state-of-the-art approaches, in our approach feasibility of the predicted runs is guaranteed and, therefore, all generated runs are fully usable for testing. Moreover, our planning-based approach has the merit that it can easily accommodate a variety of violation patterns which serve as the selection criteria for guiding search in the state space of concurrent runs. This is achieved by simply modifying the planning goal. We have implemented our approach using state-of-the-art AI planning techniques and tested it within the Penelope concurrent program testing framework [35]. Nevertheless, the approach is general and is amenable to a variety of program testing frameworks. Our experiments with a benchmark suite showed that our approach is very fast and highly effective, finding all known bugs.     

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

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

并行程序的原子性验证算法研究

原子性保证并行程序中的多线程以正确方式交互,大多主流的编程语言都没有提供确保原子性的内部机制.为了提高测试程序原子性的效率与准确性,提出了一种自动检测并行程序中违反原子性错误的算法.基于状态转换,建立了原子性的形式化定义.在此基础上,利用线程锁设计了具体的算法模型以及实现中需注意的细节,同时给出自动修正错误的设计思路和建议.结合常用的基准数据结构,对模型和算法进行了实验,实验结果表明了该算法的正确性和有效性.     

Elucidating concurrent algorithms via layers of abstraction and reification

Arguing that intricate concurrent programs satisfy their specifications can be difficult; recording understandable explanations is important for subsequent readers. Abstraction is a key tool even for sequential programs. The purpose here is to explore some abstractions that help readers (and writers) understand the design of concurrent programs. As an illustration, the paper presents a formal development of a non-trivial parallel program: Simpson’s implementation of asynchronous communication mechanisms. Although the correctness of this “4-slot algorithm” has been shown elsewhere, earlier proofs fail to offer much insight into the design. From an understandable (yet formal) design history of this one algorithm, the techniques employed in the explanation are teased out for wider application. Among these techniques is using a “fiction of atomicity” as an aid to understanding the initial steps of development. The rely-guarantee approach is, here, combined with notions of read/write frames and “phased” specifications; furthermore, the atomicity assumptions implied by the rely/guarantee conditions are achieved by clever choice of data representations.     

Model-checking multi-threaded distributed Java programs

State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of synchronization, namely, the use of locks to protect shared data structures. This pattern of synchronization is particularly common in concurrent Java programs, because Java provides built-in locks. We describe the design of a new tool for state-less state-space exploration of Java programs that incorporates this reduction. We also describe an implementation of the reduction in Java PathFinder, a more traditional state-space exploration tool for Java programs. Published online: 2 October 2002 RID="*" ID="*"Present address: Computer Science Dept., SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA. The author gratefully acknowledges the support of ONR under Grants N00014-99-1-0358 and N00014-01-1-0109 and the support of NSF under Grant CCR-9876058.     

Automatically Verifying Concurrent Queue Algorithms

Concurrent FIFO queues are a common component of concurrent systems. Using a single shared lock to prevent concurrent manipulations of queue contents reduces system concurrency. Therefore, many algorithms were suggested to increase concurrency while maintaining the correctness of queue manipulations. This paper shows how to automatically verify partial correctness of concurrent FIFO queue algorithms using existing abstract interpretation techniques. In particular, we verify all the safety properties originally specified for two concurrent queue algorithms without imposing an a priori bound on the number of allocated objects and threads.     

Exploiting purity for atomicity

Multithreaded programs often exhibit erroneous behavior because of unintended interactions between concurrent threads. This paper focuses on the noninterference property of atomicity. A procedure is atomic if, for every execution, there is an equivalent serial execution in which the actions of the atomic procedure are not interleaved with actions of other threads. This key property makes atomic procedures amenable to sequential reasoning techniques, which significantly facilitates subsequent validation activities such as code inspection and testing. Several existing tools verify atomicity by using commutativity of actions to show that every execution reduces to a corresponding serial execution. However, experiments with these tools have highlighted a number of interesting procedures that, while intuitively atomic, are not reducible. In this paper, we exploit the notion of pure code blocks to verify the atomicity of such irreducible procedures. If a pure block terminates normally, then its evaluation does not change the program state and, hence, these evaluation steps can be removed from the program trace before reduction. We develop a static typed-based analysis for atomicity based on this insight, and we illustrate this analysis on a number of interesting examples that could not be verified using earlier tools based purely on reduction.     

Verifying general safety properties of Ada tasking programs

The isolation approach to symbolic execution of Ada tasking programs provides a basis for automating partial correctness proofs. The strength of this approach lies in its isolation nature; tasks are symbolically executed and verified independently, and then checked for cooperation where interference can occur. This keeps the verification task computationally feasible and enhances its compositionality. Safety, however, is a more appropriate notion of correctness for concurrent programs than partial correctness. The author shows how the isolation approach to symbolic execution of Ada tasking program supports the verification of general safety properties. Specific safety properties that are considered include mutual exclusion, freedom from deadlock, and absence of communication failure. The techniques are illustrated using a solution to the readers and writers problem     

RGITL: A temporal logic framework for compositional reasoning about interleaved programs

This paper gives a self-contained presentation of the temporal logic Rely-Guarantee Interval Temporal Logic (RGITL). The logic is based on interval temporal logic (ITL) and higher-order logic. It extends ITL with explicit interleaved programs and recursive procedures. Deduction is based on the principles of symbolic execution and induction, known from the verification of sequential programs, which are transferred to a concurrent setting with temporal logic. We include an interleaving operator with compositional semantics. As a consequence, the calculus permits proving decomposition theorems which reduce reasoning about an interleaved program to reasoning about individual threads. A central instance of such theorems are rely-guarantee (RG) rules, which decompose global safety properties. We show how the correctness of such rules can be formally derived in the calculus. Decomposition theorems for other global properties are also derivable, as we show for the important progress property of lock-freedom. RGITL is implemented in the interactive verification environment KIV. It has been used to mechanize various proofs of concurrent algorithms, mainly in the area oflinearizable and lock-free algorithms.     

Subtleties of Transactional Memory Atomicity Semantics

Transactional memory has great potential for simplifying multithreaded programming by allowing programmers to specify regions of the program that must appear to execute atomically. Transactional memory implementations then optimistically execute these transactions concurrently to obtain high performance. This work shows that the same atomic guarantees that give transactions their power also have unexpected and potentially serious negative effects on programs that were written assuming narrower scopes of atomicity. We make four contributions: (1) we show that a direct translation of lock-based critical sections into transactions can introduce deadlock into otherwise correct programs, (2) we introduce the terms strong atomicity and weak atomicity to describe the interaction of transactional and non-transactional code, (3) we show that code that is correct under weak atomicity can deadlock under strong atomicity, and (4) we demonstrate that sequentially composing transactional code can also introduce deadlocks. These observations invalidate the intuition that transactions are strictly safer than lock-based critical sections, that strong atomicity is strictly safer than weak atomicity, and that transactions are always composable     

Applying semantic knowledge to real-time update of access control policies

Real-time update of access control policies, that is, updating policies while they are in effect and enforcing the changes immediately, is necessary for many security-critical applications. In this paper, we consider real-time update of access control policies in a database system. Updating policies while they are in effect can lead to potential security problems, such as, access to database objects by unauthorized users. In this paper, we propose several algorithms that not only prevent such security breaches but also ensure the correctness of execution. The algorithms differ from each other in the degree of concurrency provided and the semantic knowledge used. Of the algorithms presented, the most concurrency is achieved when transactions are decomposed into atomic steps. Once transactions are decomposed, the atomicity, consistency, and isolation properties no longer hold. Since the traditional transaction processing model can no longer be used to ensure the correctness of the execution, we use an alternate semantic-based transaction processing model. To ensure correct behavior, our model requires an application to satisfy a set of necessary properties, namely, semantic atomicity, consistent execution, sensitive transaction isolation, and policy-compliant. We show how one can verify an application statically to check for the existence of these properties.     

并发程序原子图挖掘技术

针对当前并发程序的不确定性和复杂性,以及程序原子性质获取困难的问题,提出一种并发程序原子性质提取方法。将并发程序中的同步区域转化为与并发操作相关的并发操作图后,采用频繁子图挖掘算法自动提取程序中的原子图,使其能刻画并发程序的原子性质,包括并发操作以及操作之间的控制依赖关系。实验结果证明,该方法能以较低的误测率有效提取并发程序的原子性质。     

Apportioning: a technique for efficient reachability analysis ofconcurrent object-oriented programs

The object-oriented paradigm in software engineering provides support for the construction of modular and reusable program components and is attractive for the design of large and complex distributed systems. Reachability analysis is an important and well-known tool for static analysis of critical properties in concurrent programs, such as deadlock freedom. It involves the systematic enumeration of all possible global states of program execution and provides the same level of assurance for properties of the synchronization structure in concurrent programs, such as formal verification. However, direct application of traditional reachability analysis to concurrent object-oriented programs has many problems, such as incomplete analysis for reusable classes (not safe) and increased computational complexity (not efficient). We propose a novel technique called apportioning, for safe and efficient reachability analysis of concurrent object-oriented programs, that is based upon a simple but powerful idea of classification of program analysis points as local (having influence within a class) and global (having possible influence outside a class). We have developed a number of apportioning-based algorithms, having different degrees of safety and efficiency. We present the details of one of these algorithms, formally show its safety for an appropriate class of programs, and present experimental results to demonstrate its efficiency for various examples     

Simple concurrent garbage collection almost without synchronization

We present two simple mark and sweep algorithms, A and B, for concurrent garbage collection by a single collector running concurrently with a number of mutators that concurrently modify shared data. Both algorithms are based on the ideas of Ben-Ari’s classical algorithm for on-the-fly garbage collection with one mutator. The algorithms require the mutators to estimate the set of objects they currently hold in private variables. They differ in the grain of atomicity of this estimate and in their mutator marking requirements.     

多重中断C程序中数据竞争及原子性检测

在多重中断C程序中,中断嵌套可能会导致一些非期望的交叠执行,从而造成错误的程序执行结果。典型的问题是共享变量引起的数据竞争破坏了程序的原子性。针对此类问题,对多重中断C程序的运行时语义进行建模,根据共享变量的访问给出了一种原子性的定义,提出了相应的数据竞争及原子性检测方法,并采用函数摘要技术缩减静态分析过程中所需遍历的程序状态。最后,设计并实现了一个数据竞争及原子性检测原型工具MIDAC(multiple interruption C program data race and atomicity checker),实验结果表明,该工具能够针对一定规模的实际程序得到很好的检测效果。     

Contracts for concurrency

The SCOOP model extends the Eiffel programming language to provide support for concurrent programming. The model is based on the principles of Design by Contract. The semantics of contracts used in the original proposal (SCOOP_97) is not suitable for concurrent programming because it restricts parallelism and complicates reasoning about program correctness. This article outlines a new contract semantics which applies equally well in concurrent and sequential contexts and permits a flexible use of contracts for specifying the mutual rights and obligations of clients and suppliers while preserving the potential for parallelism. We argue that it is indeed a generalisation of the traditional correctness semantics. We also propose a proof technique for concurrent programs which supports proofs—similar to those for traditional non-concurrent programs—of partial correctness and loop termination in the presence of asynchrony. P. J. Brooke, R. F. Paige and Dong Jin Song