summary |
shortlog |
log |
commit | commitdiff |
tree
raw |
patch |
inline | side by side (from parent 1:
1eec319)
Also, the original model I sent out has a minor bug that prevents it
from fully modeling the nested-read-side case. The patch below fixes this.
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
break;
:: tmp < 4 && reader_progress[tmp] != 0 ->
tmp = tmp + 1;
break;
:: tmp < 4 && reader_progress[tmp] != 0 ->
tmp = tmp + 1;
+ :: tmp >= 4 &&
+ reader_progress[0] == reader_progress[3] ->
+ :: tmp >= 4 &&
+ reader_progress[0] != reader_progress[3] ->
+ break;
od;
do
:: tmp < 4 && reader_progress[tmp] == 0 ->
od;
do
:: tmp < 4 && reader_progress[tmp] == 0 ->