Table of Contents

concurrency: state models & java programs, 2nd edition
Concurrency: State Models & Java Programs, 2nd Edition
byJeff MageeandJeff Kramer
John Wiley & Sons 2006 (432 pages)

Presenting concepts, techniques and problems through a variety of forms, this book provides a systematic and practical approach to designing, analyzing and implementing concurrent programs.

Table of Contents
Concurrency—State Models & Java Programs, 2nd Edition
Chapter 1 - Introduction
Chapter 2 - Processes and Threads
Chapter 3 - Concurrent Execution
Chapter 4 - Shared Objects and Mutual Exclusion
Chapter 5 - Monitors and Condition Synchronization
Chapter 6 - Deadlock
Chapter 7 - Safety and Liveness Properties
Chapter 8 - Model-Based Design
Chapter 9 - Dynamic Systems
Chapter 10 - Message Passing
Chapter 11 - Concurrent Architectures
Chapter 12 - Timed Systems
Chapter 13 - Program Verification
Chapter 14 - Logical Properties
Appendix A - FSP Quick Reference
Appendix B - FSP Language Specification
Appendix C - FSP Semantics
Appendix D - UML Class Diagrams
List of Figures
List of Tables
List of Programs

This book provides a systematic and practical approach to designing, analyzing and implementing concurrent programs, using both state models and Java programs to introduce and illustrate key concepts and techniques. Topics covered include:

  • threads and interaction
  • interference, exclusion and synchronization
  • deadlock, safety and liveness properties
  • message passing
  • concurrent software architectures
  • dynamic and timed systems.

Established as a key learning resource for computer science graduate and undergraduate students, this second edition includes new coverage of Program Verification and Logical Properties.

Ideal for classroom use or self-study, this book provides readers with the means to understand the fundamentals and practice of concurrency.

Concurrency—State Models & Java Programs, 2nd Edition




Department of Computing, Imperial College London, UK

image from book

John Wiley & Sons, Ltd

© 2006 John Wiley & Sons Ltd,

The Atrium, Southern Gate, Chichester, West Sussex PO19 8SQ, England
Telephone (+44) 1243 779777

Email (for orders and customer service enquiries):

Visit our Home Page on

All Rights Reserved. No part of this publication may be reproduced, stored in a retrieval system or transmitted in any form or by any means, electronic, mechanical, photocopying, recording, scanning or otherwise, except under the terms of the Copyright, Designs and Patents Act 1988 or under the terms of a licence issued by the Copyright Licensing Agency Ltd, 90 Tottenham Court Road, London W1T 4LP, UK, without the permission in writing of the Publisher. Requests to the Publisher should be addressed to the Permissions Department, John Wiley & Sons Ltd, The Atrium, Southern Gate, Chichester, West Sussex PO19 8SQ, England, or emailed to, or faxed to (+44) 1243 770620.

Designations used by companies to distinguish their products are often claimed as trademarks. All brand names and product names used in this book are trade names, service marks, trademarks or registered trademarks of their respective owners. The Publisher is not associated with any product or vendor mentioned in this book.

This publication is designed to provide accurate and authoritative information in regard to the subject matter covered. It is sold on the understanding that the Publisher is not engaged in rendering professional services. If professional advice or other expert assistance is required, the services of a competent professional should be sought.

Other Wiley Editorial Offices

John Wiley & Sons Inc., 111 River Street, Hoboken, NJ 07030, USA

Jossey-Bass, 989 Market Street, San Francisco, CA 94103-1741, USA

Wiley-VCH Verlag GmbH, Boschstr. 12, D-69469 Weinheim, Germany

John Wiley & Sons Australia Ltd, 42 McDougall Street, Milton, Queensland 4064, Australia

John Wiley & Sons (Asia) Pte Ltd, 2 Clementi Loop #02-01, Jin Xing Distripark, Singapore 129809

John Wiley & Sons Canada Ltd, 22 Worcester Road, Etobicoke, Ontario, Canada M9W 1L1

Wiley also publishes its books in a variety of electronic formats. Some content that appears in print may not be available in electronic books.

Library of Congress Cataloging-in-Publication Data:

Magee, Jeff, 1952–
Concurrency : state models & Java programs / Jeff Magee & Jeff Kramer.
p. cm.
Includes bibliographical references and index.
ISBN-13 978-0-470-09355-9 (cloth : alk. paper)

ISBN-10 0470093552 (cloth : alk. paper)

1. Parallel programming (Computer science) 2. Java (Computer program language) I. Kramer, Jeff. II. Title.

QA76.642.M34 2006
005.275 – dc22

British Library Cataloguing in Publication Data

A catalogue record for this book is available from the British Library

ISBN-13: 978-0-470-09356-6
ISBN-10: 0-470-09356-0


To Judith, Thomas and John

Jeff Magee

To Nitza, Lisa and Alon

Jeff Kramer


We wish to thank our colleagues in the Distributed Software Engineering research section for many helpful discussions over the years, and for their contributions to the work on software architecture. In particular, we gratefully acknowledge the contributions of Shing Chi (SC) Cheung and Dimitra Giannakopoulou to the work on behavior analysis. SC had the insight to select LTS as an appropriate modeling formalism, provided much of the ground-work and was a prime contributor to our investigation of safety properties. Dimitra has contributed crucial work in the theory and analysis of safety, liveness and progress properties, and the semantics of FSP.

Our thanks are due to Steve Crane, Nat Pryce, Wolfgang Emmerich and the anonymous reviewers for their useful comments and suggestion, on early drafts of the book. Their encouragement, and the enthusiasm of our students, is greatly appreciated. We would like to thank Storm Thorgerson, the cover designer, who worked beyond the call of duty and even friendship to produce a cover worthy of a trainspotter extraordinaire.

We would like to thank our families for their tolerance during the writing of this book. Our children – Lisa, Alon, Thomas and John – were kind enough to feign enthusiam for the examples and demonstration applets. Let us hope that the delusion of future fortune, with which we placated our wives Nitza and Judith, is not revealed as such too soon.

We take this opportunity to thank those many readers who have offered us their encouragement and suggestions. In particular, we are indebted to David Holmes who provided the motivation for Chapter 13 to address the problem of verifying the Java implementations. We also thank Alexander Höher for his comments on the bounded allocator of Chapter 9, and Paul Stroop for his many useful comments and suggestions. Finally we would like to express our thanks to the more recent members of the Distributed Software Engineering research group for their comments and contributions. In particular, we gratefully acknowledge the further contribution of Dimitra Giannakopoulou on fluents, and of Sebastian Uchitel to the work on model synthesis.

Jeff Magee & Jeff Kramer
January 2006