Re: [PATCH] tools/memory-model: update: remove rb-dep, smp_read_barrier_depends, and lockless_dereference

[Akira Yokosawa]

On 2018/02/22 2:15, Alan Stern wrote:
> Commit bf28ae562744 ("tools/memory-model: Remove rb-dep,
> smp_read_barrier_depends, and lockless_dereference") was accidentally
> merged too early, while it was still in RFC form.  This patch adds in
> the missing pieces.
> 
> Akira pointed out some typos in the original patch, and he noted that
> cheatsheet.txt should be updated to indicate how unsuccessful RMW
> operations relate to address dependencies.

My point was to separate unannotated loads from READ_ONCE(), if the
cheatsheet should concern such accesses as well.
Unsuccessful RMW operations were brought up by Andrea.

> 
> Andrea pointed out that the macro for rcu_dereference() in linux.def
> should now use the "once" annotation instead of "deref".  He also
> suggested that the comments should mention commit 5a8897cc7631
> ("locking/atomics/alpha: Add smp_read_barrier_depends() to
> _release()/_relaxed() atomics") as an important precursor, and he
> contributed commit cb13b424e986 ("locking/xchg/alpha: Add
> unconditional memory barrier to cmpxchg()"), another prerequisite.
> 
> Signed-off-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Suggested-by: Akira Yokosawa <akiyks@xxxxxxxxx>
> Suggested-by: Andrea Parri <parri.andrea@xxxxxxxxx>
> Fixes: bf28ae562744 ("tools/memory-model: Remove rb-dep, smp_read_barrier_depends, and lockless_dereference")
> 

The change itself looks good to me.

Acked-by: Akira Yokosawa <akiyks@xxxxxxxxx>

       Thanks, Akira

> ---
> 
>  tools/memory-model/Documentation/cheatsheet.txt  |    6 +++---
>  tools/memory-model/Documentation/explanation.txt |    4 ++--
>  tools/memory-model/linux-kernel.def              |    2 +-
>  3 files changed, 6 insertions(+), 6 deletions(-)
> 
> Index: usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/cheatsheet.txt
> +++ usb-4.x/tools/memory-model/Documentation/cheatsheet.txt
> @@ -1,11 +1,11 @@
>                                    Prior Operation     Subsequent Operation
>                                    ---------------  ---------------------------
>                                 C  Self  R  W  RWM  Self  R  W  DR  DW  RMW  SV
> -                              __  ----  -  -  ---  ----  -  -  --  --  ---  --
> +                              --  ----  -  -  ---  ----  -  -  --  --  ---  --
>  
>  Store, e.g., WRITE_ONCE()            Y                                       Y
> -Load, e.g., READ_ONCE()              Y                              Y        Y
> -Unsuccessful RMW operation           Y                              Y        Y
> +Load, e.g., READ_ONCE()              Y                          Y   Y        Y
> +Unsuccessful RMW operation           Y                          Y   Y        Y
>  rcu_dereference()                    Y                          Y   Y        Y
>  Successful *_acquire()               R                   Y  Y   Y   Y    Y   Y
>  Successful *_release()         C        Y  Y    Y     W                      Y
> Index: usb-4.x/tools/memory-model/Documentation/explanation.txt
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/Documentation/explanation.txt
> +++ usb-4.x/tools/memory-model/Documentation/explanation.txt
> @@ -826,7 +826,7 @@ A-cumulative; they only affect the propa
>  executed on C before the fence (i.e., those which precede the fence in
>  program order).
>  
> -read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
> +read_read_lock(), rcu_read_unlock(), and synchronize_rcu() fences have
>  other properties which we discuss later.
>  
>  
> @@ -1138,7 +1138,7 @@ final effect is that even though the two
>  program order, it appears that they aren't.
>  
>  This could not have happened if the local cache had processed the
> -incoming stores in FIFO order.  In constrast, other architectures
> +incoming stores in FIFO order.  By contrast, other architectures
>  maintain at least the appearance of FIFO order.
>  
>  In practice, this difficulty is solved by inserting a special fence
> Index: usb-4.x/tools/memory-model/linux-kernel.def
> ===================================================================
> --- usb-4.x.orig/tools/memory-model/linux-kernel.def
> +++ usb-4.x/tools/memory-model/linux-kernel.def
> @@ -13,7 +13,7 @@ WRITE_ONCE(X,V) { __store{once}(X,V); }
>  smp_store_release(X,V) { __store{release}(*X,V); }
>  smp_load_acquire(X) __load{acquire}(*X)
>  rcu_assign_pointer(X,V) { __store{release}(X,V); }
> -rcu_dereference(X) __load{deref}(X)
> +rcu_dereference(X) __load{once}(X)
>  
>  // Fences
>  smp_mb() { __fence{mb} ; }
>