caa a22 4500 445869712 CHVBK 20180317145508.0 cr unu---uuuuu 170323e20110401xx s 000 0 eng 10.1007/s00236-011-0132-0 doi (NATIONALLICENCE)springer-10.1007/s00236-011-0132-0 Nonatomic dual bakery algorithm with bounded tokens [Elektronische Daten] [Alex Aravind, Wim Hesselink] A simple mutual exclusion algorithm is presented that only uses nonatomic shared variables of bounded size, and that satisfies bounded overtaking. When the shared variables behave atomically, it has the first-come-first-served property (FCFS). Nonatomic access makes information vulnerable. The effects of this can be mitigated by minimizing the information and by spreading it over more variables. The design approach adopted here begins with such mitigating efforts. These resulted in an algorithm with a proof of correctness, first for atomic variables. This proof is then used as a blueprint for the simultaneous development of the algorithm for nonatomic variables and its proof. Mutual exclusion is proved by means of invariants. Bounded overtaking and liveness under weak fairness are proved with invariants and variant functions. Liveness under weak fairness is formalized and proved in a set-theoretic version of temporal logic. All these assertions are verified with the proof assistant PVS. We heavily rely on the possibility offered by a proof assistant like PVS to reuse proofs developed for one context in a different context. Springer-Verlag, 2011 Aravind Alex Computer Science Program, University of Northern British Columbia, V2N4Z9, Prince George, BC, Canada aut Hesselink Wim Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK, Groningen, The Netherlands aut Acta Informatica Springer-Verlag 48/2(2011-04-01), 67-96 0001-5903 48:2<67 2011 48 236 https://doi.org/10.1007/s00236-011-0132-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s00236-011-0132-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Aravind Alex Computer Science Program, University of Northern British Columbia, V2N4Z9, Prince George, BC, Canada aut NATIONALLICENCE 700 1- Hesselink Wim Department of Computing Science, University of Groningen, P.O. Box 407, 9700 AK, Groningen, The Netherlands aut NATIONALLICENCE 773 0- Acta Informatica Springer-Verlag 48/2(2011-04-01), 67-96 0001-5903 48:2<67 2011 48 236 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer