WAIT-FREE LINEARIZATION WITH A MECHANICAL PROOF

The correctness of a program for wait-free linearization of an arbitra ry shared data object in bounded memory is verified mechanically. The program uses atomic read-write registers, an array of consensus regist ers and one compare and swap register. In the program, a number of pro cesses concurrently inspect and modify a pointer structure without wai ting. Consequently, the proof of correctness is very delicate. The the orem prover NQTHM of Boyer and Moore has been used to mechanically cer tify the correctness.