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) [1] 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.

In the world of qualitative model checking, there have been great advances to this end. The work on SLAM [2] 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.

Whilst 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.

The biggest 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.

Control 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 [3], which provides a good starting point for deriving intervals for local variables.

Unlike 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 [4] to analyse one side at a time. Behaviourally, we can look for quasi-lumpable states, or perform time scale decomposition [4] to separately treat fast and slow activity rates. We need to investigate the utility of these methods, and if necessary develop more appropriate refinement techniques.

One important 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 [5], 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.

Since 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 [6] and the C Intermediate Language (CIL) [7], which provide a type-safe framework for analysis.

The success 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.

There 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.

[1] J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.

[2] T. Ball and S. K. Rajamani. The SLAM toolkit. In Proceedings of CAV 2001.

[3] J. R. C. Patterson. Accurate static branch prediction by value range propagation. In SIGPLAN Conference on Programming Language Design and Implementation, 1995.

[4] V. Mertsiotakis. Approximate Analysis Methods for Stochastic Process Algebras. PhD thesis, Institut für Mathematische Maschinen und Datenverarbeitung, 1998.

[5] J. Hillston. Fluid flow approximation of PEPA models. In Proceedings of the Second International Conference on the Quantitative Evaluation of Systems, 2005.

[6] G. C. Necula, S. McPeak and W. Weimer. CCured: Type-safe retrofitting of legacy code. In Proceedings of POPL 2002.

[7] 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.