Formal verification of an array-based nonblocking queue

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.