From experience: this is a lot harder than it may look. On a tangent: does anyone here know of techniques or algorithms for verifying that a lock-free or obstruction-free algorithm works? Ideally some that can actually be applied in practice. So far I've been manually trying out all possible scheduling combinations, which is very tedious and can be error prone on larger algorithms. It's also not clear if doing the analysis for 2 concurrent threads automatically extends to 3 or more (it clearly does for some algorithms).
I've been thinking along the lines of a DSL for such algorithms that can compile down to whatever language you need, but also easily lends itself to static analysis for verification, but I feel my lack of classical CompSci training is letting me down here a bit.
Cliff Click's presentation of his lock-free hash table is interesting in this respect. He used a different approach - based on state machines - for reasoning about correctness:
I implemented read-copy-update in a kernel in an experimental OS and it was indeed quite a lot of work. But I guess that it can improve performance quite a bit. However, RCU is only for kernel code...
Out of curiosity, what languages do you use at work? I was surprised recently to find that there are STM libraries of varying degrees of maturity for a lot more languages than I thought. Most of them feel bolted on, of course, but there might be something.
Personally, I think that hardware transactional memory can't come fast enough. We're already seeing a basic form of it on Sun's to-be-released Rock processor, but there are much more advanced types of HTM that have been developed in the past few years. With hardware support, the performance penalty of using transactional memory pretty much evaporates. The hardware doesn't have to be too terribly elaborate, either.
I've been thinking along the lines of a DSL for such algorithms that can compile down to whatever language you need, but also easily lends itself to static analysis for verification, but I feel my lack of classical CompSci training is letting me down here a bit.