Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. (English) Zbl 1312.68153
Summary: A simplification of the mutual exclusion algorithm of E. A. Lycklama and V. Hadzilacos [“A first-come-first-served mutual-exclusion algorithm with small communication variables”, ACM Trans. Program. Lang. Syst. 13, No. 4, 558–576 (1991; doi:10.1145/115372.115370)] is presented. It uses only four nonatomic shared bits per thread to guarantee mutual exclusion with the first-come-first-served property. The algorithm is verified by assertional methods, aided by the proof assistant PVS. A variation with five bits per thread is also given. This variation may give better performance when the number of threads is large. The use of the proof assistant made it easy to transfer the proof of the main algorithm to the variation.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68W05 | Nonnumerical algorithms |
Keywords:
mutual exclusion algorithmSoftware:
SPINReferences:
| [1] | Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82, 253-284 (1991) · Zbl 0728.68083 · doi:10.1016/0304-3975(91)90224-P |
| [2] | Abraham, U.: Bakery algorithms. In: Proceedings of the Concurrency, Specification, and Programming, Workshop, pp. 7-40 (1993) |
| [3] | Anderson, J.H., Gouda, M.G.: Atomic semantics of nonatomic programs. Inf. Process. Lett. 28, 99-103 (1988) · Zbl 0658.68017 · doi:10.1016/0020-0190(88)90171-8 |
| [4] | Anderson, J.H., Kim, Y.J., Herman, T.: Shared-memory mutual exclusion: major research trends since 1986. Discret. Comput. 16, 75-110 (2003) · Zbl 1448.68061 |
| [5] | Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, Reading (2000) |
| [6] | Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, New York (2009) · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5 |
| [7] | Aravind, A.A., Hesselink, W.H.: A queue based mutual exclusion algorithm. Acta Inf. 46, 73-86 (2009) · Zbl 1172.68041 · doi:10.1007/s00236-008-0086-z |
| [8] | Aravind, A.A., Hesselink, W.H.: Nonatomic dual bakery algorithm with bounded tokens. Acta Inf. 48, 67-96 (2011) · Zbl 1244.68083 · doi:10.1007/s00236-011-0132-0 |
| [9] | Ashcroft, E.: Proving assertions about parallel programs. J. Comput. Syst. Sci. 10, 110-135 (1975) · Zbl 0299.68013 · doi:10.1016/S0022-0000(75)80018-3 |
| [10] | Burns, J.E.: Complexity of Communication Among Asynchronous Parallel Processes. Ph.D. Thesis, School of Information and Computer Science, Georgia Institute of Technology (1981) · Zbl 0658.68017 |
| [11] | Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999) |
| [12] | de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification, Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2001) · Zbl 1009.68020 |
| [13] | Dijkstra, E.W.: Solution of a problem in concurrent programming control. Commun. ACM 8, 569 (1965) · doi:10.1145/365559.365617 |
| [14] | Dijkstra, E.W.: Co-operating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43-112. NATO Advanced Study Institute, Academic Press, London (1968) · Zbl 1266.68215 |
| [15] | Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17, 643-644 (1974) · Zbl 0305.68048 · doi:10.1145/361179.361202 |
| [16] | Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976) · Zbl 0368.68005 |
| [17] | Doherty, S., Herlihy, M., Luchangco, V., Moir, M.: Bringing practical lock-free synchronization to 64-bit applications. In: Proceedings of the 23rd Annual ACM Symposium on Principles of Distributed Computing, pp. 31-39. ACM Press, New York, NY, USA (2004) |
| [18] | Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distr. Comput. 17, 21-42 (2005) · Zbl 1264.68217 · doi:10.1007/s00446-004-0115-2 |
| [19] | Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free parallel and concurrent garbage collection by mark &sweep. Sci. Comput. Program. 64, 341-374 (2007) · Zbl 1178.68528 · doi:10.1016/j.scico.2006.10.001 |
| [20] | Gao, H., Hesselink, W.H.: A general lock-free algorithm using compare-and-swap. Inf. Comput. 205, 225-241 (2007) · Zbl 1107.68119 · doi:10.1016/j.ic.2006.10.003 |
| [21] | Haldar, S., Vitanyi, P.: Bounded concurrent timestamp systems using vector clocks. J. ACM 49, 101-126 (2002) · Zbl 1323.68408 · doi:10.1145/505241.505246 |
| [22] | Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Francisco (2008) |
| [23] | Hesselink, W.H.: Wait-free linearization with a mechanical proof. Distr. Comput. 9, 21-36 (1995) · Zbl 1448.68110 · doi:10.1007/BF01784240 |
| [24] | Hesselink, W.H.: A mechanical proof of Segall’s PIF algorithm. Formal Aspects Comput. 9, 208-226 (1997) · Zbl 0874.68264 · doi:10.1007/BF01211619 |
| [25] | Hesselink, W.H.: The verified incremental design of a distributed spanning tree algorithm: extended abstract. Formal Aspects Comput. 11, 45-55 (1999) · Zbl 0937.68111 · doi:10.1007/s001650050035 |
| [26] | Hesselink, W.H.: Using eternity variables to specify and prove a serializable database interface. Sci. Comput. Program. 51, 47-85 (2004) · Zbl 1091.68041 · doi:10.1016/j.scico.2003.06.001 |
| [27] | Hesselink, W.H.: Universal extensions to simulate specifications. Inf. Comput. 206, 108-128 (2008) · Zbl 1133.68044 · doi:10.1016/j.ic.2007.10.003 |
| [28] | Hesselink, W.H.: Revisiting mutual exclusion by Lycklama-Hadzilacos, PVS scripts. http://wimhesselink.nl/mechver/mx4bits (2010) · Zbl 1312.68153 |
| [29] | Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576-583 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259 |
| [30] | Holzmann, G.J.: The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2004) |
| [31] | Inoue, T., Hironaka, T., Sasaki, T., Fukae, S., Koide, T., Mattausch, H.J.: Evaluation of bank-based multiport memory architecture with blocking network. Electron. Commun. Japan 89, 498-510 (2006) · doi:10.1002/ecja.10230 |
| [32] | Israeli, A., Li, M.: Bounded time-stamps. Distr. Comput. 6, 205-209 (1993) · Zbl 0776.68018 · doi:10.1007/BF02242708 |
| [33] | Jayanti, P., Petrovic, S.: Efficient and practical constructions of LL/SC variables. In: PODC ’03: Proceedings of the twenty-second annual symposium on Principles of Distributed Computing, pp. 285-294. ACM Press, New York, NY, USA (2003) · Zbl 1321.68472 |
| [34] | Jayanti, P., Petrovic, S.: Efficient wait-free implementation of multiword LL/SC variables. In: Proceedings of the 25th IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 59-68. IEEE (2005) · Zbl 1264.68217 |
| [35] | Jayanti, P., Tan, K., Friedland, G., Katz, A.: Bounding Lamport’s Bakery algorithm. In: Proceedings of the SOFSEM, vol. 2234. LNCS, pp. 261-270 (2001) · Zbl 1052.68979 |
| [36] | Kim, Y.J., Anderson, J.H.: Nonatomic mutual exclusion with local spinning. Distr. Comput. 19, 19-61 (2006) · Zbl 1266.68215 · doi:10.1007/s00446-006-0003-z |
| [37] | Ladkin, P., Lamport, L., Olivier, B., Roegel, D.: Lazy caching in TLA. Distr. Comput. 12, 151-174 (1999) · Zbl 1448.68132 · doi:10.1007/s004460050063 |
| [38] | Lamport, L.: A new solution of Dijkstra’s concurrent programming problem. Commun. ACM 17, 453-455 (1974) · Zbl 0281.68004 · doi:10.1145/361082.361093 |
| [39] | Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. SE-3 2, 125-143 (1977) · Zbl 0349.68006 · doi:10.1109/TSE.1977.229904 |
| [40] | Lamport, L.: A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst. 1, 84-97 (1979) · Zbl 0463.68022 · doi:10.1145/357062.357068 |
| [41] | Lamport, L.: The mutual exclusion problem—part I: a theory of interprocess communication, part II: statement and solutions. J. ACM 33, 313-348 (1986) · Zbl 0627.68017 · doi:10.1145/5383.5384 |
| [42] | Lamport, L.: On interprocess communication. Parts I and II. Distr. Comput. 1, 77-101 (1986) · Zbl 0598.68022 · doi:10.1007/BF01786227 |
| [43] | Lamport, L.: Win and sin: predicate transformers for concurrency. ACM Trans. Program. Lang. Syst. 12, 396-428 (1990) · doi:10.1145/78969.78970 |
| [44] | Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 872-923 (1994) · doi:10.1145/177492.177726 |
| [45] | Lamport, L.: Composition: a way to make proofs harder. In: de Roever, W.-P., Pnueli, H. (eds.) Compositionality: The Significant Difference, vol. 1536. LNCS, pp. 402-423. Springer, Berlin (1997) |
| [46] | Lycklama, E.A., Hadzilacos, V.: A first-come-first-served mutual-exclusion algorithm with small communication variables. ACM Trans. Program. Lang. Syst. 13, 558-576 (1991) · doi:10.1145/115372.115370 |
| [47] | Lynch, N.A.: Distributed Algorithms. Morgan Kaufman, San Francisco (1996) · Zbl 0877.68061 |
| [48] | Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992) · Zbl 0753.68003 · doi:10.1007/978-1-4612-0931-7 |
| [49] | Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, New York (1995) · Zbl 1288.68169 · doi:10.1007/978-1-4612-4222-2 |
| [50] | Michael, M.M.: Practical lock-free and wait-free LL/SC/VL implementations using 64-bit CAS. In: Guerraoui, R. (ed.) 18th International Symposium on Distributed Computing, vol. 3274. LNCS, pp. 144-158 (2004) |
| [51] | Michael, M.M.: Scalable lock-free dynamic memory allocation. In: Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 35-46 (2004) |
| [52] | Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Inf. 6, 319-340 (1976) · Zbl 0312.68011 · doi:10.1007/BF00268134 |
| [53] | Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Version 2.4, System Guide, Prover Guide, PVS Language Reference. http://pvs.csl.sri.com (2001) |
| [54] | Raynal, M.: Algorithms for Mutual Exclusion. MIT Press, Cambridge (1986) · Zbl 0662.68002 |
| [55] | Rusinoff, D.M.: A mechanically verified incremental garbage collector. Formal Aspects Comput. 6, 359-390 (1994) · Zbl 0941.68624 · doi:10.1007/BF01211305 |
| [56] | Shiue, W.-T., Chakrabarti, C.: Multi-module multi-port memory design for low power embedded systems. Des. Autom. Embed. Syst. 9, 235-261 (2004) · doi:10.1007/s10617-005-1195-3 |
| [57] | Sundell, H., Tsigas, P.: Scalable and lock-free concurrent dictionaries. In: Proceedings of the 2004 ACM Symposium on Applied Computing, pp. 1438-1445. ACM Press (2004) · Zbl 0941.68624 |
| [58] | Takamura, M., Igarashi, Y.: Simple mutual exclusion algorithms based on bounded tickets on the asynchronous shared memory model. In: Proceedings of the COCOON, vol. 2387. LNCS, pp. 259-268 (2002) · Zbl 1077.68538 |
| [59] | Taubenfeld, G.: The black-white bakery algorithm and related bounded-space, adaptive, local-spinning and FIFO algorithms. In: Proceedings of the DISC, vol. 3274. LNCS, pp. 56-70 (2004) · Zbl 1110.68546 |
| [60] | Taubenfeld, G.: Synchronization Algorithms and Concurrent Programming. Pearson Education/Prentice Hall, London (2006) |
| [61] | Tel, G.: Distributed Algorithms. Cambridge University Press, Cambridge (1994) · Zbl 0803.00026 · doi:10.1007/BFb0020419 |
| [62] | Vijayaraghavan, S.: A variant of the bakery algorithm with bounded values as a solution to Abraham’s concurrent programming problem. In: Proceedings of the Design, Analysis and Simulation of Distributed Systems (2003) · Zbl 0598.68023 |
| [63] | Welch, J., Lamport, L., Lynch, N.A.: A lattice-structured proof technique applied to a minimum-weight spanning tree algorithm. In: Proceedings 7th ACM Symposium on Principles of, Distributed Computing (1988) · Zbl 0463.68022 |
| [64] | Woo, T.-K.: A note on Lamport’s mutual exclusion algorithm. SIGOPS Oper. Syst. Rev. 24(4), 78-81 (1990) · doi:10.1145/94574.94581 |
| [65] | Zuo, W., Qi, Z., Jiaxing, L.: An intelligent multi-port memory. In: Proceedings of the IEEE International Symposium on Information Technology Application Workshops, pp. 251-254 (2008) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
