On Fri, 20 Mar 2020, Joel Fernandes (Google) wrote: > This adds an example for the important RCU grace period guarantee, which > shows an RCU reader can never span a grace period. > > Signed-off-by: Joel Fernandes (Google) <joel@xxxxxxxxxxxxxxxxx> > --- > .../litmus-tests/RCU+sync+free.litmus | 40 +++++++++++++++++++ > 1 file changed, 40 insertions(+) > create mode 100644 tools/memory-model/litmus-tests/RCU+sync+free.litmus > > diff --git a/tools/memory-model/litmus-tests/RCU+sync+free.litmus b/tools/memory-model/litmus-tests/RCU+sync+free.litmus > new file mode 100644 > index 0000000000000..c4682502dd296 > --- /dev/null > +++ b/tools/memory-model/litmus-tests/RCU+sync+free.litmus > @@ -0,0 +1,40 @@ > +C RCU+sync+free > + > +(* > + * Result: Never > + * The following comment needs some rewriting. The grammar is somewhat awkward and a very important "not" is missing. > + * This litmus test demonstrates that an RCU reader can never see a write after > + * the grace period, if it saw writes that happen before the grace period. An RCU reader can never see a write that follows a grace period if it did _not_ see writes that precede the grace period. > This > + * is a typical pattern of RCU usage, where the write before the grace period > + * assigns a pointer, and the writes after destroy the object that the pointer > + * points to. ... that the pointer used to point to. > + * > + * This guarantee also implies, an RCU reader can never span a grace period and > + * is an important RCU grace period memory ordering guarantee. Unnecessary comma, and it is not clear what "This" refers to. The whole sentence should be phrased differently: This is one implication of the RCU grace-period guarantee, which says (among other things) that an RCU reader cannot span a grace period. Alan
