Toward a Performance Evaluation Methodology for the Pi-Calculus Family of Formal Modeling Languages

Abstract

Toward a Performance Evaluation Methodology for the Pi-Calculus Family of Formal Modeling Languages

Process calculi are tools capable of modeling large distributed systems of concurrent processes and among them Pi-calculus, introduced by Milner et al. in 1992 [3], is one of the most popular ones. Pi-calculus can be used to model modern concurrent systems ranging from the lowest level in software design, procedural programming, to the highest level, component composition and abstraction ([4] and [9]). The Pi-calculus has aroused intensive interests in researchers to study its applicability, extensibility, and other properties. For example, it has been shown that Pi-calculus is powerful enough to model various data structures, object-oriented programs, and communication systems. It is also the basis of several experimental programming languages such as Pict [5], Join [2], and TyCO [12], etc. The Pi-calculus is a calculus where both communication and configuration are primitives [3] and has been successfully used to model features of object-oriented programming languages [13].

My experience supports the fact that the Pi-calculus is a promising formal foundation for modeling concurrent objects ([6] and [11]) and for the definition of higher-level, reusable synchronization abstractions [10]. Other research initiatives have proven that the Pi-calculus can be used to effectively and precisely specify the configuration and behavior of concurrent programs and to deduce their behavioral properties [8]. With all the advantages that Pi-calculus offers, it does not provide any formal method to be used for performance evaluation of systems it describes. In this editorial, I present a direction for the design and implementation of a performance evaluation module by using the Markov Chain and Markov Reward Model [1].

To be able to construct a Markov Chain for a formally described system, we plan to expand the Pi-calculus by adding some performance primitives and associating performance parameters with each action that takes place internally in a system. These include actions such as sending and receiving messages from one component to another component. By using such parameters, designers can benchmark their component-oriented units and compare the performance of different architectures against one another.

Markov Chain (MC) was introduced by A. A. Markov in 1907 and has been in use for performance analysis since 1950. A Markov chain consists of a set of states and a set of labeled transitions between these states and is a sequence of random values whose probabilities at a time interval depend upon the values at the previous states. There exist two types of Markov Chains: Continuous-Time Markov Chains (CTMCs) and Discrete-Time Markov Chains (DTMCs). CTMCs are distinct from DTMCs in the sense that state transitions may occur at anytime and not merely at fixed, discrete time points, as is the case with DTMCs. More information about Markov Chains can be found in [1].

By proving that a system modeled by Pi-calculus (or an extension of it) is CTMC, the performance evaluation methodology could be built using Markov Chains theory. The steps needed to be taken for MC-based performance evaluation of a formal model described in Pi-calculus or its extensions are projected to be as follow:

1. Forming the state diagram of the system (based on MC theory): To do so, we consider the original system expression in Pi-calculus to represent the initial state of the system. Every reduction applied to the initial system expression would produce a possible next state.
2. Utilizing the state transition rate functions to calculate the rate for each transition: The transition rate function is defined as the total number of the transitions in the unit time. From [1] we know that the state sojourn times of a homogeneous CTMC must have the memory less property (does not remember the previous states). Since the exponential distribution is the only continuous distribution with this property, the random variables denoting the sojourn times (ti), also called holding times, must be exponentially distributed. If ri denotes the ith transition rate, it obviously follows that ri = 1/ ti. Therefore, for the purpose of this development, ti is based on the exponential distribution with the parameter (λ) equal to ri.
3. By associating each rate with its appropriate transition in the state diagram, the Markov Chain diagram would be formed.
4. If it is an ergodic Markov Chain, defined in (Bolch 1998), the steady probability of each state (π) could be found by solving the equation: π*Q=0, where Q is the infinitesimal generator matrix, defined in (Bolch 1998). The final performance value of the system would be equal to , where ri and πi are the reward and the steady probability for the state Si.
5. If it is not an ergodic Markov Chain, which means the system will eventually stop at some certain states, then the reward will be assigned for each transition separately. In this case, we can only calculate the performance of the system executing from one state to another.

By utilizing Markov state-based and transition-based reward models, performance evaluation can be executed for systems described in Pi-calculus or its extensions. The performance evaluation module could be integrated into a visualization tool, such as ACVisualizer [7], so the user, after visualizing component composition, can verify the model and evaluate its performance against other architectures before finalizing the design for implementation.

Here is a basic example to illustrate the above steps. In this example, a system is composed from two main components: a Memory and a Processor. The memory unit waits on the channel to receive an address and then uses another channel to send the data out. The processor sends an address to the memory, waits for the data to be received and then continues executing the instruction (τ):

Mem≡req(addr).ans〈data〉.Mem
Processor≡req〈addr〉.ans(data).τ.Processor

According to the first step, described above, we first have to reduce the model step by step using Pi-calculus reduction rules. Each reduction step introduces a state which can be used to form the state diagram in figure 1a. In this figure:

S1≡req(addr).ans〈data〉.Mem|req〈addr〉.ans(data).τ.Processor

S2≡ans〈data〉.Mem|ans(data).τ.Processor

S3≡Mem|.τ.Processor

(a)

(b)

Figure 1. a) the State Diagram b) an ergodic Markov Chain

The speed of sending and receiving data between the processor and the memory depends on the bandwidth of the bus (noted as bwbus). So we use 1/ bwbus to denote the communication cost between the processor and the memory (based on step 2). The cost of executing the action τ is denoted as 1/fe where fe is the clock frequency of the chipset. Based on this information, the state diagram can be transferred to the ergodic Markov Chain in figure 1b (step 3).

From step 4, suppose the steady probability vector is π=[π1, π2, π3]. From figure 1b, we know the infinitesimal generator matrix is:

Since π*Q=0 and π1+π2+ π3=0, we can calculate π:

Suppose we want to evaluate the throughput of the system, then the rewards for states S1, S2 and S3 are 0, 0, 1. The final performance equation, based on step 4 is:

which, if given the numerical values for bwbus and fe, can provide the calculated throughput of the system.

In summary, with all the advantages that utilization of a formal modeling tool may offer to the design and implementation of a sound and solid distributed system, the lack of a formal infrastructure for performance evaluation compromise its practical utilization. Although the Pi-calculus family of formal languages is vastly utilized, it does not provide any native theoretical mechanisms for performance evaluation of different design approaches for a particular system. This deficiency makes Pi-calculus incapable in assisting the user with design-for-performance which is a crucial component of practical application development. This editorial plots a path to address this need in Pi-calculus.

References:

[1] Bolch G., Greiner S., Meer H., and Trivedi K. S., (1998): Queuing Networks and Markov Chains Modelling and Performance Evaluation with Computer Science Applications, Wiley, New York.Borland International (1995), Delphi Benutzerhandbuch.

[2] Fournet C., and Maranget L., (1997): The Join-Calculus Language (release 1.05), http://moscova.inria.fr/join/manual/index.html, Institut National de Recherche en Informatique et Automatique.

[3] Milner R., Parrow J. and Walker D. (1992): A calculus of mobile processes (Parts I and II), Information and Computation, vol. 100, no. 1, pp. 1–77.

[4] Milner R., (1999): Communication and Mobile Systems: The π-Calculus, Cambridge University Press, Cambridge, UK.

[5] Pierce B., and Turner D., (2000): Pict: A programming language based on the Pi-calculus, In Proof, Language and Interaction, MIT Press.

[6] Rahimi S., (2003): Using Api-Calculus for Formal Modeling of SDIAgent, a Multi-Agent Distributed Geospatial Data Integration System, Journal of Geographic Information and Decision Analysis, ISSN 1480–8943, vol. 7, No. 2, pp. 132–149.

[7] Rahimi S. and Ahmad R., (2006): ACVisualizer: A Visualization Tool for API-Calculus, to appear in Multi-Agent and Grid Systems, 2006.

[8] Radestock M. and Eisenbach S., (1994): What do you get from a pi-calculus semantics? Proceedings of Parallel Architectures and Languages Europe (PARLE '94), LNCS 817, pp. 635–647. Springer.

[9] Sangiorgi D. and Walker D., (2001): The π-calculus: A Theory of Mobile Processes, Cambridge University Press, Cambridge UK.

[10] Schneider J. and Lumpe M., (1997): Synchronizing Concurrent Objects in the Pi-Calculus, Proceedings of Languages and Models with Objects '97, Brest.

[11] Shaw M. and Garlan D., (1996): Software Architecture: Perspectives on an Emerging Discipline, Prentice Hall.

[12] Vasconcelos V. and Bastos R., (1998): The TyCO Programming Language, http://www.ncc.up.pt/~lblopes/tyco/.

[13] Walker D., (1995): Objects in the Pi-Calculus, Information and Computation, vol. 116, no. 2, pp. 253–271.

Shahram Rahimi,
Department of Computer Science
Southern Illinois University.