Skip to main content
SpringerLink
Log in

Introduction

  • Chapter
  • First Online:
Distributed Programming

  • 1572 Accesses

Abstract

This chapter gives a detailed overview of the SESF method. It describes programs, service programs, how to establish that a program implements a service program, and the benefits of using service programs when writing other programs. A program consists of main code and functions. When it is instantiated, an instance of the program, referred to as a system, is created and a thread starts executing the system’s main code. The program can create threads to execute local functions, call functions of other systems, and instantiate programs. Thus a program can create a collection of concurrently-executing and interacting systems. Service programs are programs that define the intended external behavior of regular programs. They have a special structure that make them easy to understand, and hence easy to use when writing other programs. If a program A implements a service program B, then replacing an instantiation of B in any program C by an instantiation of A preserves all the correctness properties of program C. Because of its structure, a service program is easily transformed to an “inverse” program that provides the most general environment that any implementation of the service would face. To establish that a program A implements a service program B, one simply shows that the program of A and B-inverse satisfies certain conditions. Assertional reasoning is used to account for every possible evolution.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. M. Abadi, L. Lamport, The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253–284 (1991). doi:10.1016/0304-3975(91)90224-P. http://dx.doi.org/10.1016/0304-3975(91)90224-P

    Google Scholar 

  2. M. Abadi, L. Lamport, Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993). doi:10.1145/151646.151649. http://doi.acm.org/10.1145/151646.151649. Also in Stepwise Refinement of Distributed Systems, LNCS 430, Springer, 1990

    Google Scholar 

  3. C. Alaettinoglu, A.U. Shankar, Stepwise assertional design of distance-vector routing algorithms. in Protocol Specification, Testing and Verification XII, ed. by R.J. Linn Jr., M.M. Uyar. Proceedings of the IFIP TC6/WG6.1 Twelth International Symposium on Protocol Specification, Testing and Verification, Lake Buena Vista, Florida, USA, 22–25 June 1992. IFIP Transactions, vol. C-8 (North-Holland, New York, 1992), pp. 399–413

    Google Scholar 

  4. G.R. Andrews, A method for solving synchronization problems. Sci. Comput. Program. 13(4), 1–21 (1989)

    Article  MATH  Google Scholar 

  5. G.R. Andrews, F.B. Schneider, Concepts and notations for concurrent programming. ACM Comput. Surv. 15(1), 3–43 (1983). doi:10.1145/356901.356903. http://doi.acm.org/10.1145/356901.356903

    Google Scholar 

  6. K.R. Apt, Ten years of hoare’s logic: a survey-part i. ACM TOPLAS 3, 431–483 (1981)

    Article  MATH  Google Scholar 

  7. E.A. Ashcroft, Proving assertions about parallel programs. J. Comput. Syst. Sci. 10(1), 110–135 (1975). doi:10.1016/S0022-0000(75)80018-3. http://dx.doi.org/10.1016/S0022-0000(75)80018-3

    Google Scholar 

  8. R.J. Back, Invariant based programming: basic approach and teaching experiences. Form. Aspects Comput. 21, 227–244 (2009). doi:10.1007/s00165-008-0070-y

    Article  MATH  Google Scholar 

  9. R.J.R. Back, R. Kurki-Suonio, Decentralization of process nets with centralized control, in Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing, PODC ’83 (ACM, New York, 1983), pp. 131–142. doi:10.1145/800221.806716. http://doi.acm.org/10.1145/800221.806716

  10. R.J.R. Back, F. Kurki-Suonio, Distributed cooperation with action systems. ACM Trans. Program. Lang. Syst. 10(4), 513–554 (1988). doi:10.1145/48022.48023. http://doi.acm.org/10.1145/48022.48023

    Google Scholar 

  11. R.J.R. Back, K. Sere, Stepwise refinement of parallel algorithms. Sci. Comput. Program. 13(2–3), 133–180 (1990). doi10.1016/0167-6423(90)90069-P. http://dx.doi.org/10.1016/0167-6423(90)90069-P

    Google Scholar 

  12. R.J. Back, K. Sere, Stepwise refinement of action systems. Software 12, 17–30 (1991)

    Google Scholar 

  13. R.J. Back, J.V. Wright, Contracts, games, and refinement. Inf. Comput. Control 156, 25–45 (2000). doi:10.1006/inco.1999.2820

    Article  MATH  Google Scholar 

  14. R.J. Back, J.V. Wright, Compositional action system refinement. Form. Aspects Comput. 15, 103–117 (2003). doi:10.1007/s00165-003-0005-6

    Article  MATH  Google Scholar 

  15. M. Ben-Ari, The Art of Multiprocessor Programming, 2nd edn. (Addison-Wesley, San Francisco, 2006)

    Google Scholar 

  16. J.A. Carruth, J. Misra, Proof of a real-time mutual-exclusion algorithm. Parallel Process. Lett. 6(2), 251–257 (1996)

    Article  MathSciNet  Google Scholar 

  17. K.M. Chandy, J. Misra, The drinking philosophers problem. ACM Trans. Program. Lang. Syst. 6(4), 632–646 (1984). doi:10.1145/1780.1804. http://doi.acm.org/10.1145/1780.1804

    Google Scholar 

  18. K.M. Chandy, J. Misra, An example of stepwise refinement of distributed programs: quiescence detection. ACM Trans. Program. Lang. Syst. 8(3), 326–343 (1986). doi:10.1145/5956.5958. http://doi.acm.org/10.1145/5956.5958

    Google Scholar 

  19. K.M. Chandy, J. Misra, Parallel Program Design: A Foundation (Addison-Wesley, Boston, 1989)

    Google Scholar 

  20. K.M. Chandy, J. Misra, Proof of distributed algorithms: an exercise, in: Developments in Concurrency and Communication, ed. by C.A.R. Hoare (Addison-Wesley Longman, Boston, 1990), pp. 305–332. http://dl.acm.org/citation.cfm?id=107155.107171

  21. E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986). doi:10.1145/5397.5399. http://doi.acm.org/10.1145/5397.5399

    Google Scholar 

  22. E.M. Clarke Jr., O. Grumberg, D.A. Peled, Model Checking (MIT, Cambridge MA, 1999)

    Google Scholar 

  23. E. Cohen, Modular Progress Proofs of Asynchronous Programs, Ph.D. thesis, University of Texas, Austin, 1993. UMI Order No. GAX93-23370

    Google Scholar 

  24. E. Cohen, Validating the microsoft hypervisor, in: FM 2006: Formal Methods, ed. by J. Misra, T. Nipkow, E. Sekerinski. 14th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 4085 (Springer, New York, 2006), pp. 81–81

    Google Scholar 

  25. E. Cohen, L. Lamport, Reduction in tla, in Proceedings of the 9th International Conference on Concurrency Theory, CONCUR ’98 (Springer, London, 1998), pp. 317–331. http://dl.acm.org/citation.cfm?id=646733.701301

    Google Scholar 

  26. E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, Vcc: a practical system for verifying Concurrent c, in Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’09 (Springer, Berlin/Heidelberg 2009), pp. 23–42. doi:10.1007/978-3-642-03359-9_2. http://dx.doi.org/10.1007/978-3-642-03359-9_2

    Google Scholar 

  27. E. Cohen, M. Moskal, W. Schulte, S. Tobies, Local verification of global invariants in concurrent programs, in Proceedings of the 22nd International Conference on Computer Aided Verification, CAV’10 (Springer, Berlin/Heidelberg, 2010), pp. 480–494. doi:10.1007/978-3-642-14295-6_42. http://dx.doi.org/10.1007/978-3-642-14295-6_42

    Google Scholar 

  28. D. Comer, Internetworking with TCP/IP, 4th edn. Vol 1: Principles, Protocols, and Architectures (Prentice-Hall, Upper Saddle River, 2000)

    Google Scholar 

  29. D.E. Comer, D.L. Stevens, Internetworking with TCP/IP, 1st edn. Vol. 3: Client-Server Programming and Applications, Linux/Posix Sockets Version (Prentice Hall, Upper Saddle River, 2000)

    Google Scholar 

  30. E.W. Dijkstra, Cooperating sequential processes. Technical report, Burroughs, Nuenen, 1965. EWD-123

    Google Scholar 

  31. E.W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975). doi:10.1145/360933.360975. http://doi.acm.org/10.1145/360933.360975

    Google Scholar 

  32. E.W. Dijkstra, A correctness proof for communicating processes – a small exercise. Technical report, Burroughs, Nuenen, 1977. EWD-607

    Google Scholar 

  33. E.W. Dijkstra, Two starvation-free solutions of a general exclusion problem. Technical report, Nuenen, 1978. EWD-625

    Google Scholar 

  34. E.W. Dijkstra, Finding the correctness proof of a concurrent program, in Program Construction, International Summer Schoo (Springer, London, 1979), pp. 24–34. http://dl.acm.org/citation.cfm?id=647639.733356

  35. E.W. Dijkstra, The distributed snapshot of k.m. chandy and l. lamport, in Proceedings of the NATO Advanced Study Institute on Control flow and Data Flow: Concepts Of Distributed Programming (Springer, New York, 1986), pp. 513–517. http://dl.acm.org/citation.cfm?id=22086.22099. Also EWD-864a

    Google Scholar 

  36. E.W. Dijkstra, A Discipline of Programming, 1st edn. (Prentice Hall, Upper Saddle River, 1997)

    Google Scholar 

  37. E.W. Dijkstra, Cooperating sequential processes, in The Origin of Concurrent Programming, ed. P.B. Hansen (Springer, New York, 2002), pp. 65–138. http://dl.acm.org/citation.cfm?id=762971.762974

    Google Scholar 

  38. E.W. Dijkstra, C.S. Scholten, Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980)

    Article  MathSciNet  MATH  Google Scholar 

  39. E.W. Dijkstra, L. Lamport, A.J. Martin, C.S. Scholten, E.F.M. Steffens, On-the-fly garbage collection: an exercise in cooperation. Commun. ACM 21(11), 966–975 (1978). doi:10.1145/359642.359655. http://doi.acm.org/10.1145/359642.359655

    Google Scholar 

  40. E.W. Dijkstra, W.H.J. Feijen, A.J.M. van Gasteren, Derivation of a termination detection algorithm for distributed computations. Inf. Process. Lett. 16(5), 217–219 (1983). Also EWD 840

    Google Scholar 

  41. M.J. Donahoo, K. Calvert, TCP/IP Sockets in C, Practical Guide for Programmers, 2nd edn. (Morgan Kaufmann, Burlington, 2009)

    Google Scholar 

  42. N.J. Drost, J.V. Leeuwen, Assertional Verification of a Majority Consensus Algorithm for Concurrency Control in Multiple Copy Databases (Springer, New York, 1988). doi:10.1007/3-540-50403-6_48

    Google Scholar 

  43. M.R. Drost, A.A. Schoone, Assertional verification of a reset algorithm. Technical report, DSpace at Utrecht University, Netherlands, 1988 [http://dspace.library.uu.nl:8080/dspace-oai/request]. http://igitur-archive.library.uu.nl/math/2006-1214-201542/UUindex.html

  44. T. Elsharnouby, A.U. Shankar, SeSFJava harness: service and assertion checking for protocol implementations. IEEE J. Sel. Areas Commun. 22(10), 2035–2047 (2004). doi:10.1109/JSAC.2004.836012

    Article  Google Scholar 

  45. T. Elsharnouby, A.U. Shankar, Using SeSFJava in teaching introductory network courses, in Proceedings of the 36th SIGCSE Technical Symposium on Computer Science Education, SIGCSE ’05 (ACM, New York, 2005), pp. 67–71. doi:10.1145/1047344.1047381. http://doi.acm.org/10.1145/1047344.1047381

  46. E.A. Emerson, V. Kahlon, Rapid parameterized model checking of snoopy cache coherence protocols, in TACAS 2003, vol. 2619, ed. by H. Garavel, J. Hatcliff. Lecture Notes in Computer Science (Springer, New York, 2003), pp. 144–159

    Google Scholar 

  47. W.H.J. Feijen, A.J.M. van Gasteren, On a Method of Multiprogramming (Springer, New York, 1999)

    MATH  Google Scholar 

  48. R.W. Floyd, Assigning meanings to programs, in Proceedings of a Symposium on Applied Mathematics, vol. 19, ed. by J.T. Schwartz. Mathematical Aspects of Computer Science (American Mathematical Society, Providence, 1967), pp. 19–31. http://www.eecs.berkeley.edu/\~necula/Papers/FloydMeaning.pdf

  49. D. Ginat, Adaptive Ordering of Contending Processes in Distributed Systems. Ph.D. thesis, University of Maryland, Computer Science Department, College Park, 1989. CSTR-2335

    Google Scholar 

  50. D. Ginat, A.U. Shankar, An assertional proof of correctness and serializability of a distributed mutual exclusion algorithm based on path reversal. Technical report, University of Maryland, Computer Science Department, 1988. CSTR-2104

    Google Scholar 

  51. D. Ginat, A.U. Shankar, A.K. Agrawala, An efficient solution to the drinking philosophers problem and its extensions, in Distributed Algorithms, vol. 392, ed. by J.C. Bermond, M. Raynal. Lecture Notes in Computer Science (Springer, Berlin/Heidelberg, 1989), pp. 83–93. http://dx.doi.org/10.1007/3-540-51687-5_34. doi:10.1007/3-540-51687-5_34

    Google Scholar 

  52. D. Gries, An exercise in proving parallel programs correct. Commun. ACM 20(12), 921–930 (1977). doi:10.1145/359897.359903. http://doi.acm.org/10.1145/359897.359903

    Google Scholar 

  53. R. Guerraoui, T.A. Henzinger, B. Jobstmann, V. Singh, Model checking transactional memories, in Proceedings of the 2008 ACM SIGPLAN Conference on programming Language Design and Implementation, PLDI ’08 (ACM, New York, 2008), pp. 372–382. doi:10.1145/1375581.1375626. http://doi.acm.org/10.1145/1375581.1375626

  54. B. Hailpern, S. Owicki, Modular verification of computer communication protocols. IEEE Trans. Commun. 31(1), 56–68 (1983). doi:10.1109/TCOM.1983.1095720

    Article  Google Scholar 

  55. M. Herlihy, N. Shavit, The Art of Multiprocessor Programming (Morgan Kaufmann, San Francisco, 2008)

    Google Scholar 

  56. C.A.R. Hoare, An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). doi:10.1145/363235.363259. http://doi.acm.org/10.1145/363235.363259

    Google Scholar 

  57. E. Knapp, An exercise in the formal derivation of parallel programs: maximum flows in graphs. ACM Trans. Program. Lang. Syst. 12(2), 203–223 (1990). doi:10.1145/78942.78945. http://doi.acm.org/10.1145/78942.78945

    Google Scholar 

  58. D.E. Knuth: Verification of link-level protocols. BIT 21(1), 31–36 (1981)

    MathSciNet  MATH  Google Scholar 

  59. R.A. Krzysztof, E.R. Olderog, Verification of Sequential and Concurrent Programs (Springer, New York, 1991)

    Google Scholar 

  60. P. Ladkin, L. Lamport, B. Olivier, D. Roegel, Lazy caching in tla. Distrib. Comput. 12(2–3), 151–174 (1999). doi:10.1007/s004460050063. http://dx.doi.org/10.1007/s004460050063

    Google Scholar 

  61. S.S. Lam, A.U. Shankar, A relational notation for state transition systems. IEEE Trans. Softw. Eng. 16(7), 755–775 (1990). doi:10.1109/32.56101. http://dx.doi.org/10.1109/32.56101

    Google Scholar 

  62. S.S. Lam, A.U. Shankar, Specifying modules to satisfy interfaces: a state transition system approach. Distrib. Comput. 6(1), 39–63 (1992). doi:10.1007/BF02276640. http://dx.doi.org/10.1007/BF02276640

    Google Scholar 

  63. L. Lamport, A new solution of dijkstra’s concurrent programming problem. Commun. ACM 17(8), 453–455 (1974). doi:10.1145/361082.361093. http://doi.acm.org/10.1145/361082.361093

    Google Scholar 

  64. L. Lamport, Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  65. L. Lamport, Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978). doi:10.1145/359545.359563. http://doi.acm.org/10.1145/359545.359563

    Google Scholar 

  66. L. Lamport, An assertional correctness proof of a distributed algorithm. Sci. Comput. Program. 2(3), 175–206 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  67. L. Lamport, Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5(2), 190–222 (1983). doi:10.1145/69624.357207. http://doi.acm.org/10.1145/69624.357207

    Google Scholar 

  68. L. Lamport, A fast mutual exclusion algorithm. ACM Trans. Comput. Syst. 5(1), 1–11 (1987). doi:10.1145/7351.7352. http://doi.acm.org/10.1145/7351.7352

    Google Scholar 

  69. L. Lamport, A simple approach to specifying concurrent systems. Commun. ACM 32(1), 32–45 (1989). doi:10.1145/63238.63240. http://doi.acm.org/10.1145/63238.63240

    Google Scholar 

  70. L. Lamport, A theorem on atomicity in distributed algorithms. Distrib. Comput. 4, 59–68 (1990). http://dx.doi.org/10.1007/BF01786631. doi:10.1007/BF01786631

    Google Scholar 

  71. L. Lamport, The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994). doi:10.1145/177492.177726. http://doi.acm.org/10.1145/177492.177726

    Google Scholar 

  72. L. Lamport, How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Comput. 46(7), 779–782 (1997). doi:10.1109/12.599898. http://dx.doi.org/10.1109/12.599898

    Google Scholar 

  73. L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley Longman, Boston, 2002)

    Google Scholar 

  74. L. Lamport, F.B. Schneider, Pretending atomicity. Technical report, Cornell University, Ithaca, 1989

    Google Scholar 

  75. D. Leinenbach, T. Santen, Verifying the microsoft hyper-v hypervisor with vcc, in: Proceedings of the 2nd World Congress on Formal Methods, FM ’09 (Springer, Berlin/Heidelberg, 2009), pp. 806–809. doi:10.1007/978-3-642-05089-3_51. http://dx.doi.org/10.1007/978-3-642-05089-3_51

    Google Scholar 

  76. K. Li, P. Hudak, Memory coherence in shared virtual memory systems. ACM Trans. Comput. Syst. 7(4), 321–359 (1989). doi:http://doi.acm.org/10.1145/75104.75105

    Google Scholar 

  77. N.A. Lynch, Distributed Algorithms (Morgan Kaufmann, San Francisco, 1996)

    MATH  Google Scholar 

  78. N.A. Lynch, M.R. Tuttle, Hierarchical correctness proofs for distributed algorithms, in Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC ’87 (ACM, New York, 1987), pp. 137–151. doi:10.1145/41840.41852. http://doi.acm.org/10.1145/41840.41852

  79. N.A. Lynch, M.R. Tuttle, An introduction to input/output automata. Technical report, MIT/LCS/TM-373 (1988). Also CWI-Quarterly, September 1989 Massachusetts Institute of Technology, Laboratory for Computer Science, 2(3), 219–246,

    Google Scholar 

  80. Z. Manna, A. Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs. Sci. Comput. Program. 4(3), 257–289 (1984). doi:10.1016/0167-6423(84)90003-0. http://dx.doi.org/10.1016/0167-6423(84)90003-0

    Google Scholar 

  81. Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems (Springer, New York, 1992)

    Book  Google Scholar 

  82. Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety (Springer, New York, 1995)

    Book  Google Scholar 

  83. J. Misra, A discipline of multiprogramming. ACM Comput. Surv. 28(4es) (1996). doi:10.1145/242224.242286. http://doi.acm.org/10.1145/242224.242286

    Google Scholar 

  84. J. Misra, A Discipline of Multiprogramming: Programming Theory for Distributed Applications (Springer, Secaucus, 2001)

    Book  MATH  Google Scholar 

  85. S.L. Murphy, A.U. Shankar, A note on the drinking philosophers. ACM TOPLAS 10(1), 178–188 (1988)

    MATH  Google Scholar 

  86. S.L. Murphy, A.U. Shankar, Connection management for the transport layer: service specification and protocol verification. IEEE Trans. Commun. 39(12), 1762–1775 (1991). doi:10.1109/26.120163. Earlier version in Proceedings ACM SIGCOMM ’87 Workshop, Stowe, Vermont, Aug 1987

    Article  Google Scholar 

  87. A.L. Oláh, Design and Analysis of Transport Protocols for Reliable High-Speed Communications. Ph.D. thesis, University of Twente, Enschede, 1997. http://doc.utwente.nl/13676/

  88. A.L. Oláh, S.M.H.d. Groot, Assertional verification of a connection management protocol, in Proceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques VIII (Chapman and Hall, London, 1996), pp. 401–416. http://dl.acm.org/citation.cfm?id=646214.681518

  89. A.L. Oláh, S.M. Heemstra de Groot, Alternative specification and verification of a periodic state exchange protocol. IEEE/ACM Trans. Netw. 5(4), 525–529 (1997). doi:10.1109/90.649467. http://dx.doi.org/10.1109/90.649467

    Google Scholar 

  90. S. Owicki, D. Gries, An axiomatic proof technique for parallel programs – i. Acta Inform. 6, 319–340 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  91. S. Owicki, D. Gries, Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976). doi:http://doi.acm.org/10.1145/360051.360224

    Google Scholar 

  92. S. Owicki, L. Lamport, Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455–495 (1982). doi:10.1145/357172.357178. http://doi.acm.org/10.1145/357172.357178

    Google Scholar 

  93. S. Owre, N. Shankar, A brief overview of pvs, in TPHOLs ’08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (Springer, Berlin/Heidelberg, 2008), pp. 22–27. doi:{\url{http://dx.doi.org/10.1007/978-3-540-71067-7_5

    Google Scholar 

  94. D.L. Parnas, A technique for software module specification with examples. Commun. ACM 15(5), 330–336 (1972). doi:10.1145/355602.361309. http://doi.acm.org/10.1145/355602.361309

    Google Scholar 

  95. G.L. Peterson, Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)

    Article  MATH  Google Scholar 

  96. L.L. Peterson, B.S. Davie, Computer Networks: A Systems Approach, 3rd edn. (Morgan Kaufmann, San Francisco, 2003)

    Google Scholar 

  97. A. Pnueli, The temporal logic of programs, in: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS ’77 (IEEE Computer Society, Washington DC, 1977), pp. 46–57. doi:10.1109/SFCS.1977.32. http://dx.doi.org/10.1109/SFCS.1977.32

  98. A. Pnueli, The temporal semantics of concurrent programs. in Proceedings of the International Sympoisum on Semantics of Concurrent Computation (Springer, London, 1979), pp. 1–20. http://dl.acm.org/citation.cfm?id=647172.716123

  99. A.A. Schoone, Verification of connection-management protocols. Technical report, DSpace at Utrecht University, Netherlands, 1987 [http://dspace.library.uu.nl:8080/dspace-oai/request]. http://igitur-archive.library.uu.nl/math/2006-1214-201341/UUindex.html

  100. A.U. Shankar, Verified data transfer protocols with variable flow control. ACM Trans. Comput. Syst. 7(3), 281–316 (1989). doi:10.1145/65000.65003. http://doi.acm.org/10.1145/65000.65003

    Google Scholar 

  101. A.U. Shankar, An introduction to assertional reasoning for concurrent systems. ACM Comput. Surv. 25(3), 225–262 (1993). doi:10.1145/158439.158441. http://doi.acm.org/10.1145/158439.158441

    Google Scholar 

  102. A.U. Shankar, S.S. Lam, An HDLC protocol specification and its verification using image protocols. ACM Trans. Comput. Syst. 1(4), 331–368 (1983). doi:10.1145/357377.357384. http://doi.acm.org/10.1145/357377.357384

    Google Scholar 

  103. A.U. Shankar, S.S. Lam, Time-dependent distributed systems: proving safety, liveness and real-time properties. Distrib. Comput. 2, 61–79 (1987). http://dx.doi.org/10.1007/BF01667079. doi:10.1007/BF01667079

    Google Scholar 

  104. A.U. Shankar, S.S. Lam, A stepwise refinement heuristic for protocol construction. ACM Trans. Program. Lang. Syst. 14(3), 417–461 (1992). doi:10.1145/129393.129394. http://doi.acm.org/10.1145/129393.129394. Earlier version appeared in Stepwise Refinement of Distributed Systems, LNCS 430, Springer, 1990

    Google Scholar 

  105. A.U. Shankar, D. Lee, Minimum-latency transport protocols with modulo-n incarnation numbers. IEEE/ACM Trans. Netw. 3(3), 255–268 (1995). doi:10.1109/90.392385. http://dx.doi.org/10.1109/90.392385

    Google Scholar 

  106. K. Slind, M. Norrish: A brief overview of hol4, in: TPHOLs ’08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (Springer, Berlin/Heidelberg, 2008), pp. 28–32. doi:http://dx.doi.org/10.1007/978-3-540-71067-7_6

    Google Scholar 

  107. M.G. Staskauskas, The formal specification and design of a distributed electronic funds-transfer system. IEEE Trans. Comput. 37(12), 1515–1528 (1988). doi:10.1109/12.9730. http://dx.doi.org/10.1109/12.9730

    Google Scholar 

  108. W.R. Stevens, UNIX Network Programming, vol 1. Second Edition: Networking APIs: Sockets and XTI. (Prentice-Hall, Englewood Cliffs, 1998). Chapter 4, ISBN 0-13-490012-X

  109. K. Suonio, A Practical Theory of Reactive Systems: Incremental Modeling of Dynamic Behaviors (Springer, Secaucus, 2005). (Texts in Theoretical Computer Science. An EATCS Series)

    Google Scholar 

  110. R.E. Tarjan, J. van Leeuwen, Worst-case analysis of set union algorithms. J. ACM 31(2), 245–281 (1984). doi:10.1145/62.2160. http://doi.acm.org/10.1145/62.2160

    Google Scholar 

  111. G. Taubenfeld, The black-white bakery algorithm and related bounded-space, adaptive, local-spinning and fifo algorithms, in DISC, ACM (Association for Computing Machinery), New York, pp. 56–70 (2004)

    Google Scholar 

  112. G. Tel, Assertional verification of a timer-based protocol. Technical report, DSpace at Utrecht University, Netherlands, 1987 [http://dspace.library.uu.nl:8080/dspace-oai/request]. http://igitur-archive.library.uu.nl/math/2006-1214-201352/UUindex.html

  113. G. Tel, F. Mattern, The derivation of distributed termination detection algorithms from garbage collection schemes. sACM Trans. Program. Lang. Syst. 15(1), 1–35 (1993). doi:10.1145/151646.151647. http://doi.acm.org/10.1145/151646.151647

    Google Scholar 

  114. G. Tel, R.B. Tan, J. van Leeuwen, The derivation of graph marking algorithms from distributed termination detection protocols. Sci. Comput. Program. 10(2), 107–137 (1988). doi:10.1016/0167-6423(88)90024-X. http://dx.doi.org/10.1016/0167-6423(88)90024-X

    Google Scholar 

  115. M. Trehel, M. Naimi, A distributed algorithm for mutual exclusion based on data structures and fault tolerance, in: 6th Annual International Phoenix Conference on Computers and Communication (Scottsdale, Arizona, 1987), pp. 35–39

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Maryland, Paint Branch Dr, College Park, MD, USA

    A. Udaya Shankar

Authors
  1. A. Udaya Shankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer Science+Business Media New York

About this chapter

Cite this chapter

Shankar, A.U. (2013). Introduction. In: Distributed Programming. Springer, New York, NY. https://doi.org/10.1007/978-1-4614-4881-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4614-4881-5_1

  • Published:

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4614-4880-8

  • Online ISBN: 978-1-4614-4881-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation