Formal verification of an array-based nonblocking queue Export

@inproceedings{citeulike:566171, abstract = {We describe an array-based nonblocking implementation of a concurrent bounded queue, due to Shann, Huang and Chen (2000), and explain how we detected errors in the algorithm while attempting a formal verification. We explain how we first corrected the errors, and then modified the algorithm to obtain nonblocking behaviour in the boundary cases. Both the corrected and modified versions of the algorithm were verified using the PVS theorem proven. We describe the verification of the modified algorithm, which subsumes the proof of the corrected version.}, author = {Colvin, R. and Groves, L.}, booktitle = {Engineering of Complex Computer Systems, 2005. ICECCS 2005. Proceedings. 10th IEEE International Conference on}, citeulike-article-id = {566171}, citeulike-linkout-0 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1467933}, citeulike-linkout-1 = {http://dx.doi.org/10.1109/ICECCS.2005.49}, doi = {10.1109/ICECCS.2005.49}, journal = {Engineering of Complex Computer Systems, 2005. ICECCS 2005. Proceedings. 10th IEEE International Conference on}, keywords = {concurrency, lock-free, nonblocking, queue, simulation, verification}, pages = {507--516}, posted-at = {2006-03-27 22:50:23}, priority = {0}, publisher = {IEEE Computer Society Press}, title = {Formal verification of an array-based nonblocking queue}, url = {http://dx.doi.org/10.1109/ICECCS.2005.49}, year = {2005} }

TY - CONF ID - citeulike:566171 L3 - citeulike-article-id:566171 N2 - We describe an array-based nonblocking implementation of a concurrent bounded queue, due to Shann, Huang and Chen (2000), and explain how we detected errors in the algorithm while attempting a formal verification. We explain how we first corrected the errors, and then modified the algorithm to obtain nonblocking behaviour in the boundary cases. Both the corrected and modified versions of the algorithm were verified using the PVS theorem proven. We describe the verification of the modified algorithm, which subsumes the proof of the corrected version. JF - Engineering of Complex Computer Systems, 2005. ICECCS 2005. Proceedings. 10th IEEE International Conference on EP - 516 TI - Formal verification of an array-based nonblocking queue PB - IEEE Computer Society Press T2 - Engineering of Complex Computer Systems, 2005. ICECCS 2005. Proceedings. 10th IEEE International Conference on SP - 507 KW - concurrency KW - lock-free KW - nonblocking KW - queue KW - simulation KW - verification AU - Colvin, R AU - Groves, L PY - 2005/// UR - http://dx.doi.org/10.1109/ICECCS.2005.49 ER -