Very nice paper; it seems to cover datastructures used for several different algorithms. I've only glanced at it so far, as it is quite long. I noticed in 1.1.

Very nice paper; it seems to cover datastructures used for several different algorithms. I've only glanced at it so far, as it is quite long. I noticed in 1.1.5 "Correctness" that it discusses equivalency of locking, sequential non-locking and combining tree methods. This is the bread and butter that I'm personally looking for, but it appears that the paper doesn't do any more than just mention methods that are used for proving correctness and equivalency. Can anyone recommend some good resources that delve into that topic? I'd also love to read about mapping high-level concurrency to low-level locking primitives, and specifically how to prove correctness. Again. :D