Proving the Correctness of Nonblocking Data Structures. - DESNOYERS, MATHIEU (Communications of the ACM, 2013)
The article discusses the correctness of nonblocking data structures. Topics covered include language and architecture memory models as considerations when programming nonblocking data structures, the unaligned word-sized memory accesses as a good example of a problem with nonblocking data-structure programming, and how reordering can be conducted at various levels for performance reasons. Also mentioned are the considerations of throughput and scalability tied to atomic accesses and memory barriers, the use of counterexamples to illustrate problems in nonblocking data-structure design and implementation, and execution-based model checking.