[Concurrency - State Models & Java Programs] Preface

Preface

This book arose from concurrent programming courses taught by the authors at Imperial College London and from their experience with using concurrency in industrial applications. It was motivated by dissatisfaction with the lack of practical and accessible techniques that aid reasoning about designs for concurrent software.

Most courses and textbooks in this area are targeted at either the theory and formal methods aspects of concurrency or the practical aspects of concurrent programming and concurrency in operating systems. Due to the lack of a widely available concurrent programming language, textbooks had to resort to special purpose notations that could not easily be related by the reader to normal sequential programming practice. Two recent technical developments have made it possible to offer a practical and accessible approach to learning about concurrency and concurrent programming. First, model-checking tools have made the use of design models for concurrent behavior practical, informative and rewarding. Second, the availability and widespread use of Java has solved the problem of finding an accessible general purpose programming language with in-built concurrency constructs. As a result, this book offers a soundly-based systematic approach to the development of concurrent software which is supported by software tools, is interesting and fun to use, and can be used to develop practical concurrent programs.

What Can Readers Expect from this Book?

The book provides a comprehensive description and explanation of the important concepts and techniques in concurrent programming, the problems that arise and the means for ensuring that desirable properties are achieved and undesirable ones avoided. Readers will learn about concepts such as threads and interaction, gain an appreciation of how these lead to problems such as interference and deadlock, and learn how to use techniques such as exclusion and synchronization to good effect.

To ensure a thorough understanding, concurrency concepts, techniques and problems are presented in many forms: through informal descriptions and illustrative examples, abstractly in models and concretely in Java. The modeling techniques will enable readers to reason about the properties of their proposed designs and programs. As in other engineering disciplines, modeling is promoted as a means to gaining greater confidence in the proposed designs. Using Java, readers can turn their designs into programs.

Together with a knowledge and understanding of the principles of concurrency, readers can expect to aquire experience in its application. The book uses examples to illustrate concepts and techniques, and exercises for learning by doing. Use of the associated analysis tool provides practical experience of concurrency modeling, model animation, model property checking and model correction. Similarly, use of Java provides practical experience of programming concurrency.

Thus, the book provides:

• a systematic treatment of the concepts and issues in concurrency;
• a rigorous technique to specify and model concurrent behavior, with analysis tools for animation and verification;
• a wide range of Java examples to illustrate the concepts and issues in concurrent programming.

We hope that this will leave readers with the ability to use concurrency with confidence and expertise, recognizing when problems might arise and knowing how to avoid or solve them. Concurrency is a fascinating and challenging area of software design. The combination of learning and doing should make acquiring design skills in this area an interesting and enjoyable process. We hope that readers will find that concurrency can be both challenging and fun!

Intended Readership

The book is intended for students in Computer Science and for professional software engineers and programmers. We believe that it has much to offer for anyone interested in the concepts of concurrency, interaction and synchronization.

Readers are expected to have some background in sequential programming and an acquaintance with object-oriented concepts. Some knowledge of operating systems concepts is an advantage, but is not a prerequisite.

The material has been used by a variety of students: undergraduate students in the second year of three and four year computing, software engineering and combined computing/electrical engineering degree courses; and graduate students taking conversion courses in computing. In all cases, the material represented the students’ first introduction to concurrent programming.

Chapters 1 to 8 are designed to provide a comprehensive and cohesive course on concurrency. They cover the main concepts of concurrency, including modeling, programming and the process of model-based design. Since each chapter builds on the preceding one, we recommend that these chapters be read sequentially from start to finish.

Chapters 9 to 14 provide more advanced material on dynamic systems, message passing, concurrent software architectures, timed systems, program verification and logical properties. Readers may pick and choose from these according to their interests.

Additional Resources

Accompanying this book are the following:

• Java examples and demonstration programs
• state models for the examples
• the Labeled Transition System Analyzer (LTSA) for concurrency modeling, model animation, and model property checking
• overhead slides for course presentation

These are provided at the following URL: http://www.wileyeurope.com/college/magee.

Second Edition

This second edition of the book provides the following main additions:

• Dynamic Systems.
  A new model and implementation for bounded dynamic resource allocation is presented and discussed in Chapter 9.
• A new chapter on Program Verification.
  The general approach used in the book is model-based design, where models are developed and analyzed before implementation. This chapter describes how concurrent implementations in Java can be modeled and verified. This is illustrated using examples from previous chapters.
• Sequential process composition.
  Processes are generally composed using parallel composition to model interaction and concurrency. Composition is extended to include sequential composition as well, thereby extending the ways in which models can be specified and analyzed.
• A new chapter on Logical Properties.
  The formalism used in the book is based on the identification and specification of events and actions rather than states. This chapter introduces the use of fluents and abstract states as a means of specifying logical, state-based properties in an event-based formalism. This extension supports property specification using Linear Temporal Logic (LTL). In addition to the provision of counterexamples in the case of property violations, witnesses can be provided to give examples of acceptable executions. This is illustrated using examples, both new and from previous chapters.
• Extensions to LTSA.
  Tool support for model analysis using LTSA has been extended to provide a number of additional features. These include a revised user interface, on-the-fly safety and progress analysis allowing complete analysis of much larger state spaces, approximate safety analysis using Holtzmann’s SuperTrace algorithm for larger state spaces, support for sequential composition, support for graphic animation, no limit on potential statespace (previously 2**63), and Partial Order Reduction during composition and analysis.
• Java platform.
  The demonstration programs and examples have been updated to use the new Java version which includes generic classes.