João Lourenço

This paper describes our experience with the design and implementation of a distributed debugger for C/PVM programs within the scope of the SEPP and HPCTI Copernicus projects. These projects aimed at the development of an integrated parallel software engineering environment based on a high-level graphical parallel programming model (GRAPNEL) and a set of associated tools supporting graphical edition, compilation, simulated and real parallel execution, testing, debugging, performance monitoring, mapping, and load balancing. We discuss how the development of the debugging tool was strongly influenced by the requirements posed by other tools in the environment, namely support for high-level graphical debugging of GRAPNEL programs, and support for the integration of static and dynamic analysis tools. We describe the functionalities of the DDBG debugger and its internal architecture, and discuss its integration with two separate tools in the SEPP/HPCTI environment: the GRED graphical editor for GRAPNEL programs, and the STEPS testing tool for C/PVM programs.

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.

This paper presents an automatic verification technique for transactional memory Java programs executing under snapshot isolation level. We certify which transactions in a program are safe to execute under snapshot isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements. Our work builds on a novel deep-heap analysis technique based on separation logic to statically approximate the read- and write-sets of a transactional memory Java program. We implement our technique and apply our tool to a set of micro benchmarks and also to one benchmark of the STAMP package. We corroborate known results, certifying some of the examples for safe execution under snapshot isolation by proving the absence of write-skew anomalies. In other cases our analysis has identified transactions that potentially trigger previously unknown write-skew anomalies.>