Search

We present Konure, a new system that uses active learning to infer models of applications that retrieve data from relational databases. Konure comprises a domain-specific language (each model is a program in this language) and associated inference algorithm that infers models of applications whose behavior can be expressed in this language. The inference algorithm generates inputs and database contents, runs the application, then observes the resulting database traffic and outputs to progressively refine its current model hypothesis. Because the technique works with only externally observable inputs, outputs, and database contents, it can infer the behavior of applications written in arbitrary languages using arbitrary coding styles (as long as the behavior of the application is expressible in the domain-specific language). Konure also implements a regenerator that produces a translated Python implementation of the application that systematically includes relevant security and error checks. [ABSTRACT FROM AUTHOR]

Software errors and hardware failures can cause data structures in running programs to violate key data structure consistency properties. As a result of this violation, the program may produce unacceptable results or even fail. We present a new data structure repair system. This system accepts a specification of data structure consistency properties stated in terms of an abstract set- and relation-based model of the data structures in the running program. It then automatically generates a repair algorithm that, during the execution of the program, detects and repairs any violations of these constraints. The goal is to enable the program to continue to execute acceptably in the face of otherwise crippling data structure corruption errors. We have applied our system to repair inconsistent data structures in five applications: CTAS (an air traffic control system), AbiWord (an open source word processing program), Freeciv (an interactive multiplayer game), a parallel x86 emulator, and a simplified Linux file system. Our results indicate that the generated repair algorithms can effectively repair inconsistent data structures in these applications to enable the applications to continue to operate successfully in cases where the original application would have failed. Without repair, all of the applications fail. [ABSTRACT FROM AUTHOR]

Hob is a program analysis system that enables the focused application of multiple analyses to different modules in the same program. In our approach, each module encapsulates one or more data structures and uses membership in abstract sets to characterize how objects participate in data structures. Each analysis verifies that the implementation of the module 1) preserves important internal data structure consistency properties and 2) correctly implements a set algebra interface that characterizes the effects of operations on the data structure. Collectively, the analyses use the set algebra to 1) characterize how objects participate in multiple data structures and to 2) enable the interanalysis communication required to verify properties that depend on multiple modules analyzed by different analyses. We implemented our system and deployed several pluggable analyses, including a flag analysis plug-in for modules in which abstract set membership is determined by a flag field in each object, a PALE shape analysis plug-in, and a theorem proving plug-in for analyzing arbitrarily complicated data structures. Our experience shows that our system can effectively 1) verify the consistency of data structures encapsulated within a single module and 2) combine analysis results from different analysis plug-ins to verify properties involving objects shared by multiple modules analyzed by different analyses. [ABSTRACT FROM AUTHOR]

This article presents a novel framework for the symbolic bounds analysis of pointers, array indices, and accessed memory regions. Our framework formulates each analysis problem as a system of in- equality constraints between symbolic bound polynomials. It then reduces the constraint system to a linear program. The solution to the linear program provides symbolic lower and upper bounds for the values of pointer and array index variables and for the regions of memory that each statement and procedure accesses. This approach eliminates fundamental problems associated with applying standard fixed-point approaches to symbolic analysis problems. Experimental results from our implemented compiler show that the analysis can solve several important problems, including static race detection, automatic parallelization, static detection of array bounds violations, elimination of array bounds checks, and reduction of the number of bits used to store computed values. [ABSTRACT FROM AUTHOR]

Proposes adaptive replication for automatically eliminating synchronization bottlenecks in multithread programs that perform atomic operations on objects. Description of the concurrency model; Illustration of the issues associated with lock coarsening and adaptive replication; Presentation of the replication analysis and code generation algorithms; Overview of experimental results.

Presents a pointer analysis algorithm for structured parallel programs that may concurrently update shared pointers. Properties of the algorithm; Results of the multithreaded analysis of the algorithm; Uses foreseen for pointer analysis.

Presents information on a study which illustrated the application of dynamic feedback to measure the performance of different source code versions in computer systems organization. Summary of the analysis technique; Issues associated with synchronization optimizations and description of different policies; Issues affecting the performance impact of dynamic feedback.

This article describes a framework for synchronization optimizations and a set of transformations for programs that implement critical sections using mutual exclusion locks. The basic synchronization transformations take constructs that acquire and release locks and move these constructs both within and between procedures. They also eliminate, acquire and release constructs that use the same lock and are adjacent in the program. The article also presents a synchronization optimization algorithm, lock elimination, that uses these transformations to reduce the synchronization overhead. This algorithm locates computations that repeatedly acquire and release the same lock, then transforms the computations so that they acquire and release the lock only once. The goal of this algorithm is to reduce the lock overhead by reducing the number of times that computations acquire and release locks. But because the algorithm also increases the sizes of the critical sections, it may decrease the amount of available concurrency. The algorithm addresses this trade-off by providing several different optimization policies. The policies differ in the amount by which they increase the sizes of the critical sections. Experimental results from a parallelizing compiler for object-based programs illustrate the practical utility of the lock elimination algorithm. For three benchmark applications, the algorithm can dramatically reduce the number of times the applications acquire and release locks, which significantly reduces the amount of time processors spend acquiring and releasing locks. The resulting overall performance improvements for these benchmarks range from no observable improvement to up to 30% performance improvement. Copyright © 1999 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]

Examines the capacity of Jade computer program language. Three concepts of Jade; Implementation of the program language; Advantages of the program language; Features.

Analyzes data structures for parallel processing compilers. Utilization of data dependence analysis to detect independent computations; Key to dynamic, pointer-based computations; Advantages of commutativity analysis; Performance results for parallelized versions of scientific computations.

This paper presents our experience developing applications in Jade, a portable, implicitly parallel programming language designed for exploiting task-level concurrency. Jade programmers start with a program written in a standard serial, imperative language, and then use Jade constructs to describe how parts of the program access data. The Jade implementation analyzes this information to automatically extract the concurrency and execute the program in parallel. The resulting parallel execution is guaranteed to preserve the semantics of the serial program. We have implemented Jade as an extension to C on shared-memory multiprocessors, a homogeneous message-passing machine and networks of heterogeneous workstations. To evaluate Jade, we obtained several complete scientific and engineering applications and parallelized them using Jade. We then executed these applications on several computational platforms. We use this applications experience to evaluate Jade with respect to two properties: how well Jade supports the process of writing parallel programs and how well the resulting programs perform. Our applications experience shows that the current version of Jade is a qualified success. For all but one application the use of Jade entails limited programming overhead. The coarse-grain computations perform very well, with the dynamic Jade overhead having no significant impact on the performance. The finer-grain computations suffer from some Jade-specific performance problems, but some of these could be eliminated with a more advanced Jade implementation. © 1998 John Wiley & Sons, Ltd. [ABSTRACT FROM AUTHOR]