3 ms·
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 obstru
by pmjordan 17y ago
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.
- barrkel 17y agoCliff 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: http://video.google.com/videoplay?docid=2139967204534450862# http://video.google.com/videoplay?docid=2139967204534450862# (Cliff Click was architect and lead developer for the HotSpot server JIT compiler.)
- pmjordan 17y agoI'll check it out, thanks.
- yread 17y agoI 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...