Run-Time Analysis for Atomicity

Writing and debugging concurrent (shared-variable) programs is notoriously difficult. This motivated the development of numerous static analysis and run-time analysis techniques designed to (help) ensure that concurrent programs satisfy common correctness requirements for concurrent programs, such as absence of race conditions and absence of deadlocks. This paper focuses on another common correctness requirement for concurrent programs, namely, atomicity, which requires that any set of concurrent invocations of designated procedures is equivalent to performing those invocations serially in some order. Run-time analysis algorithms for detecting violations of atomicity are presented. The algorithms vary in cost and precision.     

Comments analysis and programming errors

Software validation is treated as the problem of detecting errors that programmers make during the software development process. This includes fault detection, in which the focus is on techniques for detecting the occurrence of local errors that result in well-defined classes of program statement faults. It also includes detecting other kinds of errors, such as decomposition errors. The main focus of the work is on a decomposition-error analysis technique called comments analysis. In this technique, errors are detected by analyzing special classes of program comments. Comments analysis has been applied to a variety of systems, including a data-processing program and an avionics real-time program. The use of comments analysis for sequential and concurrent systems is discussed, and the basic features of comments analysis tools are summarized. The relationship of comments analysis to other techniques, such as event sequence analysis, is discussed, and the differences between it and earlier work are explained     

Compile—time detection of aliasing in euclid programs

Aliasing of variables occurs when two or more identifiers accessible in the same scope refer to the same storage location. When aliasing is present, the meaning of assignments becomes obscure because assignment to one variable identifier may change the value of others. Some of the more obscure kinds of variable aliasing can be the cause of particularly insidious bugs in computer programs. Axiomatic proof systems, such as that used for the Euclid language, assume that no aliasing is present so that the meaning of assignment is clear. For this reason, Euclid requires that no aliasing be present in Euclid programs and requires the compiler to implement checks to ensure this. This paper discusses the features of Euclid that aid in the detection of aliasing. It enumerates the kinds of aliasing that can be present in Euclid programs and gives efficient one-pass algorithms for compile-time detection of potential aliases. Aliasing is related to interference between concurrent processes, and a similar algorithm for detection of inter-process interference in Concurrent Euclid programs is presented.     

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

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

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.     

Anomaly detection in concurrent Java programs using dynamic data flow analysis

Concurrency constructs are widely used when developing complex software such as real-time, networking and multithreaded client–server applications. Consequently, testing a program, which includes concurrency constructs is a very elaborate and complex process. In this work, we first identify the different classes of synchronization anomalies that may occur in concurrent Java programs. We then consider testing concurrent Java programs against synchronization anomalies using dynamic data flow analysis techniques. Moreover, we show how the data flow analysis technique can be extended to detect such anomalies.     

Modeling and Verifying Concurrent Programs with Finite Chu Spaces

Finite Chu spaces are proposed for the modeling and verification of concurrent programs. In order to model not only typical concurrent behaviors but also modern exception handling and synchronization mechanisms, we design an enriched process algebra of Chu spaces from a practical point of view. To illustrate the power of finite Chu spaces and the process algebra while abstracting away from language-specific details, an imaginary concurrent programming language (ICL) is designed. A denotational semantics of ICL is presented using finite Chu spaces and the enriched process algebra. The valuation functions are fairly straightforward since the carefully designed operators have done much of the job. The enriched process algebra is also used as the specification language for Chu spaces, with which process-algebraic properties can be specified. Verification algorithms are presented with their time complexities discussed.     

Computation of dynamic program slices for unstructured programs

A dynamic program slice is an executable part of the program whose behaviour is identical, for the same program input, to that of the original program with respect to a variable(s) of interest at some execution position. The existing algorithms of dynamic slice computation use data and control dependencies to compute dynamic slices. These algorithms are limited to structured programs because they may compute incorrect dynamic slices for unstructured programs, due to the limitations of control dependencies that are used to compute dynamic slices. In this paper, we present a novel approach to dynamic slice computation for unstructured programs. The approach employs the notion of a removable block in finding dynamic program slices. Dynamic slices are derived by identifying not only those parts of program execution that contribute to the computation of the value of a variable of interest, but also those parts of program execution that do not contribute to the computation of the variable value. Data dependencies are used to identify contributing computations, whereas removable blocks are used to identify noncontributing computations. We have proved that the presented dynamic slicing algorithms correctly compute dynamic slices. In addition, these algorithms may compute more accurate dynamic slices compared to existing algorithms that use control dependencies. The presented algorithms have been implemented in a tool that supports dynamic slicing for Pascal programs     

自动验证并发实时系统的线性时段性质

介绍了一个就线性时段性验证实时系统正确性的工具的设计思想以及相关算法,使用时间自动机作为产时系统的描述模型,同时,为了便珩描述并发实时系统,使用带共享变量和通道的时间自动机网作为模型描述并发实时系统,在检验时间自动机网时,用户可以使用工具提供的合成程序将其合并为一个时间自动机然后进行检验,由于时间自动机的状态空间是无究的,通过引入整数状态和状态等价关系的概念,将整个状态0空间划分为有限的状态等价类空间,模型检验过程只需要通过对等价类空间的搜索就可以完成,但往往等价类空间的规模很大,超出了现在计算机的处理能力,原始搜索算法仅仅在理论上是可知地的,为了增工具的使用性,工具中使用的算法运用了一些优化技术来避免对等价类空间的穷尽搜索,使得工具在使用时具有比较好的时间和空间效率。     

Precise slicing of interprocedural concurrent programs

Program slicing is an effective technique for analyzing concurrent programs. However, when a conventional closure-based slicing algorithmfor sequential programs is applied to a concurrent interprocedural program, the slice is usually imprecise owing to the intransitivity of interference dependence. Interference dependence arises when a statement uses a variable defined in another statement executed concurrently. In this study, we propose a global dependence analysis approach based on a program reachability graph, and construct a novel dependence graph calledmarking-statement dependence graph (MSDG), in which each vertex is a 2-tuple of program state and statement. In contrast to the conventional program dependence graph where the vertex is a statement, the dependence relation in MSDG is transitive. When traversing MSDG, a precise slice will be obtained. To enhance the slicing efficiency without loss of precision, our slicing algorithm adopts a hybrid strategy. The procedures containing interaction statements between threads are inlined and sliced by the slicing algorithm based on program reachability graphs while allowing other procedures to be sliced as sequential programs. We have implemented our algorithm and three other representative slicing algorithms, and conducted an empirical study on concurrent Java programs. The experimental results show that our algorithm computes more precise slices than the other algorithms. Using partial-order reduction techniques, which are effective for reducing the size of a program reachability graph without loss of precision, our algorithm is optimized, thereby improving its performance to some extent.     

Outlier detection based on Gaussian process with application to industrial processes

Due to the extensive usage of data-based techniques in industrial processes, detecting outliers for industrial process data become increasingly indispensable. This paper proposes an outlier detection scheme that can be directly used for either process monitoring or process control. Based on traditional Gaussian process regression, we develop several detection algorithms, of which the mean function, covariance function, likelihood function and inference method are specially devised. Compared with traditional detection methods, the proposed scheme has less postulation and is more suitable for modern industrial processes. The effectiveness of the proposed scheme is verified by experiments on both synthetic and real-life data sets.     

A probe effect in concurrent programs

This paper reports on an experimental study of the probe effect, defined as an alteration in the frequency of run-time computational errors observed when delays are introduced into concurrent programs. If the concurrent program being studied has no synchronization errors, then there is no probe effect. In the presence of synchronization errors, the frequency of observable output errors for a sample experimental program starts at a high value for small delays, oscillates rapidly as the delay is increased, and apparently settles at zero errors for larger values of delay. Thus, for sufficiently large delays, the probe effect can almost completely mask synchronization errors in concurrent programs. For sufficiently large concurrent process sets, even small values of embedded delay may mask synchronization errors, provided side effects in shared memory are not included in the observation.     

Deadlock detection without wait-for graphs

Deadlock detection is an important service that the run-time system of a parallel environment should provide. In parallel programs deadlock can occur when the different processes are waiting for various events, as opposed to concurrent systems, where deadlock occurs when processes wait for resources held by other processes. Therefore classical deadlock detection techniques such as checking for cycles in the wait-for graph are unapplicable. An alternative algorithm that checks whether all the processes are blocked is presented. This algorithm deals with situations in which the state transition from blocked to unblocked is indirect, as may happen when busy-waiting is used.     

A robust monitor construct with runtime fault detection

The monitor concept provides a structured and flexible high‐level programming construct to control concurrent accesses to shared resources. It has been widely used in a concurrent programming environment for implicitly ensuring mutual exclusion and explicitly achieving process synchronization. This paper proposes an extension to the monitor construct for detecting runtime errors in monitor operations. Monitors are studied and classified according to their functional characteristics. A taxonomy of concurrency control faults over a monitor is then defined. The concepts of a monitor event sequence and a monitor state sequence provide a uniform approach to history information recording and fault detection. Rules for detecting various types of faults are defined. Based on these rules, fault‐detection algorithms are developed. A prototypical implementation of the proposed monitor construct with runtime fault detection mechanisms has been developed in Java. We shall briefly report our experience with and the evaluation of the robust monitor prototype. Copyright © 2005 John Wiley & Sons, Ltd.     

Model-based diagnosis of spreadsheet programs: a constraint-based debugging approach

Spreadsheet programs are probably the most successful example of end-user software development tools and are used for a variety of purposes. Like any type of software, they are prone to error, in particular as they are usually developed by non-programmers. While various techniques exist to support the developer in finding errors in procedural programs, the tool support for spreadsheet debugging is still limited. In this paper, we show how techniques from model-based diagnosis can be applied and extended for spreadsheet debugging by translating the relevant parts of a spreadsheet to a constraint satisfaction problem. We additionally propose both problem-specific and generalizable extensions to the classical diagnosis algorithms which help to detect potential problems in a spreadsheet based on user-provided test cases more efficiently. The proposed techniques were integrated into a modular framework for spreadsheet debugging and evaluated with respect to scalability based on a number of real-world and artificially created spreadsheets. An additional error detection exercise involving 24 subjects was performed to assess the general applicability of such advanced spreadsheet debugging techniques for end users.     

Multistrategy Discovery and Detection of Novice Programmer Errors

Detecting and diagnosing errors in novice behavior is an important student modeling task. In this paper, we describe MEDD, an unsupervised incremental multistrategy system for the discovery of classes of errors from, and their detection in, novice programs. Experimental results show that MEDD can effectively detect and discover misconceptions and other knowledge-level errors that underlie novice Prolog programs, even when multiple errors are enmeshed together in a single program, and when the programs are presented to MEDD in a different order.     

GC-MCR: Directed Graph Constraint-guided Concurrent Bug Detection Method

Constraint solving has been applied to many domains of program analysis and is further used in concurrent program analysis. Concurrent programs have been widely used with the rapid development of multi-core processors. However, concurrent bugs threaten the security and reliability of concurrent programs, and thus it is of great importance to detect concurrent bugs. The explosion of thread interleaving caused by the uncertainty of the execution of concurrent program threads brings some challenges to the detection of concurrent bugs. Existing concurrent defect detection algorithms reduce the exploration cost in the state space of concurrent programs by reducing invalid thread interleaving. For example, the maximal causal model algorithm transforms the state space exploration problem of concurrent programs into a constraint solving problem. However, it will produce a large number of redundant and conflicting constraints during constraint construction, which greatly prolongs the time of constraint solving, increases the number of constraint solver calls, and reduces the exploration efficiency of concurrent program state space. Thus, this study proposes a directed graph constraint-guided maximal causality reduction method, called GC-MCR. This method aims to improve the speed of constraint solving and the efficiency of the state space exploration of concurrent programs by filtering and reducing constraints using directed graphs. The experimental results show that the GC-MCR method can effectively optimize the expression of constraints, so as to improve the solving speed of the constraint solver and reduce the number of solver calls. Compared with the existing J-MCR method, GC-MCR can significantly improve the detection efficiency of concurrent program bugs without reducing the detection ability of concurrent bugs, and the test time on 38 groups of concurrent test programs widely used by existing research methods can be reduced by 34.01% on average.     

Separate computation of alias information for reuse

Interprocedural data flow information is useful for many software testing and analysis techniques, including data flow testing, regression testing, program slicing and impact analysis. For programs with aliases, these testing and analysis techniques can yield invalid results, unless the data flow information accounts for aliasing effects. Recent research provides algorithms for performing interprocedural data flow analysis in the presence of aliases; however, these algorithms are expensive, and achieve precise results only on complete programs. This paper presents an algorithm for performing alias analysis on incomplete programs that lets individual software components such as library routines, subroutines or subsystems be independently analyzed. The paper also presents an algorithm for reusing the results of this separate analysis when the individual software components are linked with calling modules. Our algorithms let us analyze frequently used software components, such as library routines or classes, independently, and reuse the results of that analysis when analyzing calling programs, without incurring the expense of completely reanalyzing each calling program. Our algorithms also provide a way to analyze large systems incrementally     

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