A generic approach to the static analysis of concurrent programs with procedures

We present a generic aproach to the static analysis of concurrent programs with procedures. We model programs as communicating pushdown systems. It is known that typical dataflow problems for this model are undecidable, because the emptiness problem for the intersection of context-free languages, which is undecidable, can be reduced to them. In this paper we propose an algebraic framework for defining abstractions (upper approximations) of context-free languages. We consider two classes of abstractions: finite-chain abstractions, which are abstractions whose domains do not contain any infinite chains, and commutative abstractions corresponding to classes of languages that contain a word if and only if they contain all its permutations. We show how to compute such approximations by combining automata theoretic techniques with algorithms for solving systems of polynomial inequations in Kleene algebras.

Download Full-text

Detecting concurrency anomalies in transactional memory programs

Computer Science and Information Systems ◽

10.2298/csis110110007l ◽

2011 ◽

Vol 8 (2) ◽

pp. 534-548 ◽

Cited By ~ 2

Author(s):

João Lourenço ◽

Diogo Sousa ◽

Bruno Teixeira ◽

Ricardo Dias

Keyword(s):

Shared Memory ◽

Static Analysis ◽

Transactional Memory ◽

Analysis Procedure ◽

Concurrent Programs ◽

Program Correctness ◽

Classic Case ◽

Analysis Techniques ◽

High Level ◽

Different Sources

Concurrent programs may suffer from concurrency anomalies that may lead to erroneous and unpredictable program behaviors. To ensure program correctness, these anomalies must be diagnosed and corrected. This paper addresses the detection of both low- and high-level anomalies in the Transactional Memory setting. We propose a static analysis procedure and a framework to address Transactional Memory anomalies. We start by dealing with the classic case of low-level dataraces, identifying concurrent accesses to shared memory cells that are not protected within the scope of a memory transaction. Then, we address the case of high-level dataraces, bringing the programmer?s attention to pairs of memory transactions that were misspecified and should have been combined into a single transaction. Our framework was applied to a set of programs, collected form different sources, containing well known low- and high-level anomalies. The framework demonstrated to be accurate, confirming the effectiveness of using static analysis techniques to precisely identify concurrency anomalies in Transactional Memory programs.

Download Full-text

Concurrent Bug Detection Using Invariant Analysis

International Journal of Engineering & Technology ◽

10.14419/ijet.v7i3.4.14666 ◽

2018 ◽

Vol 7 (3.4) ◽

pp. 6

Author(s):

Bidush Kumar Sahoo ◽

Mitrabinda Ray

Keyword(s):

Static Analysis ◽

Source Code ◽

Invariant Set ◽

Concurrent Programs ◽

Testing Technique ◽

Bug Detection ◽

Concurrent Program ◽

Call Graph ◽

Multiple Thread ◽

Invariant Analysis

In concurrent programs, bug detection is a tedious job due to non-determinism and multiple thread control. The bug detection is done by checking the interleaving of threads which is not available in operational phases. So, static analysis is one of the preferred approaches for detection of concurrent bug. Invariant based testing technique is one approach of static analysis used for detecting the concurrent bugs. In this paper, we discuss an invariant based testing approach using three steps: (i) the invariants of a given concurrent program are generated using Daikon tool. (ii) The bad invariants are removed by using the static call graph of the source code, where the static call graph is generated by the javacg tool. (iii) The reduced invariant set is obtained by eliminating the bad and redundant invariants which is used for testcase generation. Using the reduced invariant set, we generate the testcases that are used to find the various concurrent bugs such as Deadlock, Atomicity violation and Bad composition. We conducted an experiment on a well-known concurrent program called the Dining Philosopher Problem. The experimental results show that, the testcases obtained from the reduced invariant set is able to detect more types and no. of concurrent bugs than the existing approach on invariant based testing.

Download Full-text

FORWARD ANALYSIS OF DYNAMIC NETWORK OF PUSHDOWN SYSTEMS IS EASIER WITHOUT ORDER

International Journal of Foundations of Computer Science ◽

10.1142/s0129054111008453 ◽

2011 ◽

Vol 22 (04) ◽

pp. 843-862 ◽

Cited By ~ 4

Author(s):

DENIS LUGIEZ

Keyword(s):

Static Analysis ◽

Dynamic Networks ◽

Dynamic Network ◽

Concurrent Programs ◽

Parallel Composition ◽

Tree Automata ◽

Weighted Tree ◽

Weighted Automata ◽

Forward Analysis ◽

Weighted Tree Automata

Dynamic networks of Pushdown Systems (DNPS in short) have been introduced to perform static analysis of concurrent programs that may spawn threads dynamically. In this model the set of successors of a regular set of configurations can be non-regular, making forward analysis of these models difficult. We refine the model by adding the associative-commutative properties of parallel composition, and we define Presburger weighted tree automata, an extension of weighted automata and tree automata, that accept the set of successors of a regular set of configurations. This yields decidability of the forward analysis of DNPS. Finally, we extend this result to the model where configurations are sets of threads running in parallel.

Download Full-text