An introduction to assertional reasoning for concurrent systems

ABSTRACT

This is a tutorial introduction to assertional reasoning based on temporal logic. The objective is to provide a working familiarity with the technique. We use a simple system model and a simple proof system, and we keep to a minimum the treatment of issues such as soundness, completeness, compositionality, and abstraction. We model a concurrent system by a state transition system and fairness requirements. We reason about such systems using Hoare logic and a subset of linear-time temporal logic, specifically, invariant assertions and leads-to assertions. We apply the method to several examples.

REFERENCES

• 1: Martín Abadi , Leslie Lamport, Composing specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.73-132, Jan. 1993 [doi>10.1145/151646.151649]
• 2: Martín Abadi , Leslie Lamport, The existence of refinement mappings, Theoretical Computer Science, v.82 n.2, p.253-284, May 31, 1991 [doi>10.1016/0304-3975(91)90224-P ]
• 3: Cengiz Alaettinoglu , A. Udaya Shankar, Stepwise Assertional Design of Distance-Vector Routing Algorithms, Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification XII, p.399-413, June 22-25, 1992
• 4: ALPERN, B., AND SCHNEIDER, F 1985. Defining liveness Inf. Process. Lett. 21, 4 (Oct.), 181 185
• 5: G. R. Andrews, A method for solving synchronization problems, Science of Computer Programming, v.13 n.1, p.1-21, December 1989 [doi>10.1016/0167-6423(89)90013-0 ]
• 6: Krzysztof R. Apt, Ten Years of Hoare's Logic: A Survey—Part I, ACM Transactions on Programming Languages and Systems (TOPLAS), v.3 n.4, p.431-483, Oct. 1981 [doi>10.1145/357146.357150]
• 7: APT, K. R., FRANCEZ, N., AND }~4TZ, S. 1988. Apprmsing fairness in languages for distributed programming. Dzstrzb. Cornput. 2, 4, 226 241.
• 8: R. J. R. Back , F. Kurki-Suonio, Distributed cooperation with action systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.4, p.513-554, Oct. 1988 [doi>10.1145/48022.48023]
• 9: R. J. R. Back , R. Kurki-Suonio, Decentralization of process nets with centralized control, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.131-142, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806716]
• 10: R. J. R. Back , K. Sere, Stepwise refinement of parallel algorithms, Science of Computer Programming, v.13 n.2-3, p.133-180, May 1990 [doi>10.1016/0167-6423(90)90069-P ]
• 11: K. Mani Chandy, Parallel program design: a foundation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 12: Mani Chandy , Jayadev Misra, An example of stepwise refinement of distributed programs: quiescence detection, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.3, p.326-343, July 1986 [doi>10.1145/5956.5958]
• 13: DI,IKSTRA, E W 1977 A correctness proof for communicating processes A small exermse. EWD-607, Burroughs, Nuenen, The Netherlands
• 14: Dt.JKSTI~A, E.W. 1976 A Discipline of ProgrammlTlg Prentme-Hall, Englewood Cliffs, N.J.
• 15: E. W. Dijkstra, Solution of a problem in concurrent programming control, Communications of the ACM, v.8 n.9, p.569, Sept. 1965 [doi>10.1145/365559.365617]
• 16: DI,JK~TI~A, E. W., AND SCHOLTEN, C.S. 1980. Termination detection for diffusing computations. Inf. Process. Lett 11 (Aug.), 1-4.
• 17: DI,IKSTRA, E W., FEIJN, W. H. J., AND VAN GASTEREN, A. J. M. 1983. Derivation of a termination detection algorithm for distributed computations. Inf. Process. Lett. 16, 217 219.
• 18: Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978 [doi>10.1145/359642.359655]
• 19: DROST, N. J, AND SCHOONE, A.A. 1988. Asserhonal verification of a reset algorithm. R1jksuniverslteit Utrecht, RUU-CS-88-5.
• 20: DROST, N. J., AND VAN LEEUWEN, J. 1988. Assertional verification of a majority consensus algorithm tbr concurrency control in multiple copy databases. Rijksuniversiteit Utrecht, RUU-CS- 88-13.
• 21: FLoY/), R. W. 1967. Assigning' meanings to programs. In Proceedings o{ the Synzposzum on Applied Mothematzcs. Vol. 19. American Mathematical Society, 19 32,
• 22: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 23: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 24: HAmPFRN, B. T., AN1) OWICKL S. S. 1983. Modular verification of computer communication protocols. IEEE Trans. Commun. COM-31, 1 (Jan.), 56 68.
• 25: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 26: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 27: KNUTH, D.E. 1981. Vemfication of link-level protocols BIT21, 31 36.
• 28: Simon S. Lam , A. Udaya Shankar, Specifying modules to satisfy interfaces: a state transition system approach, Distributed Computing, v.6 n.1, p.39-63, July 1992 [doi>10.1007/BF02276640]
• 29: Simon S. Lam , A. Udaya Shankar, A Relational Notation for State Transition Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.755-775, July 1990 [doi>10.1109/32.56101 ]
• 30: LAMPOm', L. 1991. The temporal logic of actions. DEC SRC Rep..57, Pale Alto, Calif' Revised 1991
• 31: L^M,Om', L. 1990. A theorem on atomicity in distnbuted algorithms. Dzstnb. Comput. 4, 2, 59-68.
• 32: Leslie Lamport, A simple approach to specifying concurrent systems, Communications of the ACM, v.32 n.1, p.32-45, Jan. 1989 [doi>10.1145/63238.63240]
• 33: Leslie Lamport, A fast mutual exclusion algorithm, ACM Transactions on Computer Systems (TOCS), v.5 n.1, p.1-11, Feb. 1987 [doi>10.1145/7351.7352]
• 34: LAMPORT, L. 1983a. What good is temporal logic. in Proceedings of In/brmation Processing 83. IFIP, Arlington, Va.
• 35: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 36: LAMPORT, L. 1982. An assertional correctness proof of a distributed algorithm. Sez Comput. Program. 2, 3, 175-206.
• 37: LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3, 2 (Feb.), 125-143.
• 38: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 39: Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
• 40: Zohar Manna , Amir Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Science of Computer Programming, v.4 n.3, p.257-289, Dec. 1984 [doi>10.1016/0167-6423(84)90003-0 ]
• 41: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 42: MILNER, R. 1989. Comnzunzcotmn and Concurrency. Prentice-Hall, Englewood Cliffs, N.J
• 43: MURPHY, S. L., AND SHANKAR, A. U. 1991 Connection management for the transport layer: Service specification and protocol construction. IEEE Trans. Commun. 39 (Dec.), 1762-1775.
• 44: OWICKI, S., AND GRIES, D. 1976. An axiomatic proof technique for parallel programs I. Aeta In/brmatwa 6, 4, 319-340.
• 45: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 46: PETERSON, G.L. 1981. Myths about the mutual exclusion problem. Inf. Process. Lett. 12, 3 (June) 1133 1145
• 47: A. Pnueli, In transition from global to modular temporal reasoning about programs, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 48: Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
• 49: PNEUM, A. 1977 The temporal logic of programs. In Proceedings o{ the 18th ACM Symposn~m on the Foundatmna' of Computer Seienoe. ACM, New York, 46 57.
• 50: F B Schneider , G R Andrews, Concepts for concurrent programming, Current trends in concurrency. Overviews and tutorials, Springer-Verlag New York, Inc., New York, NY, 1986
• 51: SCHOONE, A A. 1987. Verification of connectionmanagement protocols. Rijksuniverslteit Utrecht, RUU-CS-87-14
• 52: A. Udaya Shankar, Verified data transfer protocols with variable flow control, ACM Transactions on Computer Systems (TOCS), v.7 n.3, p.281-316, Aug. 1989 [doi>10.1145/65000.65003]
• 53: A. Udaya Shankar , Simon S. Lam, A stepwise refinement heuristic for protocol construction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.3, p.417-461, July 1992 [doi>10.1145/129393.129394]
• 54: SHAN}OkR, A. U., AND LAM, S. S. 1987 Tramdependent distributed systems Proving safety, liveness and real-time propertms D~strlb. Comput. 2, 2, 61 79.
• 55: A. Udaya Shankar , Simon S. Lam, An HDLC protocol specification and its verification using image protocols, ACM Transactions on Computer Systems (TOCS), v.1 n.4, p.331-368, Nov. 1983 [doi>10.1145/357377.357384]
• 56: A. P. Sistla, Distributed algorithms for ensuring fair interprocess communicatons, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.266-277, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806753]
• 57: TEL, G 1987 Assertional verification of a timer-based protocol. R1jksunlversltmt Utrecht, RUU-CS-87-15.
• 58: G. Tel , R. B. Tan , J. van Leeuwen, The derivation of graph marking algorithms from distributed termination detection protocols, Science of Computer Programming, v.10 n.2, p.107-137, April 1988 [doi>10.1016/0167-6423(88)90024-X ]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Assertions; Invariants; Pre- and post-conditions; Logics of programs

General Terms:
Verification

Keywords:
Hoare logic, assertional reasoning, generation of preconditions, invariants, leads-to, progress properties, safety properties, state transition systems, weakest preconditions