[lttng-dev] FYI, another paper checking URCU correctness

[Paul E. McKenney]

Hello!

On the off chance that this is new news of interest...

https://arxiv.org/pdf/1606.01400v1.pdf

"Operational Aspects of C/C++ Concurrency", Anton Podkopaev, Ilya Sergey,
Aleksandar Nanevski.

At first glance, they seem to be using a combination of formal
verification and testing, using a simple linked-list usage of URCU.
The state space was too large for their formal technique, so they added
a random state-space sampling approach, sort of like what Promela/spin
does for large problems.  They did promote rcu_dereference() to an
acquire load, but list real rcu_dereference() as future work.

They didn't find any bugs, but their technique did find an injected bug
that resulted in too-short grace periods.

							Thanx, Paul