|Table of Contents|
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:
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
John Wiley & Sons,
© 2006 John Wiley & Sons Ltd,
The Atrium, Southern Gate, Chichester, West Sussex PO19 8SQ,
Telephone (+44) 1243 779777
Email (for orders and customer service enquiries): firstname.lastname@example.org
Visit our Home Page on www.wiley.com
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 email@example.com, 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.
Includes bibliographical references and index.
ISBN-13 978-0-470-09355-9 (cloth : alk. paper)
1. Parallel programming (Computer science) 2. Java (Computer program language) I. Kramer, Jeff. II. Title.
005.2′75 – dc22
British Library Cataloguing in Publication Data
A catalogue record for this book is available from the British Library
To Judith, Thomas and John
To Nitza, Lisa and Alon
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