| [1] |
Apt KR, de Boer FS, Olderog E-R: Verification of sequential and concurrent programs. Springer, New York (2009) · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5 |
| [2] |
Aravind A: Simple, space-efficient, and fairness improved FCFS mutual exclusion algorithms. J Parallel Distrib Comput 73, 1029-1038 (2013) · Zbl 1327.68040 · doi:10.1016/j.jpdc.2013.03.009 |
| [3] |
Afek Y, Stupp G, Touitou D (1999) Long-lived adaptive collect with applications. In: Proceedings 40th IEEE symp. on foundations of computer science, pp 262-272 · Zbl 1448.68056 |
| [4] |
Buhr PA, Dice D, Hesselink WH (2015) High-performance N-thread software solutions for mutual exclusion. Concurr Comput Pract Exp 27:651-701. doi:10.1002/cpe.3263 · Zbl 1312.68153 |
| [5] |
Chandy KM, Misra J: Parallel program design. A foundation. Addison-Wesley, Menlo Park (1988) · Zbl 0717.68034 |
| [6] |
Dijkstra EW: Solution of a problem in concurrent programming control. Commun ACM 8, 569 (1965) · doi:10.1145/365559.365617 |
| [7] |
Hesselink WH: Progress under bounded fairness. Distrib Comput 12, 197-207 (1988) · Zbl 1448.68111 · doi:10.1007/s004460050066 |
| [8] |
Hesselink WH: Mechanical verification of Lamport’s Bakery Algorithm. Sci Comput Program 78, 1622-1638 (2013) · doi:10.1016/j.scico.2013.03.003 |
| [9] |
Hesselink WH: Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. Acta Inf 50, 297-329 (2013) · Zbl 1312.68153 · doi:10.1007/s00236-013-0181-7 |
| [10] |
Hesselink WH (2015) Mutual exclusion by four shared bits with not more than quadratic complexity. Sci Comput Program 102:57-75. doi:10.1016/j.scico.2015.01.001 · Zbl 1327.68040 |
| [11] |
Hesselink WH (2015) PVS proof scripts for four Bakery Algorithms. http://wimhesselink.nl/mechver/bakery/index.html. Accessed 17 March 2016 · Zbl 0312.68011 |
| [12] |
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 |
| [13] |
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 |
| [14] |
Lamport L: On interprocess communication. Parts I and II. Distrib Comput 1, 77-101 (1986) · Zbl 0598.68022 · doi:10.1007/BF01786227 |
| [15] |
Lycklama EA, Hadzilacos V. (1991) A first-come-first-served mutual-exclusion algorithm with small communication variables. ACM Trans Program Lang Syst 13:558-576 |
| [16] |
Misra J: A discipline of multiprogramming: programming theory for distributed applications. Springer, New York (2001) · Zbl 0999.68121 · doi:10.1007/978-1-4419-8528-6 |
| [17] |
Nanevski A, Ley-Wild R, Sergey I, Delbianco GA (2014) Communicating state transition systems for fine-grained concurrent resources. In: Shao Z (ed) ESOP 2014. LNCS, vol 8410, pp 290-310 · Zbl 1405.68219 |
| [18] |
Owicki S, Gries D: An axiomatic proof technique for parallel programs. Acta Inf 6, 319-340 (1976) · Zbl 0312.68011 · doi:10.1007/BF00268134 |
| [19] |
Owre S, Shankar N, Rushby JM, Stringer-Calvert DWJ (2001) PVS version 2.4, system guide, prover guide, PVS language reference. http://pvs.csl.sri.com. Accessed 17 March 2016 |
| [20] |
Taubenfeld G (2004) The Black-White Bakery Algorithm and related bounded-space, adaptive, local-spinning and FIFO algorithms. In: Proceedings of the DISC. LNCS, vol 3274, pp 56-70 · Zbl 1110.68546 |
