Narrow Results

PARFORMAN (PARallel FORMal ANnotation language) is a high-level specification language for expressing intended behavior or known types of error conditions when debugging or testing parallel programs. Models of intended or faulty target program behavior can be succinctly specified in PARFORMAN. These models are then compared with the actual behavior in terms of execution traces of events, in order to localize possible bugs. PARFORMAN can also be used as a general language for expressing computations over target program execution histories.

PARFORM AN is based on a precise model of target program behavior. This model, called H-space (History-space), is formally defined through a set of general axioms about three basic relations, which may or may not hold between two arbitrary events: they may be sequentially ordered (SEQ), they may be parallel (PAR), or one of them might be included in another composite event (IN).

The general notion of composite event is exploited systematically, which makes possible more powerful and succinct specifications. The notion of event grammar is introduced to describe allowed event patterns over a certain application domain or language. Auxiliary composite events such as Snapshots are introduced to be able to define the notion “occurred at the same time” at suitable levels of abstraction. Finally, patterns and aggregate operations on events are introduced to make possible short and readable specifications. In addition to debugging and testing, PARFORMAN can also be used to specify profiles and performance measurements.

We propose a systematic approach for design and validation of error detection software. Formally, the semantic of a specification is represented by a transition system. This representation is then used to generate a flowgraph or ddgraph which is used to construct an execution path tree. The information obtained from this algorithm representation is used to aid in the design of software-based fault detection techniques for hardware faults.

Flowgraph and ddgraph representations provide information to predict future program flow. During execution, the current program path is recorded, along with the expected path. Checks are placed to verify that the program path follows the predicted path.

Algorithm-based fault tolerance (ABFT) techniques are used to detect data structure corrupting faults and to improve the fault coverage. Fault coverage provided by this approach for different types of hardware faults has been estimated through experiments with the software-based fault injection tool (SOFIT) and the data is presented to demonstrate the effectiveness of the method.