Re: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")

[Akira Yokosawa <akiyks@gmail.com>]

On 2018/02/09 17:07:03 -0800, Paul E. McKenney wrote:
> On Sat, Feb 10, 2018 at 08:46:25AM +0900, Akira Yokosawa wrote:
>> >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Fri, 9 Feb 2018 04:51:05 -0800
>> Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_")
>>
>> As of herd7 7.47, these '-'s are not permitted and end up in
>> errors such as:
>>
>>     File "./linux-kernel.def", line 44, characters 29-30:
>>     unexpected '-' (in macros)
>>
>> Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU
>> identifiers match ASPLOS paper") in the repository at
>> https://github.com/aparri/memory-model can restore the compatibility
>> with herd7 7.47.
>>
>> Reported-by: Patrick Bellasi <patrick.bellasi@arm.com>
>> Suggested-by: Andrea Parri <parri.andrea@gmail.com>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>> Paul,
>>
>> FWIW, this is a squashed version relative to patch 07/10 in the RFC series.
> 
> Thank you, Akira!
> 
> I am going to hold off on this for a bit to see if we can instead get
> a new release of herd7, but if we can't. this might well be a very good
> way to go.

So, herdtools7.7.48 is now available by "opam update; opam upgrade".
Maybe mentioning the required version of herdtools7 in README would help.

One glitch I'm aware of is one of the output of klitmus7 fails to
compile on kernels prior to 4.14, because of smp_mb__after_spinlock()
used in Z6.0+pooncelock+poonceLock+pombonce.litmus.

And there is a question I want to ask.

Z6.0+pooncelock+pooncelock+pombonce.litmus, which doesn't have
smp_mb__after_spinlock(), has a comment of:

(*
 * Result: Never
 *
 * This example demonstrates that a pair of accesses made by different
 * processes each while holding a given lock will not necessarily be
 * seen as ordered by a third process not holding that lock.
 *)

The result was changed from "Sometimes" to "Never" in response to
Alan's feedback the other day, but the following comment indicates
the result should be "Sometimes". And the current model gives the
result of "Sometimes".

As I have no idea of the pending patches, I'd like to know once
the pending patches are applied, would 
Z6.0+pooncelock+pooncelock+pombonce.litmus and
Z6.0+pooncelock+poonceLock+pombonce.litmus become identical?

    Thanks, Akira

> 
> 							Thanx, Paul
[...]
d_lock*)  ||
>> +		'rcu_unlock (*rcu_read_unlock*) ||
>> +		'sync_rcu (*synchronize_rcu*) ||
>>  		'before_atomic (*smp_mb__before_atomic*) ||
>>  		'after_atomic (*smp_mb__after_atomic*) ||
>>  		'after_spinlock (*smp_mb__after_spinlock*)
>> @@ -35,8 +35,8 @@ instructions F[Barriers]
>>
>>  (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *)
>>  let matched = let rec
>> -	    unmatched-locks = Rcu-lock \ domain(matched)
>> -	and unmatched-unlocks = Rcu-unlock \ range(matched)
>> +	    unmatched-locks = Rcu_lock \ domain(matched)
>> +	and unmatched-unlocks = Rcu_unlock \ range(matched)
>>  	and unmatched = unmatched-locks | unmatched-unlocks
>>  	and unmatched-po = [unmatched] ; po ; [unmatched]
>>  	and unmatched-locks-to-unlocks =
>> @@ -46,8 +46,8 @@ let matched = let rec
>>  	in matched
>>
>>  (* Validate nesting *)
>> -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking
>> -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking
>> +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking
>>
>>  (* Outermost level of nesting only *)
>>  let crit = matched \ (po^-1 ; matched ; po^-1)
>> diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
>> index babe2b3..d0085d5 100644
>> --- a/tools/memory-model/linux-kernel.cat
>> +++ b/tools/memory-model/linux-kernel.cat
>> @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) |
>>  	([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) |
>>  	([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) |
>>  	([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M])
>> -let gp = po ; [Sync-rcu] ; po?
>> +let gp = po ; [Sync_rcu] ; po?
>>
>>  let strong-fence = mb | gp
>>
>> diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
>> index a397387..fc08371 100644
>> --- a/tools/memory-model/linux-kernel.def
>> +++ b/tools/memory-model/linux-kernel.def
>> @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; }
>>  spin_trylock(X) __trylock(X)
>>
>>  // RCU
>> -rcu_read_lock() { __fence{rcu-lock}; }
>> -rcu_read_unlock() { __fence{rcu-unlock};}
>> -synchronize_rcu() { __fence{sync-rcu}; }
>> -synchronize_rcu_expedited() { __fence{sync-rcu}; }
>> +rcu_read_lock() { __fence{rcu_lock}; }
>> +rcu_read_unlock() { __fence{rcu_unlock};}
>> +synchronize_rcu() { __fence{sync_rcu}; }
>> +synchronize_rcu_expedited() { __fence{sync_rcu}; }
>>
>>  // Atomic
>>  atomic_read(X) READ_ONCE(*X)
>> -- 
>> 2.7.4
>>
>>
>