<div dir="ltr">Thanks so much for your great help.<div>I definitely will look at those resources and papers!</div><div><br></div><div>One more thing that I am confused</div><div>As I mentioned earlier, someone said One key distinction is that both MVCC and RLU provide much stronger consistency guarantees to readers than does RCU ...) (<a href="https://lwn.net/Articles/777036/">https://lwn.net/Articles/777036/</a>).</div><div>I am not sure if the above statement is correct or not. But in general, </div><div>How can we compare RCU consistency guarantees to other techniques (such as RLU)?</div><div>How to reason about which one has stronger or weaker guarantees?</div><div><br></div><div>Thanks</div><div>Yuxin</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Dec 6, 2019 at 11:30 AM Paul E. McKenney <<a href="mailto:paulmck@kernel.org">paulmck@kernel.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Fri, Dec 06, 2019 at 10:59:05AM -0500, Mathieu Desnoyers wrote:<br>
> ----- On Dec 6, 2019, at 3:51 PM, Yuxin Ren <<a href="mailto:ryx@gwmail.gwu.edu" target="_blank">ryx@gwmail.gwu.edu</a>> wrote: <br>
> <br>
> > On Fri, Dec 6, 2019 at 5:49 AM Mathieu Desnoyers < [<br>
> > mailto:<a href="mailto:mathieu.desnoyers@efficios.com" target="_blank">mathieu.desnoyers@efficios.com</a> | <a href="mailto:mathieu.desnoyers@efficios.com" target="_blank">mathieu.desnoyers@efficios.com</a> ] ><br>
> > wrote:<br>
> <br>
> >> ----- On Dec 5, 2019, at 8:17 PM, Yuxin Ren < [ mailto:<a href="mailto:ryx@gwmail.gwu.edu" target="_blank">ryx@gwmail.gwu.edu</a> |<br>
> >> <a href="mailto:ryx@gwmail.gwu.edu" target="_blank">ryx@gwmail.gwu.edu</a> ] > wrote:<br>
> <br>
> >>> Hi,<br>
> >>> I am a student, and learning RCU now, but still know very little about it.<br>
> >>> Are there any documents/papers/materials which (in)formally define and explain<br>
> >>> RCU consistency guarantees?<br>
> <br>
> >> You may want to have a look at<br>
> <br>
> >> User-Level Implementations of Read-Copy Update<br>
> >> Article in IEEE Transactions on Parallel and Distributed Systems 23(2):375 - 382<br>
> >> · March 2012<br>
> <br>
> > Thanks for your info.<br>
> > However, I do not think URCU talks about any consistency model formally.<br>
> <br>
> > From previous communication with Paul, he said RCU is not designed for<br>
> > linearizability, and it is totally acceptable that RCU is not linearizable.<br>
> > However, I am curious how to accurately/formally Characterize RCU consistency<br>
> > model/guarantees<br>
> <br>
> Adding Paul E. McKenney in CC. <br>
> <br>
> I am referring to the section "Overview of RCU semantics" in the paper. Not sure it has the level of <br>
> formality you are looking for though. Paul, do you have pointers to additional material ? <br>
<br>
Indeed I do! The Linux kernel memory model (LKMM) includes RCU. It is<br>
in tools/memory-model in recent kernel source trees, which includes<br>
documentation. This is an executable model, which means that you<br>
can create litmus tests and have the model formally and automatically<br>
evaluate them.<br>
<br>
There are also a number of publications covering LKMM:<br>
<br>
o A formal kernel memory-ordering model<br>
<a href="https://lwn.net/Articles/718628/" rel="noreferrer" target="_blank">https://lwn.net/Articles/718628/</a><br>
<a href="https://lwn.net/Articles/720550/" rel="noreferrer" target="_blank">https://lwn.net/Articles/720550/</a><br>
<br>
These cover the release stores and dependency ordering that<br>
provide RCU's publish-subscribe guarantees.<br>
<br>
Backup material here:<br>
<br>
<a href="https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/" rel="noreferrer" target="_blank">https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/</a><br>
<br>
With these two likely being of particular interest:<br>
<br>
<a href="https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/RCUguarantees.html" rel="noreferrer" target="_blank">https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/RCUguarantees.html</a><br>
<a href="https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/srcu.html" rel="noreferrer" target="_blank">https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/srcu.html</a><br>
<br>
o Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel<br>
<a href="https://dl.acm.org/citation.cfm?id=3177156" rel="noreferrer" target="_blank">https://dl.acm.org/citation.cfm?id=3177156</a><br>
<a href="http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/asplos18.pdf" rel="noreferrer" target="_blank">http://www0.cs.ucl.ac.uk/staff/j.alglave/papers/asplos18.pdf</a><br>
<br>
Backup material:<br>
<br>
<a href="http://diy.inria.fr/linux/" rel="noreferrer" target="_blank">http://diy.inria.fr/linux/</a><br>
<br>
o Who's afraid of a big bad optimizing compiler?<br>
<a href="https://lwn.net/Articles/793253/" rel="noreferrer" target="_blank">https://lwn.net/Articles/793253/</a><br>
<br>
o Calibrating your fear of big bad optimizing compilers<br>
<a href="https://lwn.net/Articles/799218/" rel="noreferrer" target="_blank">https://lwn.net/Articles/799218/</a><br>
<br>
These last two justify use of normal C-language assignment<br>
statements to initialize and access data referenced by<br>
RCU-protected pointers.<br>
<br>
There is a large body of litmus tests (thousands of them) here:<br>
<br>
<a href="https://github.com/paulmckrcu/litmus" rel="noreferrer" target="_blank">https://github.com/paulmckrcu/litmus</a><br>
<br>
Many of these litmus tests involve RCU, and these can be located by<br>
search for files containing rcu_read_lock(), rcu_read_unlock(),<br>
synchronize_rcu(), and so on.<br>
<br>
Or were you looking for something else?<br>
<br>
Thanx, Paul<br>
<br>
> Thanks, <br>
> <br>
> Mathieu <br>
> <br>
> >> as a starting point.<br>
> <br>
> >> Thanks,<br>
> <br>
> >> Mathieu<br>
> <br>
> >>> I know there are some consistency models in the database area (such as PRAM,<br>
> >>> Read Uncommitted, etc) from [ <a href="https://jepsen.io/consistency" rel="noreferrer" target="_blank">https://jepsen.io/consistency</a> |<br>
> >>> <a href="https://jepsen.io/consistency" rel="noreferrer" target="_blank">https://jepsen.io/consistency</a> ] and [1].<br>
> >>> How does RCU related to those consistency models?<br>
> <br>
> >>> I also found some comments online (One key distinction is that both MVCC and RLU<br>
> >>> provide much stronger consistency guarantees to readers than does RCU ...) ( [<br>
> >>> <a href="https://lwn.net/Articles/777036/" rel="noreferrer" target="_blank">https://lwn.net/Articles/777036/</a> | <a href="https://lwn.net/Articles/777036/" rel="noreferrer" target="_blank">https://lwn.net/Articles/777036/</a> ] ).<br>
> >>> I do not understand how we reason/dresibe/compare the consistency guarantees. (<br>
> >>> I even do not know what consistency guarantees provided by RCU formally)<br>
> >>> Could someone explain this to me?<br>
> <br>
> >>> [1] Bailis, P., Davidson, A., Fekete, A., Ghodsi, A., Hellerstein, J. M., &<br>
> >>> Stoica, I. (2013). Highly available transactions: Virtues and limitations.<br>
> >>> Proceedings of the VLDB Endowment, 7(3), 181-192.<br>
> <br>
> >>> Thanks<br>
> >>> Yuxin<br>
> <br>
> >>> _______________________________________________<br>
> >>> lttng-dev mailing list<br>
> >>> [ mailto:<a href="mailto:lttng-dev@lists.lttng.org" target="_blank">lttng-dev@lists.lttng.org</a> | <a href="mailto:lttng-dev@lists.lttng.org" target="_blank">lttng-dev@lists.lttng.org</a> ]<br>
> >>> [ <a href="https://lists.lttng.org/cgi-bin/mailman/listinfo/lttng-dev" rel="noreferrer" target="_blank">https://lists.lttng.org/cgi-bin/mailman/listinfo/lttng-dev</a> |<br>
> >>> <a href="https://lists.lttng.org/cgi-bin/mailman/listinfo/lttng-dev" rel="noreferrer" target="_blank">https://lists.lttng.org/cgi-bin/mailman/listinfo/lttng-dev</a> ]<br>
> <br>
> >> --<br>
> >> Mathieu Desnoyers<br>
> >> EfficiOS Inc.<br>
> >> [ <a href="http://www.efficios.com/" rel="noreferrer" target="_blank">http://www.efficios.com/</a> | <a href="http://www.efficios.com" rel="noreferrer" target="_blank">http://www.efficios.com</a> ]<br>
> <br>
> -- <br>
> Mathieu Desnoyers <br>
> EfficiOS Inc. <br>
> <a href="http://www.efficios.com" rel="noreferrer" target="_blank">http://www.efficios.com</a> <br>
</blockquote></div>