João Lourenço

This special issue concerns a range of issues related to the development of concurrent programs. This is an important topic, because many systems are now either multi-threaded or distributed, and it is well known that concurrency makes testing, analysis and debugging significantly more complicated. Essentially, the alternative interleavings of events can lead to different behaviours, and so any analysis, debugging or testing technique must consider these interleavings. The interest in this topic is reflected in the larger than normal issue, which contains five papers. The papers fall into three groups: we start with a paper on debugging, then have two on static analysis techniques and finally have two on testing. All papers were reviewed in the normal way.

Multi-threaded programs allow one to achieve better performance by doing a lot of work in parallel using multiple threads. Such parallel programs often contain code blocks that a thread must execute atomically, i.e., with no interference from the other threads of the program. Failing to execute these code blocks atomically leads to errors known as atomicity violations. However, frequently it not obvious to tell when a piece of code should be executed atomically, especially when that piece of code contains calls to some third-party library functions, about which the programmer has little or no knowledge at all. One solution to this problem is to associate a contract with such a library, telling the programmer how the library functions should be used, and then check whether the contract is indeed respected. For contract validation, static approaches have been proposed, with known limitations on precision and scalability. In this paper, we propose a dynamic method for contract validation, which is more precise and scalable than static approaches.

Software developers are expected to protect concurrent accesses to shared regions of memory with some mutual exclusion primitive that ensures atomicity properties to a sequence of program statements. This approach prevents data races but may fail to provide all necessary correctness properties.The composition of correlated atomic operations without further synchronization may cause atomicity violations. Atomic violations may be avoided by grouping the correlated atomic regions in a single larger atomic scope. Concurrent programs are particularly prone to atomicity violations when they use services provided by third party packages or modules, since the programmer may fail to identify which services are correlated. In this paper we propose to use contracts for concurrency, where the developer of a module writes a set of contract terms that specify which methods are correlated and must be executed in the same atomic scope. These contracts are then used to verify the correctness of the main program with respect to the usage of the module(s). If a contract is well defined and complete, and the main program respects it, then the program is safe from atomicity violations with respect to that module. We also propose a static analysis based methodology to verify contracts for concurrency that we applied to some real-world software packages. The bug we found in Tomcat 6.0 was immediately acknowledged and corrected by its development team.

Transactional memory (TM) is an increasingly popular technique for synchronising threads in multi-threaded programs. To address both correctness and performance-related issues of TM programs, one needs to monitor and analyse their execution. However, monitoring concurrent programs (including TM programs) may have a non-negligible impact on their behaviour, which may hamper the objectives of the intended analysis. In this paper, we propose several approaches for monitoring TM programs and study their impact on the behaviour of the monitored programs. The considered approaches range from specialised lightweight monitoring to generic heavyweight monitoring. The implemented monitoring tools are publicly available to the scientific community, and the implementation techniques used for lightweight monitoring of TM programs may be used as an inspiration for developing other specialised lightweight monitors.

A programação concorrente obriga o programador a sincronizar os acessos concorrentes a regiões de memória partilhada, contudo esta abordagem não é suficiente para evitar todas as anomalias que podem ocorrer num cenário concorrente. Executar uma sequência de operações atómicas pode causar violações de atomicidade se existir uma correlação entre essas operações, devendo o programador garantir que toda a sequência de operações é executada atomicamente. Este problema é especialmente comum quando se usam operações de pacotes ou módulos de terceiros, pois o programador pode identificar incorretamente o âmbito das regiões de código que precisam de ser atómicas para garantir o correto comportamento do programa. Para evitar este problema o programador do módulo pode criar um contrato que especifica quais as sequências de operações do módulo que devem ser sempre executadas de forma atómica. Este trabalho apresenta uma análise estática para verificação destes contratos.

n/a

n/a

Uma das estratégias para tirar partido dos múltiplos processadores disponíveis nos computadores atuais passa por adaptar código legado, inicialmente concebido para ser executado num contexto meramente sequencial, para ser agora executado num contexto multithreading. Nesse processo de adaptação é necessário proteger apropriadamente os dados que são agora partilhados e acedidos por diferentes threads concorrentes. A proteção dos dados com locks usando uma granulosidade grossa inibe a concorrência e opõe-se ao objetivo inicial de explorar o paralelismo suportado por múltiplos processadores. Por outro lado, a utilização de uma granulosidade fina pode levar à ocorrência de anomalias próprias da concorrência, como deadlocks e violações de atomicidade (high-level data races). Este artigo discute o conceito de fecho de um programa e uma metodologia que, quando aplicados em conjunto, permitem adaptar código legado para o tornar thread-safe, garantindo a ausência de violações de atomicidade na versão corrente do software e antecipando algumas violações de atomicidade que poderão ocorrer em versões futuras do mesmo software.

A set of methods defining an API (Application Programming Interface) are to be made thread safe; thus running any subset of these methods in parallel should not create races or deadlocks. Originally, the set of methods were not designed to be thread safe, so races and deadlocks are expected when running them in parallel. The number of possible interleavings when running methods from this API in parallel is huge, and this work focuses on the identification of the high level data races introduced by such interleavings. We propose an analysis that avoids the exhaustive exploration of all possible interleavings. For a concurrent program P, the closure of P, clos(P), is defined. Roughly speaking, we can say that the clos(P) is obtained by adding threads to P in such a way that high level data races resulting from running P in parallel to other programs are exposed statically. A set of methods representing the API is then modeled as a set of concurrent programs and their closure is analysed to identify high level data races. These high level data races are then inspected and removed to make the API thread safe. We illustrate the application of this methodology with a simple use case.

In this paper we present MoTh, a tool that uses static analysis to enable the automatic verification of concurrency anomalies in Transactional Memory Java programs. Currently MoTh detects high-level dataraces and stale-value errors, but it is extendable by plugging-in sensors, each sensor implementing an anomaly detecting algorithm. We validate and benchmark MoTh by applying it to a set of well known concurrent buggy programs and by close comparison of the results with other similar tools. The results achieved so far are very promising, yielding good accuracy while triggering only a very limited number of false warnings.

n/a

Transactional Memory allows programmers to reduce the number of synchronization errors introduced in concurrent programs, but does not ensures its complete elimination. This paper proposes a pattern matching based approach to the static detection of atomicity violation, based on a path-sensitive symbolic execution method to model four anomalies that may affect Transactional Memory programs. The proposed technique may be used to to bring to programmer's attention pairs of transactions that the programmer has mis-specified, and should have been combined into a single transaction. The algorithm first traverses the AST tree, removing all the non-transactional blocks and generating a trace tree in the path sensitive manner for each thread. The trace tree is a Trie like data structure, where each path from root to a leaf is a list of transactions. For each pair of threads, erroneous patterns involving two consecutive transactions are then checked in the trace tree. Results allow to conclude that the proposed technique, although triggering a moderate number of false positives, can be successfully applied to Java programs, correctly identifying the vast majority of the relevant erroneous patterns.

n/a

n/a

To provide high-level graphical support for PVM (Parallel Virtual Machine) based program development, a complex programming environment (GRADE) is being developed. GRADE currently provides tools to construct, execute, debug, monitor and visualise message-passing parallel programs. It offers high-level graphical programming abstraction mechanism to construct parallel applications by introducing a new graphical language called GRAPNEL. GRADE also provides the programmer with the same graphical user interface during the program design and debugging stages. A distributed debugging engine (DDBG) assists the user in debugging GRAPNEL programs on distributed memory computer architectures. Tape/PVM and PROVE support the performance monitoring and visualization of parallel programs developed in the GRADE environment.