Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
27 lines (21 sloc) 268 Bytes
C C-S-rcunoderef-2
(* Result: Never *)
{
}
P0(int *a, int *b)
{
WRITE_ONCE(*a, 1);
synchronize_rcu();
*b = 2;
}
P1(int *a, int *b)
{
int *r1;
rcu_read_lock();
r1 = READ_ONCE(*a);
if (r1 == 0)
*b = 1;
rcu_read_unlock();
}
locations [1:r1]
exists (~b=2)
You can’t perform that action at this time.