Introduction

In this chapter an alternative notion of equivalence for PEPA components is developed. This equivalence, strong equivalence, is defined in Section 8.2. It is developed in the style of Larsen and Skou's probabilistic bisimulation which was discussed in Section 5.2.3. Here transition rates, already embedded in the PEPA labelled transition system as activity rates, are used instead of probabilities. As with strong bisimulation the relation aims to capture a notion of equivalent behaviour between components. However, observation now occurs without detailed knowledge of the individual transitions involved. Strong equivalence, unlike strong bisimulation, is unable to distinguish between a single (α, 2r) activity and two simultaneously enabled instances of the (α, r) activity.

Some properties of the relation from a process algebra perspective are examined in Section 8.3. Like strong bisimulation, strong equivalence is found to be a congruence relation for PEPA. In Section 8.4 we discuss some of the implications of strong equivalence for the system components being represented, and in Section 8.5 the implications for the underlying Markov processes are reviewed. Finally, in Section 8.6, we outline the use of strong equivalence as a state-to-state equivalence forming the basis of exact aggregation. An alternative approach to the generation of the Markov process underlying a PEPA model is also discussed. These ideas are illustrated in Section 8.6.3 with an example taken from Section 4.4.4.

Consider a communication network in which processors want to transmit many short messages to each other. The processors are not necessarily connected by a communication channel. Usually this service is provided for by protocols in the transport layer. A protocol can incorporate such a message in a packet and send the packet to the destination processor. As discussed in chapter 1, in the transport layer it is again necessary that communication errors are considered, even though we can assume that the communication over channels is handled correctly by the lower layers. -Thus we have to assume that the communication network can lose packets, copy packets (due to necessary retransmissions), delay packets arbitrarily long, and deliver packets in a different order than the order in which they were sent.

We consider the design of some protocols that handle the communication of messages correctly, in the sense that there is no loss or duplication of messages (cf. Belsnes [Bel76]). To specify this more precisely, suppose processor i wants to transmit a message m to processor j. The message m is said to be lost if i thinks that j received m while this is not the case, and m is said to be duplicated if j receives two or more copies of m from i and thinks that they are different messages.

If a processor i has a message or a sequence of messages to send to j, it sets up a temporary connection with j, which is closed as soon as i knows that j received the message(s) (or that j is not in a position to receive them).

Introduction

In this chapter we present a modelling study demonstrating the use of PEPA for performance evaluation. Examples drawn from the modelling study will be used to exhibit the model simplification techniques developed later in the thesis. This study considers and compares various multi-server multi-queue systems. Such systems, an extension of the traditional polling system, have been used to model applications in which multiple resources are shared among several users, possibly with differing requirements. Examples include local area networks with multiple tokens, and multibus interconnection networks in distributed systems. Similar systems have been investigated in [26, 84, 85, 86, 87, 88].

A polling system consists of several queues and a single server which moves round the queues in cyclic order. These systems have been found to be good models of many systems which arise in computer network and communication scenarios, and consequently they have been extensively studied. A recent survey by Takagi [89] references over four hundred contributions.

A variety of extensions and modifications to the traditional polling system have been investigated [89], including non-cyclic polling, priority queues, and queues with feedback. One extension which is particularly suited to modelling innovative local area networks is the introduction of additional servers, each of which moves around the queues providing service where it is needed. These systems, sometimes known as multi-server multi-queue systems, are not readily amenable to queueing theory solution. Several suggested approximation techniques, based on queueing theory, and exact solutions based on GSPNs are reviewed in Section 4.3.1.

Introduction

This chapter presents the Performance Evaluation Process Algebra (PEPA). This language has been developed to investigate how the compositional features of process algebra might impact upon the practice of performance modelling. Section 3.2 outlines the major design objectives for the language. Most of the rest of the chapter is taken up with the subsequent informal and formal descriptions of the language, and a description of its use as a paradigm for specifying Markov models. Some simple examples are presented to introduce the reader to the language and its use in describing systems. This establishes PEPA as a formal system description technique. Presentation of more complex examples is postponed until Chapter 4.

The use of PEPA for performance modelling is based on an underlying stochastic process. It is shown that, under the given assumptions, this stochastic process will be a continuous time Markov process. Generating this Markov process, solving it and using it to derive performance results are presented and illustrated by a simple example. The relationship between PEPA and established performance modelling paradigms is discussed in Section 3.6.

Design Objectives for PEPA

An objective when designing a process algebra suitable for performance evaluation has been to retain as many as possible of the characteristics of a process algebra whilst also incorporating features to make it suitable for specifying a stochastic process.

In this chapter we consider some link-level protocols and show their partial correctness by assertional verification. Link-level protocols, i.e., protocols residing in the data link layer, are designed to control the exchange of information between two computing stations, e.g. computers or processors over a full-duplex link. They should guard against the loss of information when the transmission medium is unreliable. We only discuss transmission errors that occur while the link is up, and thus use the model of a static network consisting of two nodes i and j, and a bidirectional link (i, j). We will not deal with the problems caused by links or nodes going down, nor with the termination of a protocol. In a different context, these issues will be dealt with in later chapters.

In section 2.1 we discuss a generalization of the sliding window protocol. This protocol is meant to control the exchange of messages in an asynchronous environment. Although sliding window protocols belong to the data link layer, we will see in chapter 4 that the generalization can also be used as a basis for connection management, which belongs to the transport layer. We show that the alternating bit protocol and the “balanced” two-way sliding window protocol are instances of this one general protocol skeleton, that contains several further parameters to tune the simultaneous transmission of data over a full-duplex link. After proving the partial correctness of the protocol skeleton, we discuss the dependence of the optimal choice of the parameters on the propagation delay of the link, the transmission speed of the senders, and the error rate of the link.

In the past two decades, distributed computing has evolved rapidly from a virtually non-existent to an important area in computer science research. As hardware costs declined, single mainframe computers with a few simple terminals were replaced by all kinds of general and special purpose computers and workstations, as the latter became more cost effective. At many sites it became necessary to interconnect all these computers to make communication and file exchanges possible, thus creating a computer network. Given a set of computers that can communicate, it is also desirable that they can cooperate in some sense, for example, to contribute to one and the same computation. Thus a network of computers is turned into a distributed system, capable of performing distributed computations. The field of distributed computing is concerned with the problems that arise in the cooperation and coordination between computers in performing distributed tasks.

Distributed algorithms (or: protocols) range from algorithms for communication to algorithms for distributed computations. These algorithms in a distributed system appear to be conceptually far more complex than in a single processing unit environment. With a single processing unit only one action can occur at a time, while in a distributed system the number of possibilities of what can happen when and where at a time tends to be enormous, and our human minds are just not able to keep track of all of them.

This leads to the problem of determining whether the executions of a distributed algorithm indeed have the desired effect in all possible circumstances and combinations of events. Testing algorithms has now become completely infeasible: some form of “verification” is the only way out.

Introduction

In this chapter we develop a very strong notion of equivalence between PEPA components called isomorphism. This is a condition on the derivation graphs of components and it ensures that components are only considered equivalent if there is a one-to-one correspondence between their derivatives and they are capable of carrying out exactly the same activities. It is not an observation based notion of equivalence in the style of bisimulation which is usual for process algebras. It is structural, in the style of the equivalence between Markov processes introduced in Section 5.3. Isomorphism is defined in Section 6.2.

In Sections 6.3 to 6.5 we examine some properties of this notion of equivalence, from the perspectives of a process algebra, the modelled system components and the underlying Markov processes. As we might expect from such a strong notion of equivalence, we can derive strong properties for isomorphism. The relation is a congruence for PEPA. The relationship between isomorphism and the Markov processes underlying the PEPA components is found to be a close one—isomorphic components generate equivalent Markov processes.

In the remainder of the chapter we develop a weaker form of this equivalence called weak isomorphism. This equivalence reflects the hidden nature of τ type activities. We will consider two components equivalent in this way if they only differ in their capabilities to carry out such activities. A definition of this notion of equivalence is presented in Section 6.6.

This book is, in essence, the dissertation I submitted to the University of Edinburgh in early January 1994. My examiners, Peter Harrison of the Imperial College, and Stuart Anderson of the University of Edinburgh, suggested some corrections and revisions. Apart from those changes, most chapters remain unaltered except for minor corrections and reformatting. The exceptions are the first and final chapter.

Since the final chapter discusses several possible directions for future work, it is now supplemented with a section which reviews the progress which has been made in each of these directions since January 1994. There are now many more people interested in stochastic process algebras and their application to performance modelling. Moreover, since these researchers have backgrounds and motivations different from my own some of the most interesting new developments are outside the areas identified in the original conclusions of the thesis. Therefore the book concludes with a brief overview of the current status of the field which includes many recent references. This change to the structure of the book is reflected in the summary given in Chapter 1. No other chapters of the thesis have been updated to reflect more recent developments. A modified version of Chapter 8 appeared in the proceedings of the 2nd International Workshop on Numerical Solution of Markov Chains, January 1995.

I would like to thank my supervisor, Rob Pooley, for introducing me to performance modelling and giving me the job which brought me to Edinburgh initially.

In this chapter, we provide a result which characterizes well-formedness of free-choice nets in a very suitable way for verification purposes. All the conditions of the characterization are decidable in polynomial time in the size of the net. The most interesting feature of the result is that it exhibits a tight relation between the well-formedness of a free-choice net and the rank of its incidence matrix. Accordingly, it is known as the Rank Theorem. It will be an extremely useful lemma in the proof of many results of this chapter and of the next ones.

We also provide a characterization of the live and bounded markings of a well-formed free-choice net. Again, the conditions of the characterization can be checked in polynomial time. Together with the Rank Theorem, this result yields a polynomial time algorithm to decide if a given free-choice system is live and bounded.

In the last section of the chapter we use the Rank Theorem to prove the Duality Theorem. This result states that the class of well-formed free-choice nets is invariant under the transformation that interchanges places and transitions and reverses the arcs of the net.

Characterizations of well-formedness

Using the results of Chapter 4 and Chapter 5, it is easy to obtain the following characterization of well-formed free-choice nets.

Proposition 6.1A first characterization of well-formedness

Let N be a connected free-choice net with at least one place and at least one transition.

1. N is structurally live iff every proper siphon contains a proper trap.

2. […]