rcu: Decrease memory-barrier usage based on semi-formal proof