PARFORMAN-an assertion language for specifying behaviour when debugging parallel applications
Mikhail Auguston, Peter Fritzson · 2002
PARFORMAN (PARallel FORMal ANnotation language) is a specification language for expressing the intended behaviour or known types of error conditions when debugging or testing parallel programs. The high-level debugging approach which is supported by PARFORMAN is model-based. Models of intended or faulty behaviour can be succinctly specified in PARFORMAN. These models are then compared with the actual behaviour in terms of execution traces of events, in order to localize possible bugs. PARFORMAN is based on an axiomatic model of target program behaviour. This model, called H-space (history-space), is formally defined through a set of general axioms about three basic relations between events. Events may be sequentially ordered, they may be parallel, or one of them might be included in another composite event. The notion of an 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. In addition to debugging and testing, PARFORMAN can also be used to specify profiles and performance measurements.>