Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Alan Stern
On Fri, 16 Nov 2018, Boqun Feng wrote: > > -let rcu-rscsi = po ; rcu-rscs^-1 ; po? > > +let rcu-gp = [Sync-rcu](* Compare with gp *) > > +let rcu-rscsi = rcu-rscs^-1 > > Isn't it more straight-forward to use "rcu-rscs^-1" other than > "rcu-rscsi" in the definition of "rcu-fence", is

Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Alan Stern
On Fri, 16 Nov 2018, Boqun Feng wrote: > > -let rcu-rscsi = po ; rcu-rscs^-1 ; po? > > +let rcu-gp = [Sync-rcu](* Compare with gp *) > > +let rcu-rscsi = rcu-rscs^-1 > > Isn't it more straight-forward to use "rcu-rscs^-1" other than > "rcu-rscsi" in the definition of "rcu-fence", is

Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Boqun Feng
Hi Alan, On Thu, Nov 15, 2018 at 11:19:58AM -0500, Alan Stern wrote: > In preparation for adding support for SRCU, refactor the definitions > of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po? > terms from the first two to the second two. An rcu-gp relation is > added; it is

Re: [PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Boqun Feng
Hi Alan, On Thu, Nov 15, 2018 at 11:19:58AM -0500, Alan Stern wrote: > In preparation for adding support for SRCU, refactor the definitions > of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po? > terms from the first two to the second two. An rcu-gp relation is > added; it is

[PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Alan Stern
In preparation for adding support for SRCU, refactor the definitions of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po? terms from the first two to the second two. An rcu-gp relation is added; it is equivalent to gp with the po and po? terms removed. This is necessary because for

[PATCH 2/3] tools/memory-model: Refactor some RCU relations

2018-11-15 Thread Alan Stern
In preparation for adding support for SRCU, refactor the definitions of rcu-fence, rcu-rscsi, rcu-link, and rb by moving the po and po? terms from the first two to the second two. An rcu-gp relation is added; it is equivalent to gp with the po and po? terms removed. This is necessary because for