- if
- :: get_pid() >= NR_READERS ->
- smp_mb_pid(get_pid(), j);
- i = 0;
- do
- :: i < NR_READERS ->
- smp_mb_pid(i, j);
- i++;
- :: i >= NR_READERS -> break
- od;
- smp_mb_pid(get_pid(), j);
- :: else -> skip;
- fi;
+ smp_mb_pid(get_pid(), j);
+ i = 0;
+ do
+ :: i < NR_READERS ->
+ smp_mb_pid(i, j);
+ i++;
+ :: i >= NR_READERS -> break
+ od;
+ smp_mb_pid(get_pid(), j);
+}
+
+inline smp_mb_reader(i, j)
+{
+ skip;