Specifying Systems First Printing Version of 18 June 2002 Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers Leslie Lamport Microsoft Research Boston San Francisco New York Toronto Montreal • • • • London Munich Paris Madrid • • • Capetown Sydney Tokyo Singapore Mexico City • • • • Manyofthedesignationsusedbymanufacturersandsellerstodistinguishtheir productsareclaimedastrademarks. Wherethosedesignationsappearinthisbook, andAddison-Wesleywasawareofatrademarkclaim,thedesignationshavebeen printedwithinitialcapitallettersorinallcapitals. Theauthorandpublisherhavetakencareinthepreparationofthisbook,butmakeno expressedorimpliedwarrantyofanykindandassumenoresponsibilityforerrorsor omissions. Noliabilityisassumedforincidentalorconsequentialdamagesinconnection withorarisingoutoftheuseoftheinformationorprogramscontainedherein. Thepublisheroffersdiscountsonthisbookwhenorderedinquantityforspecialsales. Formoreinformation,pleasecontact: U.S.CorporateandGovernmentSales (800)382-3419 [email protected] ForsalesoutsideoftheU.S.,pleasecontact: InternationalSales (317)581-3793 [email protected] VisitAddison-WesleyontheWeb: www.awprofessional.com Library of Congress Cataloging-in-Publication Data Lamport,Leslie Specifyingsystems: the TLA+ languageand tools for hardwareand software engineers/LeslieLamport. p. cm. Includesbibliographicalreferencesandindex. ISBN0-321-14306-X(alk. paper) 1. Systemdesign. 2. Computersystems–Specifications. 3. Logic,symbolic andmathematical.I.Title. QA76.9.S88L352003 2002074369 004.2′1--dc21 Copyright(cid:13)c 2003byPearsonEducation,Inc Allrightsreserved. Nopartofthispublicationmaybereproduced,storedinare- trievalsystem,ortransmitted,inanyform,orbyanymeans,electronic,mechanical, photocopying,recording,orotherwise,withoutthepriorconsentofthepublisher. PrintedintheUnitedStatesofAmerica. PublishedsimultaneouslyinCanada. Forinformationonobtainingpermissionforuseofmaterialfromthiswork,please submitawrittenrequestto: PearsonEducation,Inc. RightsandContractsDepartment 75ArlingtonStreet,Suite300 Boston,MA02116 Fax: (617)848-7047 ISBN0-321-14306-X Textprintedonrecycledpaper 12345678910-MA-0605040302 Firstprinting, July 2002 To Ellen This whole book is but a draught—nay, but the draught of a draught. Herman Melville Contents List of Figures and Tables xv Acknowledgments xvii Introduction 1 Part I Getting Started 5 1 A Little Simple Math 9 1.1 Propositional Logic . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.2 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 1.3 Predicate Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 1.4 Formulasand Language . . . . . . . . . . . . . . . . . . . . . . . 14 2 Specifying a Simple Clock 15 2.1 Behaviors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.2 An Hour Clock . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3 A Closer Look at the Specification . . . . . . . . . . . . . . . . . 18 2.4 The Specification in TLA+. . . . . . . . . . . . . . . . . . . . . . 19 2.5 An Alternative Specification . . . . . . . . . . . . . . . . . . . . . 21 3 An Asynchronous Interface 23 3.1 The First Specification . . . . . . . . . . . . . . . . . . . . . . . . 24 3.2 Another Specification . . . . . . . . . . . . . . . . . . . . . . . . 28 3.3 Types: A Reminder . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.4 Definitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.5 Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 A FIFO 35 4.1 The Inner Specification . . . . . . . . . . . . . . . . . . . . . . . 35 4.2 Instantiation Examined . . . . . . . . . . . . . . . . . . . . . . . 37 ix x CONTENTS 4.2.1 Instantiation Is Substitution. . . . . . . . . . . . . . . . . 37 4.2.2 Parametrized Instantiation . . . . . . . . . . . . . . . . . 39 4.2.3 ImplicitSubstitutions . . . . . . . . . . . . . . . . . . . . 40 4.2.4 Instantiation Without Renaming . . . . . . . . . . . . . . 40 4.3 Hiding the Queue . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 4.4 A Bounded FIFO . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.5 What We’re Specifying . . . . . . . . . . . . . . . . . . . . . . . . 43 5 A Caching Memory 45 5.1 The MemoryInterface . . . . . . . . . . . . . . . . . . . . . . . . 45 5.2 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.3 A Linearizable Memory . . . . . . . . . . . . . . . . . . . . . . . 51 5.4 Tuples as Functions . . . . . . . . . . . . . . . . . . . . . . . . . 53 5.5 Recursive Function Definitions . . . . . . . . . . . . . . . . . . . 54 5.6 A Write-Through Cache . . . . . . . . . . . . . . . . . . . . . . . 54 5.7 Invariance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 5.8 Proving Implementation . . . . . . . . . . . . . . . . . . . . . . . 62 6 Some More Math 65 6.1 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 6.2 Silly Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 6.3 Recursion Revisited . . . . . . . . . . . . . . . . . . . . . . . . . 67 6.4 Functions versus Operators . . . . . . . . . . . . . . . . . . . . . 69 6.5 Using Functions. . . . . . . . . . . . . . . . . . . . . . . . . . . . 72 6.6 Choose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 7 Writing a Specification: Some Advice 75 7.1 Why Specify . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 7.2 What to Specify . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 7.3 The Grain of Atomicity . . . . . . . . . . . . . . . . . . . . . . . 76 7.4 The Data Structures . . . . . . . . . . . . . . . . . . . . . . . . . 78 7.5 Writing the Specification . . . . . . . . . . . . . . . . . . . . . . . 79 7.6 Some Further Hints. . . . . . . . . . . . . . . . . . . . . . . . . . 80 7.7 When and How to Specify . . . . . . . . . . . . . . . . . . . . . . 83 Part II More Advanced Topics 85 8 Liveness and Fairness 87 8.1 Temporal Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . 88 8.2 Temporal Tautologies . . . . . . . . . . . . . . . . . . . . . . . . 92 8.3 Temporal Proof Rules . . . . . . . . . . . . . . . . . . . . . . . . 95 8.4 Weak Fairness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 8.5 The MemorySpecification . . . . . . . . . . . . . . . . . . . . . . 100