The rely-guarantee method for verifying shared variable concurrent programs

Compositional proof systems for shared variable concurrent programs can be devised by including the interference information in the specifications. The formalism falls into a category calledrely-guarantee (orassumption-commitment), in which a specification is explicitly (syntactically) split into two corresponding parts. This paper summarises existing work on the rely-guarantee method and gives a systematic presentation. A proof system for partial correctness is given first, thereafter it is demonstrated how the relevant rules can be adapted to verify deadlock freedom and convergence. Soundness and completeness, of which the completeness proof is new, are studied with respect to an operational model. We observe that the rely-guarantee method is in a sense a reformulation of the classical non-compositional Owicki & Gries method, and we discuss throughout the paper the connection between these two methods.The research was partially supported by Esprit-BRA project 6021 (REACT).     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms.This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms. This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

Forward and Backward Simulations

A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model. In particular, (1) refinements, (2) forward and backward simulations, (3) hybrid forward-backward and backward-forward simulations, and (4) history and prophecy relations are defined. History and prophecy relations are abstract versions of the history and prophecy variables of Abadi and Lamport, as well as the auxiliary variables of Owicki and Gries, Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. Finally, it is shown how invariants can be incorporated into all the simulations. Even though many results are presented here for the first time, this paper can also be read as a survey (in a simple setting) of the research literature on simulation techniques. The development for untimed automata is designed to support a similar development for timed automata, Part II of this paper will show how the results of this paper can be carried over to the setting of timed automata.     

Recursive assertions and parallel programs

Summary We prove that recursive assertions are enough for proofs of parallel programs considered in Owicki and Gries [7]. In other words, we prove that for any parallel program S and recursive assertions p and q if {p} S{q} is true under the standard interpretation in natural numbers then all intermediate assertions needed in the proof can be chosen recursive. Finally, we show that if auxiliary variables are used only as program counters then the above result does not hold.     

A shared-variable concurrency analysis of multi-threaded object-oriented programs

In this paper a proof outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. The main contribution is a generalization of the Owicki& Gries proof method for shared-variable concurrency to dynamic thread creation. This paper also provides a formal justification of this generalization in terms of soundness and completeness proofs.     

Inductive inference of logic programs based on algebraic semantics

In this paper we present a new inductive inference algorithm for a class of logic programs, calledlinear monadic logic programs. It has several unique features not found in Shapiro’s Model Inference System. It has been proved that a set of trees isrational if and only if it is computed by a linear monadic logic program, and that the rational set of trees is recognized by a tree automaton. Based on these facts, we can reduce the problem of inductive inference of linear monadic logic programs to the problem of inductive inference of tree automata. Further several efficient inference algorithms for finite automata have been developed. We extend them to an inference algorithm for tree automata and use it to get an efficient inductive inference algorithm for linear monadic logic programs. The correctness, time complexity and several comparisons of our algorithm with Model Inference System are shown.     

A Standard Model—Theoretic Approach to Operational Semmantics of Recursiv Programs

In this paper we try to introduce a new approach to operational semantics of recursive programs by using ideas in the“priority method”which is a fundamental tool in Recursion Theory.In lieu of modelling partial functions by introducing undefined values in a traditional approach,we shall define a priority derivation tree for every term,and by respecting thr rule“attacking the subtem of the highest priority first”we define transition relations,computation sequences etc.directly based on a standard interpretation whic includes no undefined value in its domain,Finally,we prove that our new approach generates the same opeational semantics as the traditional one.It is also pointed out that we can use our strategy oto refute a claim of Loeckx and Sieber that the opperational semantics of recursive programs cannot be built based on predicate logic.     

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

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

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.     

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction refinement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.     

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.     

Asynchronous communication model based on linear logic

We propose a new framework called ACL for concurrent computation based on linear logic. ACL is a kind oflinear logic programming framework, where its operational semantics is described in terms ofproof construction in linear logic. We also give a model-theoretic semantics based onphase semantics, a model of linear logic. Our framework well captures concurrent computation based on asynchronous communication. It will, therefore, provide us with a new insight into other models of asynchronous concurrent computation from alogical point of view. We also expect ACL to become a formal framework for analysis, synthesis and transformation of concurrent programs by the use of techniques for traditional logic programming. ACL's attractive features for concurrent programming paradigms are also discussed.     

Dynamic slicing of concurrent AspectJ programs: An explicit context‐sensitive approach

This paper presents a context‐sensitive dynamic slicing technique for the concurrent and aspectized programs. To effectively represent the concurrent aspect‐oriented programs, we propose an intermediate graph called the multithreaded aspect‐oriented dependence graph (MAODG). The MAODG is a dynamic graph generated from the execution trace of a given program with respect to a particular set of values given as an input. Interference dependencies between the statements are shown by a distinguished edge called the interference dependence edge in the MAODG. Based on this intermediate representation, we propose a precise and accurate dynamic slicing algorithm for the concurrent aspect‐oriented programs implemented using AspectJ. The proposed dynamic slicing algorithm is implemented in a slicing tool developed using the ASM framework. Several open source programs are studied and evaluated using the proposed technique along with some existing techniques. The experimentation shows that our proposed slicing algorithm generates slices of the same or smaller size, as compared with the existing algorithms. Furthermore, we found that the slice computation time is significantly less in our proposed algorithm, as compared with the existing algorithms.     

Fast and accurate mining of correlated heavy hitters

The problem of mining correlated heavy hitters (CHH) from a two-dimensional data stream has been introduced recently, and a deterministic algorithm based on the use of the Misra–Gries algorithm has been proposed by Lahiri et al. to solve it. In this paper we present a new counter-based algorithm for tracking CHHs, formally prove its error bounds and correctness and show, through extensive experimental results, that our algorithm outperforms the Misra–Gries based algorithm with regard to accuracy and speed whilst requiring asymptotically much less space.     

A transformation system for concurrent processes

Program transformation techniques have been extensively studied in the framework of functional and logic languages, where they were applied mainly to obtain more efficient and readable programs. All these works are based on the Unfold/Fold program transformation method developed by Burstall and Darlington in the context of their recursive equational language. The use of Unfold/Fold based transformations for concurrent languages is a relevant issue that has not yet received an adequate attention. In this paper we define a transformation methodology for CCS. We give a set of general rules which are a specialization of classical program transformation rules, such as Fold and Unfold. Moreover, we define the general form of other rules, “oriented” to the goal of a transformation strategy, and we give conditions for the correctness of these rules. We prove that a strategy using the general rules and a set of goal oriented rules is sound, i.e. it transforms CCS programs into equivalent ones. We show an example of application of our method. We define a strategy to transform, if possible, a full CCS program into an equivalent program whose semantics is a finite transition system. We show that, by means of our methodology, we are able to a find finite representations for a class of CCS programs which is larger than the ones handled by the other existing methods. Our transformational approach can be seen as unifying in a common framework a set of different techniques of program analysis. A further advantage of our approach is that it is based only on syntactic transformations, thus it does not requires any semantic information. Received: 24 April 1997 / 19 November 1997     

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.     

Consistency Property of Finite FC-Normal Logic Programs

Marek＇s forward-chaining construction is one of the important techniques for investigating the non-monotonic reasoning. By introduction of consistency property over a logic program, they proposed a class of logic programs, FC-normal programs, each of which has at least one stable model. However, it is not clear how to choose one appropriate consistency property for deciding whether or not a logic program is FC-normal. In this paper, we firstly discover that, for any finite logic programⅡ, there exists the least consistency property LCon（Ⅱ） overⅡ, which just depends onⅡitself, such that, Ⅱ is FC-normal if and only ifⅡ is FC-normal with respect to （w.r.t.） LCon（Ⅱ）. Actually, in order to determine the FC-normality of a logic program, it is sufficient to check the monotonic closed sets in LCon（Ⅱ） for all non-monotonic rules, that is LFC（Ⅱ）. Secondly, we present an algorithm for computing LFC（Ⅱ）. Finally, we reveal that the brave reasoning task and cautious reasoning task for FC-normal logic programs are of the same difficulty as that of normal logic programs.     

Formal Reasoning About Lazy-STM Programs

Transactional memory (TM) is an easy-using parallel programming model that avoids common problems associated with conventional locking techniques. Several researchers have proposed a large amount of alternative hardware and software TM implementations. However, few ones focus on formal reasoning about these TM programs. In this paper, we propose a framework at assembly level for reasoning about lazy software transactional memory (STM) programs. First, we give a software TM implementation based on lightweight locks. These locks are also one part of the shared memory. Then we define the semantics of the model operationally, and the lightweight locks in transaction are non-blocking, avoiding deadlocks among transactions. Finally we design a logic — a combination of permission accounting in separation logic and concurrent separation logic — to verify various properties of concurrent programs based on this machine model. The whole framework is formalized using a proof-carrying-code (PCC) framework.     

Modalities for model checking: branching time logic strikes back

We consider automatic verification of finite state concurrent programs. The global state graph of such a program can be viewed as a finite (Kripke) structure, and amodel checking algorithm can be given for determining if a given structure is a model of a specification expressed in a propositional temporal logic. In this paper, we present a unified approach for efficient model checking under a broad class of generalized fairness constraints in a branching time framework extending that of Clarke et al. (1983). Our method applies to any type of fairness expressed in a certain canonical form. Almost all ‘practical’ types of fairness from the literature, including the fundamental notions of impartiality, weak fairness, and strong fairness, can be succintly written in our canonical form. Moreover, our branching time approach can easily be adapted to handle types of fairness (such as fair reachability of a predicate) which cannot even be expressed in a linear temporal logic. We go on to argue that branching time logic is always better than linear time logic for model checking. We show that given any model checking algorithm for any system of linear time logic (in particular, for the usual system of linear time logic) there is a model checking algorithm of the same order of complexity (in both the structure and formula size) for the corresponding full branching time logic which trivially subsumes the linear time logic in expressive power (in particular, for the system of full branching time logic CTL^*). We also consider an application of our work to the theory of finite automata on infinite strings.