Summary of Research
The use of quantitative modelling techniques in Computer Science has grown
rapidly in the last ten years, largely thanks to stochastic extensions
of many traditional formalisms, such as process algebra and Petri nets.
In particular, the Performance Evaluation Process Algebra (PEPA) 
has been highly successful, due to its compositionality, straightforward
semantics and large tool-base. However, the current approaches to formal
analyses of large-scale distributed systems all involve direct use of
such abstract modelling languages. This leads to the question of how
to relate such models to the implementations of the systems they concern.
In particular, we wish to investigate techniques for analysing the program
code directly; in other words, the ability to automatically derive a
stochastic model from the code.
world of qualitative model checking, there have been great advances
to this end. The work on SLAM  at Microsoft Research is a prime example
of this, leading to the release of the Static Driver Verifier as a practical
tool. Using predicate abstraction, they produce a highly abstract model,
which is then iteratively refined with the aid of counter-examples from
the concrete program. This works because the properties concern just
possibilities of certain behaviours, rather than probabilities,
or durations. The challenge we face is to develop corresponding techniques
that can be applied in a quantitative setting.
our immediate goal is to derive a PEPA model that represents the performance
characteristics of a program, we must stress that this is not the ultimate
aim of the research (although it is an essential part of it). A model
is only as good as the analysis it can undergo, and its structure will
vary depending on the properties we are interested in. We must therefore
be careful to guide the model extraction with respect to its intended
analysis, and also relate the results of this analysis back to the original
program. Bearing this in mind, we can divide the process into four distinct
phases; namely instrumentation, abstraction, refinement and analysis.
To begin with, there is too little information in a program to decide the purpose of the model. Therefore we must start by instrumenting the code, annotating the important elements of its state so that we can refer to them in the model. We can then compute relevant performance properties by assigning rewards to these states. Furthermore, we need an abstract interface for our code, to avoid analysing unnecessary details such as library and system calls. It is therefore vital for us to develop an appropriate framework for these annotations.
challenge when dealing with real code is how to manage the size of its
state space. To do this, we need to develop abstractions with
which we can calculate the probabilities of control-flow decisions (branches).
In particular, it is vital that we can bound the error in our approximations.
Predicate abstraction is useful for handling discrete state elements
(such as binary flags, or enumeration types), but not in general for
integer variables. On the other hand, certain classes of variable, such
as loop counters, are readily modelled using intervals. Determining
the most appropriate abstraction for each variable, and reasoning about
the errors involved, is one of the most important challenges we face.
flow abstraction is similarly important, for which static analysis techniques
are required. In particular, great care must be taken when assuming
independence between variables. At present, path-based abstractions
look to be promising, but we must investigate this more thoroughly.
There is some (though surprisingly little) relevant work from the branch
prediction community, such as value-range propagation , which
provides a good starting point for deriving intervals for local variables.
SLAM, we have no obvious way in which to add more detail to an over-simplified
model, since altering any one probability (or rate) affects the entire
model’s behaviour. Instead, we need to take the opposite view of
refinement, by increasingly simplifying a detailed initial model.
The only way to handle such a large model to begin with is by exploiting
its structure. Remaining in the process algebra representation (and
so avoiding expansion of cooperation points), we have a number of potential
techniques for refinement. Structurally, we can split the model at interaction
points, using response time approximation  to analyse one
side at a time. Behaviourally, we can look for quasi-lumpable
states, or perform time scale decomposition  to separately
treat fast and slow activity rates. We need to investigate the utility
of these methods, and if necessary develop more appropriate refinement
advantage of using PEPA as our modelling language is its alternative
semantics. Traditionally, a PEPA process maps onto a Continuous Time
Markov Chain (CTMC), but the size of this grows exponentially in the
number of concurrent processes. More recent work, in , describes
how to map a process onto a set of ordinary differential equations (ODEs).
This avoids the state space explosion problem by recording just the
number of processes in each local state, rather than the detailed
state of the entire system. This is particularly useful for analysing
the large-scale behaviour when many components interact.
we are interested in application domains such as communications protocols,
it is important to deal with real-world programming languages such as
C. Thankfully, there exist tools such as CCured  and the C Intermediate
Language (CIL) , which provide a type-safe framework for analysis.
of this research would lead to a great many applications. A practical
tool would considerably widen the application of performance analysis
techniques, and could significantly improve upon current methods for
non-functional testing. Indeed, the ability to track performance criteria
from the design stage through the entire development, without having
to maintain a separate model, would be invaluable. Furthermore, the
use of performance contracts is of great interest to many application
domains, such as web services, which would welcome a tool for deriving
the resource-usage distributions of code in different contexts.
is certainly a significant gap in the current research, which we hope
this work can fill. We believe that now is the time to bring existing
work together, to allow quantitative, and not just qualitative, model
checking of real code.
Hillston. A Compositional Approach to Performance Modelling.
Cambridge University Press, 1996.
Ball and S. K. Rajamani. The SLAM toolkit. In Proceedings of CAV
R. C. Patterson. Accurate static branch prediction by value range propagation.
In SIGPLAN Conference on Programming Language Design and Implementation,
Mertsiotakis. Approximate Analysis
Methods for Stochastic Process Algebras. PhD thesis, Institut für
Mathematische Maschinen und Datenverarbeitung, 1998.
Hillston. Fluid flow approximation of PEPA models. In Proceedings
of the Second International Conference on the Quantitative Evaluation
of Systems, 2005.
C. Necula, S. McPeak and W. Weimer. CCured: Type-safe retrofitting of
legacy code. In Proceedings of POPL 2002.
 G. C. Necula, S. McPeak, S. P. Rahul and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proceedings of Conference on Compiler Construction, 2002.