abstract_rcu.nim is based on 'Verifying Concurrent Memory Reclamation Algorithms with Grace' (2013) by Alexey Gotsman, Noam Rinetzky, and Hongseok Yang
received 2022-07 from PDF online
abstract_rcu.nim is strictly a proof-of-concept and not intended for other purposes than exploring, testing and understanding the concept behind Read-Copy-Update and Hazard-Pointers. A formal proof of correctness is included in the above cited work.
In Figure.2 the authors show the conceptual algorithm of RCU. This is covered in src/abstract_rcu.nim.
Figure.3 shows a Counter-type with RCU-memory-reclamation. src/ds_rcu/counter.nim tries to implement this counter. More lockfree data-structures will follow, if it turns out that Nim is a suitable workbench for such developments.
More information on RCU and HP
- Wikipedia [ en.wikipedia.org/wiki/Read-copy-update ]
- Wikipedia [ en.wikipedia.org/wiki/Hazard_pointer ]
- McKenney, Walpole, 2007, 'What is RCU, fundamentally?', Linux Weekly News [ http://lwn.net/Articles/262464/ ]
