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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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
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
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
G.R. Andrews, A method for solving synchronization problems. Sci. Comput. Program. 13(4), 1–21 (1989)
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
K.R. Apt, Ten years of hoare’s logic: a survey-part i. ACM TOPLAS 3, 431–483 (1981)
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
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
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
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
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
R.J. Back, K. Sere, Stepwise refinement of action systems. Software 12, 17–30 (1991)
R.J. Back, J.V. Wright, Contracts, games, and refinement. Inf. Comput. Control 156, 25–45 (2000). doi:10.1006/inco.1999.2820
R.J. Back, J.V. Wright, Compositional action system refinement. Form. Aspects Comput. 15, 103–117 (2003). doi:10.1007/s00165-003-0005-6
M. Ben-Ari, The Art of Multiprocessor Programming, 2nd edn. (Addison-Wesley, San Francisco, 2006)
J.A. Carruth, J. Misra, Proof of a real-time mutual-exclusion algorithm. Parallel Process. Lett. 6(2), 251–257 (1996)
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
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
K.M. Chandy, J. Misra, Parallel Program Design: A Foundation (Addison-Wesley, Boston, 1989)
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
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
E.M. Clarke Jr., O. Grumberg, D.A. Peled, Model Checking (MIT, Cambridge MA, 1999)
E. Cohen, Modular Progress Proofs of Asynchronous Programs, Ph.D. thesis, University of Texas, Austin, 1993. UMI Order No. GAX93-23370
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
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
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
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
D. Comer, Internetworking with TCP/IP, 4th edn. Vol 1: Principles, Protocols, and Architectures (Prentice-Hall, Upper Saddle River, 2000)
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)
E.W. Dijkstra, Cooperating sequential processes. Technical report, Burroughs, Nuenen, 1965. EWD-123
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
E.W. Dijkstra, A correctness proof for communicating processes – a small exercise. Technical report, Burroughs, Nuenen, 1977. EWD-607
E.W. Dijkstra, Two starvation-free solutions of a general exclusion problem. Technical report, Nuenen, 1978. EWD-625
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
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
E.W. Dijkstra, A Discipline of Programming, 1st edn. (Prentice Hall, Upper Saddle River, 1997)
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
E.W. Dijkstra, C.S. Scholten, Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980)
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
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
M.J. Donahoo, K. Calvert, TCP/IP Sockets in C, Practical Guide for Programmers, 2nd edn. (Morgan Kaufmann, Burlington, 2009)
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
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
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
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
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
W.H.J. Feijen, A.J.M. van Gasteren, On a Method of Multiprogramming (Springer, New York, 1999)
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
D. Ginat, Adaptive Ordering of Contending Processes in Distributed Systems. Ph.D. thesis, University of Maryland, Computer Science Department, College Park, 1989. CSTR-2335
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
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
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
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
B. Hailpern, S. Owicki, Modular verification of computer communication protocols. IEEE Trans. Commun. 31(1), 56–68 (1983). doi:10.1109/TCOM.1983.1095720
M. Herlihy, N. Shavit, The Art of Multiprocessor Programming (Morgan Kaufmann, San Francisco, 2008)
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
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
D.E. Knuth: Verification of link-level protocols. BIT 21(1), 31–36 (1981)
R.A. Krzysztof, E.R. Olderog, Verification of Sequential and Concurrent Programs (Springer, New York, 1991)
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
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
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
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
L. Lamport, Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125–143 (1977)
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
L. Lamport, An assertional correctness proof of a distributed algorithm. Sci. Comput. Program. 2(3), 175–206 (1982)
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
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
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
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
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
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
L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley Longman, Boston, 2002)
L. Lamport, F.B. Schneider, Pretending atomicity. Technical report, Cornell University, Ithaca, 1989
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
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
N.A. Lynch, Distributed Algorithms (Morgan Kaufmann, San Francisco, 1996)
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
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,
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
Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems (Springer, New York, 1992)
Z. Manna, A. Pnueli, Temporal Verification of Reactive Systems: Safety (Springer, New York, 1995)
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
J. Misra, A Discipline of Multiprogramming: Programming Theory for Distributed Applications (Springer, Secaucus, 2001)
S.L. Murphy, A.U. Shankar, A note on the drinking philosophers. ACM TOPLAS 10(1), 178–188 (1988)
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
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/
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
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
S. Owicki, D. Gries, An axiomatic proof technique for parallel programs – i. Acta Inform. 6, 319–340 (1976)
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
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
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
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
G.L. Peterson, Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)
L.L. Peterson, B.S. Davie, Computer Networks: A Systems Approach, 3rd edn. (Morgan Kaufmann, San Francisco, 2003)
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
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
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
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
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
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
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
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
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
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
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
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
K. Suonio, A Practical Theory of Reactive Systems: Incremental Modeling of Dynamic Behaviors (Springer, Secaucus, 2005). (Texts in Theoretical Computer Science. An EATCS Series)
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
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)
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
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
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
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
Author information
Authors and Affiliations
Rights 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)