Messages in this thread | | | Date | Fri, 20 Feb 2009 12:15:16 -0500 | From | Mathieu Desnoyers <> | Subject | Re: [PATCH URCU formal] Remove spurious read-side infinite loops. |
| |
* Paul E. McKenney (paulmck@linux.vnet.ibm.com) wrote: > Remove spurious read-side infinite loops from urcu_reader() model. >
Merged, thanks !
Mathieu
> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> > --- > formal-model/urcu.spin | 21 +++++++++++++++++---- > 1 files changed, 17 insertions(+), 4 deletions(-) > > diff --git a/formal-model/urcu.spin b/formal-model/urcu.spin > index 611464b..eea18e8 100644 > --- a/formal-model/urcu.spin > +++ b/formal-model/urcu.spin > @@ -27,6 +27,10 @@ bit free = 0; /* Has RCU reclamation happened, e.g., kfree()? */ > bit need_mb = 0; /* =1 says need reader mb, =0 for reader response. */ > byte reader_progress[4]; > /* Count of read-side statement executions. */ > +bit reader_done = 0; > + /* =0 says reader still running, =1 says done. */ > +bit updater_done = 0; > + /* =0 says updater still running, =1 says done. */ > > /* urcu definitions and variables, taken straight from the algorithm. */ > > @@ -50,7 +54,7 @@ proctype urcu_reader() > do > :: need_mb == 1 -> > need_mb = 0; > - :: 1 -> skip; > + :: !updater_done -> skip; > :: 1 -> break; > od; > > @@ -92,7 +96,7 @@ proctype urcu_reader() > reader_progress[2] + > reader_progress[3] == 0) && need_mb == 1 -> > need_mb = 0; > - :: 1 -> skip; > + :: !updater_done -> skip; > :: 1 -> break; > od; > urcu_active_readers = tmp; > @@ -150,7 +154,7 @@ proctype urcu_reader() > do > :: need_mb == 1 -> > need_mb = 0; > - :: 1 -> skip; > + :: !updater_done -> skip; > :: 1 -> break; > od; > :: else -> skip; > @@ -167,11 +171,14 @@ proctype urcu_reader() > od; > assert((tmp_free == 0) || (tmp_removed == 1)); > > + /* Reader has completed. */ > + reader_done = 1; > + > /* Process any late-arriving memory-barrier requests. */ > do > :: need_mb == 1 -> > need_mb = 0; > - :: 1 -> skip; > + :: !updater_done -> skip; > :: 1 -> break; > od; > } > @@ -248,6 +255,12 @@ proctype urcu_updater() > > /* free-up step, e.g., kfree(). */ > free = 1; > + > + /* > + * Signal updater done, ending any otherwise-infinite loops > + * in the reading process. > + */ > + updater_done = 1; > } > > /* > -- > 1.5.2.5 >
-- Mathieu Desnoyers OpenPGP key fingerprint: 8CD5 52C3 8E3C 4140 715F BA06 3F25 A8FE 3BAE 9A68
| |