Correctness and concurrent complexity of the Black-White Bakery Algorithm

Formal Aspects of Computing - Tập 28 Số 2 - Trang 325-341 - 2016
Wim H. Hesselink1
1Johann Bernoulli Institute, University of Groningen, Groningen, The Netherlands

Tóm tắt

Abstract

Lamport’s Bakery Algorithm (Commun ACM 17:453–455, 1974 ) implements mutual exclusion for a fixed number of threads with the first-come first-served property. It has the disadvantage, however, that it uses integer communication variables that can become arbitrarily large. Taubenfeld’s Black-White Bakery Algorithm (Proceedings of the DISC. LNCS, vol 3274, pp 56–70, 2004 ) keeps the integers bounded, and is adaptive in the sense that the time complexity only depends on the number of competing threads, say N . The present paper offers an assertional proof of correctness and shows that the concurrent complexity for throughput is linear in N , and for individual progress is quadratic in N . This is proved with a bounded version of UNITY, i.e., by assertional means.

Từ khóa


Tài liệu tham khảo

10.5555/1642724

10.1016/j.jpdc.2013.03.009

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

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

10.5555/59087

10.1145/365559.365617

Hesselink WH, 1988, Progress under bounded fairness, Distrib Comput, 12, 197, 10.1007/s004460050066

10.1016/j.scico.2013.03.003

10.1007/s00236-013-0181-7

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

Hesselink WH (2015) PVS proof scripts for four Bakery Algorithms. http://wimhesselink.nl/mechver/bakery/index.html. Accessed 17 March 2016

10.1145/361082.361093

10.1145/5383.5384

10.1007/BF01786227

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

10.1007/978-1-4419-8528-6

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

10.1007/BF00268134

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

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

Thông tin
Thông tin xuất bản

Formal Aspects of Computing

Tập 28 Số 2

325-341

Thông tin tác giả