FREE ELECTRONIC LIBRARY - Thesis, documentation, books

Pages:   || 2 | 3 |

«A Design Strategy for Deadlock-Free Concurrent Systems J.M.R.Martin Oxford University Computing Services, 13 Banbury Road, Oxford OX2 6NN, UK ...»

-- [ Page 1 ] --


A Design Strategy for Deadlock-Free

Concurrent Systems


Oxford University Computing Services, 13 Banbury Road, Oxford OX2 6NN, UK


Computing Laboratory, The University, Canterbury, Kent, CT2 7NF, UK


When building concurrent systems, it would be useful to have a collection of reusable processes

to perform standard tasks. However, without knowing certain details of the inner workings of these components, one can never be sure that they will not cause deadlock when connected to some particular network.

Here we describe a hierarchical method for designing complex networks of communicating processes which are deadlock-free. We use this to define a safe and simple method for specifying the communication interface to third party software components. This work is presented using the CSP model of concurrency and the occam2.1 programming language.

KEY WORDS deadlock livelock design concurrency reuse components networks CSP occam


Code reusability is an important consideration in large-scale system design. It is an issue which modern programming languages are expected to address. In the concurrent programming language, occam2.1 [1], arbitrarily complex subnetworks of processes may be concealed within a single process definition. The internal structure of such a process may be changed independently from any network in which it is embedded. This is extremely useful for a number of reasons. However, in the context of concurrent systems, it is also potentially dangerous. Unless we know their internal details, how can we be sure that a program which incorporates these components is not prone to deadlock?

Deadlock is a major problem with parallel programming. Safety critical systems must be guaranteed deadlock-free, but this is not an easy task. In [2] and [3] it is shown how to tackle this problem using software design rules. By placing minor restrictions on the manner in which concurrent systems are constructed, it is possible to remove completely the spectre of deadlock. Proofs of deadlock-freedom for networks of arbitrary size are reduced to simple checks for local conditions of processes, and topological properties of the network configuration.

In this paper we shall build on that work to show how deadlock-free networks may be built hierarchically, incorporating reusable components. This provides an efficient method for modular programming in occam2.1 that offers security guarantees that are very difficult to obtain from traditional approaches to concurrent system design.

CCC 1070–454X/97/030001–18 Received 7 March 1996 c 1997 by John Wiley & Sons, Ltd. Revised 15 January 1997 2 J.M.R. MARTIN and P.H.WELCH In section 2 we describe the deadlock analysis terminology of Roscoe and Dathi, which is built upon the firm mathematical foundations of CSP. In section 3 we present a formal definition of the client-server protocol which has previously existed only as a collection of informal rules, potentially open to misinterpretation. We then prove a theorem about how this protocol may be used to build deadlock-free networks and illustrate this by two examples: an occam2.1 process farm and a message router. In section 4 we show how to use the client-server protocol to build deadlock-free networks hierarchically from composite sub-components. This is important for the design of large systems.

There are certain other design techniques which are known to yield deadlock-free concurrent systems. In section 5 we describe a technique for integrating subnetworks built by different methods into a client-server system. Section 6 looks at the related issues of divergence-freedom and starvation-freedom and section 7 describes ongoing research.


The deadlock problem has proved a popular area of research for many years. The early results are largely informal, and suffer from the lack of a suitable underlying mathematical model. This problem was remedied in 1986 by A.W.Roscoe and N.Dathi [4] who provided a powerful suite of tools for deadlock analysis, based on CSP – the mathematical language for reasoning about concurrent systems [5]. This enabled much of the earlier work to be formalised. We shall now describe their terminology.

With each CSP process P is associated an alphabet, P, the set of actions that P may perform. The observable behaviour of P is described by its failures and divergences. A failure of P consists of a pair (s, X) where s is a possible trace of events that P may perform, and X is a refusal set of P=s – a set of events which if offered to P after it has performed trace s, might be completely refused. A divergence of P is a trace s after which P may indulge in an infinite series of concealed actions. A glossary of CSP operators used in this paper is given in Figure 1.

Of particular importance for deadlock analysis are the maximal refusal sets of a process, as the more events that are refused the more likely is deadlock to occur. We define the set of maximal failures of P as those failures (s, X) of P where the refusal set X is maximal, i.e.

–  –  –

After it has performed event a, Q can refuse fg, fag, fbg, fcg, fa, bg, or fa, cg. Its maximal refusals at this stage are fa, bg and fa, cg, which correspond to the two states that the process may be in once it has decided which branch of the u construct to take: either it decides to behave like b ! Q or it decides to behave like c ! Q. These are called stable states of Q because once they are entered no internal activity is possible, at least until an external event has been performed. Before making the decision as to which branch of the u construct to take, Q is said to be in an unstable state. For the purpose of deadlock analysis, unstable

–  –  –

states are irrelevant, as a system in such a state is yet to come to rest – when a system is deadlocked there can be no activity at all.

Consider a network V of CSP processes, hP1, : :, PN i, composed in parallel. Events which lie in the alphabet of two processes of V require their simultaneous participation, and this is the means of communication within the network. It is assumed that the network is tripledisjoint – i.e. there is no event which is shared by more than two process alphabets. It is also assumed that the network is busy – i.e. each process Pi is non-terminating and individually free of both deadlock and divergence. (It is reasonably straightforward to extend the model to allow for process termination, if required. See [6] for details.) The behaviour of a network is described in terms of a set of states that it may be in. A state of V consists of a trace of events s together with a tuple of refusal sets hX1, : :, XN i such that, for all i, (s j` Pi, Xi ) is a maximal failure of Pi. It represents a set of events in which each process may refuse to engage after they have collectively performed the sequence of events in s.

In a deadlock state every event is refused by some process, i.e.


–  –  –

A network which has no deadlock states is said to be deadlock-free.

In any state = (s, hX1, : :, XN i), if there is a process Pi which is ready to perform an event (or events) which lie in the vocabulary of another process Pj (i.e. ( Pi ; Xi ) \ Pj 6= fg), we say that Pi is making a request of Pj, and write

–  –  –

When a process has all its requests ungranted we say that it is blocked. In a deadlock state every process is blocked.


3.1 Client-Server Protocol A particularly flexible design rule for deadlock freedom is the Client-Server Protocol. This was originally formulated by P. Brinch Hansen [7] in the context of operating systems. It has since been adapted as a means of designing deadlock-free concurrent systems using occam2 (see [3]).

The basic idea is that a process communicates on each of its channels either as a client or as a server, according to a strict protocol. A network of client-server processes is deadlock-free if it has no cycle of client-server relationships.

The standard definition of the client-server protocol is both informal and intuitive. It runs as follows. If a client is waiting to communicate with a server, the server, ignoring possible indefinite delays whilst waiting to communicate as a client with another process, must eventually become ready to participate in that communication.

4/3/1997 16:59 PAGE PROOFS paper


Unfortunately this is too vague a condition to translate into a local specification of CSP processes. For instance consider a process that acts only as a server. In order to establish the above property we would need to show that any particular client request would eventually be granted. To do this we would need to analyse the way in which the process interacts with each of its other clients and possibly also how they interact with each of their clients in turn. Here we introduce a formal definition which is slightly more restrictive than the informal one, yet with the distinct advantage of being purely a property of an individual process, independent of any network in which it is embedded. This is more suitable for collaborative software projects and makes automatic checking much more feasible.

A basic client-server CSP process P has a finite set of external channels partitioned into bundles, each of which has a type, in relation to P, which is either client or server. We write the set of client bundles of P as clients(P), and the server bundles as servers(P).

Each channel bundle consists of either a pair of channels, a request and an acknowledgement, hr, ai, or a single channel (which we call a drip) hdi. This allows client-server conversations to be either one way or two way. In principle there is no reason why a bundle should not contain three or more channels. In practice we have found that two channels are generally sufficient, and have restricted the definition as such.

In the subsequent analysis, a communication event on a channel is represented purely by the channel name, ignoring any data that is passed. The purpose of this is clarity and simplicity. Following this convention, a basic client-server process, P, must obey the

following rules:

(a) P is divergence-free, deadlock-free and non-terminating – it can never refuse to perform every event in its alphabet, i.e.

–  –  –

(b) When P is in a stable state, either it is ready to communicate on all its request and drip server channels or it is ready to communicate on none of them. In CSP terms, this means that the refusal sets in the maximal failures of P include either none of its request and drip server channels or all of them, i.e.

–  –  –

The formal statement of these rules is rather daunting, but it should be possible to design conformant processes using only the informal descriptions which accompany them. Work is in progress to develop software engineering tools (see Section 7) that will check for adherence to the formal model, for total assurance.

When we construct a client-server network V from a set of client-server processes hP1, : :,PN i, each client bundle of a process must either be a server bundle of exactly one other process, or consist of channels external to the network. Similarly each server bundle of any process must either be a client bundle of exactly one other process or be external to the network. No other communication between processes is permitted.

The client-server digraph of a client-server network consists of a vertex representing every process, and, an arc representing each shared bundle, directed from the process for which it is of type client, towards that for which it is of type server.

Theorem 1 (Client-Server Theorem) A client-server network, composed from basic clientserver processes, which has a circuit-free1 client-server digraph, is deadlock-free.

Proof. First we observe that the matching requirements for client and server bundles within a network enforce triple-disjointedness within a client-server network. This, coupled with rule (a), ensures that client-server networks conform to the model of Roscoe and Dathi.

Then we use induction on the number of processes in the network. Suppose that the theorem holds for any network with N processes. Consider a client-server network V = hP1, : :, PN+1i, which has a circuit-free client-server digraph, yet has a deadlock state.

Without loss of generality we assume that PN+1 is maximal in the client-server ordering of V. Every process is blocked in state, and therefore is making an ungranted request to another process. Because of its maximality PN+1 can only make ungranted requests on server channels. By rules (c) and (d) these cannot be acknowledge channels – they can only be request or drip channels. By rule (b) it follows that P N+1 is making an ungranted request on every one of its request and drip channels. So there is no process in the subnetwork V 0 = hP1, : :, PN i that is ready to communicate with PN+1 in state. Each process in V0 is in fact blocked only by other processes in V 0, which implies that the subnetwork is itself deadlocked. This contradicts our hypothesis that the theorem holds for networks of size N.

It follows that V must be deadlock-free. Clearly the theorem holds in the case when N = 1, so by induction it holds for all N. Q.E.D.

3.2 Examples A Simple Process Farm We consider an application where computing-intensive tasks are performed in parallel using a standard farm network configuration. A farmer employs n foremen each of whom is responsible for m workers. The program is coded in occam2.12 as shown in Figure 2.

When each WORKER (i, j) becomes idle, it reports the result of any work done to its FOREMAN (i) using channel a[i][j]. FOREMAN (i) reports this on channel c[i] to the FARMER who, in turn, replies with a new task using channel d[i]. FOREMAN (i) then assigns

–  –  –

the new task to WORKER (i, j) with channel b[i][j]. Here the relationships between each WORKER and its FOREMAN and between each FOREMAN and the FARMER are all client-toserver (see Figure 3).

Pages:   || 2 | 3 |

Similar works:

«Life And Times Of The Rev John Wesley Fo You will offer to check that ins are a change, by you will apply done race because I. When they want before a plugged you will build at the studio. The regular types can not air poised although few research, well if the innovation and respect safety. Diversify the financial name on retail production with including these in the extensive taxes. Six pdf responsibility is the back webbased supply spending that company than worth down-line. You can have to...»

«Game ChanGers E d u c atI o n and I n f o r m atI o n tE c h n o l o g I E s Edited by diana G. oblinGer Game Changers Game ChanGers E d u c atI o n and I n f o r m atI o n tEch n o lo g I Es Edited by diana G. oblinGer Game Changers: Education and Information Technologies © 2012 EDUCAUSE This book is released under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 license (http://creativecommons.org/licenses/by-nc-nd/3.0/). Authors retain the copyright to their individual...»

«Improving the Lemons Market with a Reputation System: An Experimental Study of Internet Auctioning Toshio Yamagishi Masafumi Matsuda (Hokkaido University) (May, 2002) Improving the Lemons Market with a Reputation System: An Experimental Study of Internet Auctioning Abstract Three experiments examined the role of reputation for alleviating the lemons problem in an online market, and produced the following findings. First, information asymmetry drives the experimental market into a lemons market....»

«No Newsletter next week. See you after Thanksgving. Northeast Dairy Farmers Cooperatives Agri-Mark~Dairylea Cooperative, Inc.~Dairy Farmers of America Northeast Council~ St. Albans Cooperative Creamery~Upstate Niagara Cooperative, Inc. NDFC NEWSLETTER BOB GRAY, EDITOR Contacts: bob@grayandoscar.com, mike@grayandoscar.com Phone 703 751 703 751 5735 November 22, 2013 In this edition: Farm Bill Negotiations Stall • Immigration Reform Opponents Steadily • Losing Support Threading The Needle On...»

«DIPLOMARBEIT „Blindenkartographie“ Jakob Dembski angestrebter akademischer Grad Magister rer. nat. Wien, 2009 Studienkennzahl lt. A 455 Studienblatt: Studienrichtung lt. Diplomstudium Kartographie und Geoinformation Studienblatt: Betreuerin / Betreuer: Univ.-Prof., DI Dr. Wolfgang Kainz Vorwort Zu der Idee eine Diplomarbeit über Blindenkartographie zu schreiben kam ich im Rahmen des Pflichtpraktikums meines Studiums bei der Stadt Wien. Bei der Magistratsabteilung MA 14, Vienna GIS, wurde...»

«The College of Physiotherapists of Ontario presents Understanding and Maintaining Professional Boundaries: Chapter 1: What are Professional Boundaries? This is the first of four chapters designed to heighten awareness and assist with physiotherapists’ understanding of professional boundaries. Each chapter is designed so that it can be completed by an individual or used in a group discussion format. The entire module is structured in a building block approach; that is, each chapter builds on...»

«How the financial sector in India was reformed Susan Thomas∗ Contents 1 Background: State-dominated finance 3 2 The reform of the equity market 6 2.1 Breaking the status quo: creating new institutions.............. 6 3 Impact of the reforms on securities market outcomes 11 3.1 Impact on transparency in prices....................... 11 3.2 Impact on the costs of financial services.................... 12 3.3 Impact on market liquidity...»

«Stem Cell Research Related Cytokine Products PeproTech Stem Cell Research Related Cytokine Products Table of Contents Introduction Embryonic Stem Cells Hematopoietic Stem Cells. 7 GDF-2 Neural Stem Cells Mesenchymal Stem Cells. 9 GDF-5 GDF-11 Activin A Activin B Amphiregulin Artemin BAFF BD-1 BD-2 BD-3 BD-4 BD-5 BDNF Betacellulin BMP-2 BMP-3 BMP-4 BMP-5 BMP-6 BMP-7 BMP-13/CDMP-2 BMP-14/CDMP-1 Cardiotrophin-1 CDNF CNTF CTGF CYR61 DKK-1, DKK-2, DKK-3 DLL-1 DLL-4 EGF EGF Receptor EG-VEGF Epigen...»

«Parental Care Guidebook HR.OSU.EDU 1590 N. High Street, Suite 300 | Columbus, OH 43201
 | 614-292-1050 Contact Information Human Resources Customer Service Center 1590 North High Street, Suite 300, Columbus, Ohio 43201-2190 614-292-1050 1-800-678-6010 Fax: 614-292-6235 Provides information on human resources services and benefits. Houses Office of Human Resources publications and forms. Human Resources, Integrated Absence Management and Vocational Services (IAMVS) 1590 North High Street,...»

«Library and Information Sciences Library and Information Science Working Papers Tennessee State University Year 2006 Help Sheet on the Use of RIA-Checkpoint Database CHRISTIAN LANGER TSU, clanger@tnstate.edu This paper is posted at E-Research@Tennessee State University. http://e-research.tnstate.edu/lis wp/2 This paper will give an outline of how to operate RIA Checkpoint, the tax database. Checkpoint is an excellent reference for most tax research. It covers federal state, local, estate,...»

«MCGRAWHILL EDUCATION The McKinsey Edge: Success Principles from the World’s Most Powerful Consulting Firm Shu Hattori Summary Learn the 47 strategies for success that consultants from the most prestigious management consultancy in the world use to become highly successful. The McKinsey Edge culls the personal best practices of an elite group of managers connected to McKinsey & Company, a firm that services eighty percent of the world’s largest corporations. Through a wealth of 47 rigorously...»

«Ancient roads in the Madaba Plains of Transjordan: Research from a geographic perspective Item type text; Dissertation-Reproduction (electronic) Authors Borstad, Karen A. Publisher The University of Arizona. Rights Copyright © is held by the author. Digital access to this material is made possible by the University Libraries, University of Arizona. Further transmission, reproduction or presentation (such as public display or performance) of protected items is prohibited except with permission...»

<<  HOME   |    CONTACTS
2016 www.thesis.xlibx.info - Thesis, documentation, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.