Messages in this thread | | | Date | Tue, 24 Jan 2023 13:54:14 +0100 | Subject | Re: [PATCH] tools/memory-model: Make ppo a subrelation of po | From | Jonas Oberhauser <> |
| |
On 1/23/2023 9:25 PM, Alan Stern wrote: > On Mon, Jan 23, 2023 at 07:25:48PM +0100, Jonas Oberhauser wrote: >> Alright, after some synchronization in the other parts of this thread I am >> beginning to prepare the next iteration of the patch. >> >> On 1/19/2023 4:13 AM, Alan Stern wrote: >>> On Wed, Jan 18, 2023 at 10:38:11PM +0100, Jonas Oberhauser wrote: >>>> On 1/18/2023 8:52 PM, Alan Stern wrote: >>>>> On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote: >>>>>> - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | >>>>>> - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; >>>>>> - fencerel(After-unlock-lock) ; [M]) >>>>>> + ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) >>>>> Shouldn't the po case of (co | po) remain intact here? >>>> You can leave it here, but it is already covered by two other parts: the >>>> ordering given through ppo/hb is covered by the po-unlock-lock-po & int in >>>> ppo, and the ordering given through pb is covered by its inclusion in >>>> strong-order. >>> What about the ordering given through >>> A-cumul(strong-fence)/cumul-fence/prop/hb? I suppose that might be >>> superseded by pb as well, but it seems odd not to have it in hb. >> How should we resolve this? >> My current favorite (compromise :D) solution would be to >> 1. still eliminate both po and co cases from first definition of >> strong-fence which is used in ppo, >> 2. define a relation equal to the strong-order in this patch (with po|rf) > Wouldn't it need to have po|co? Consider: > > Wx=1 Rx=1 Ry=1 Rz=1 > lock(s) lock(s) lock(s) > unlock(s) unlock(s) unlock(s) > Wy=1 Wz=1 smp_mb__after_unlock_lock > Rx=0 > > With the co term this is forbidden. With only the rf term it is > allowed, because po-unlock-lock-po isn't A-cumulative. No, but unlock() is ( https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git/tree/tools/memory-model/lock.cat?h=dev.2023.01.19a#n67 ). So you get
Rx=0 ->overwrite Wx=1 ->rfe Rx1 ->po-rel T1:unlock(s) ->rfe T2:lock(s) ->po-unlock-lock-po;after ... fence;po Rx=0 which is Rx=0 ->prop ; po-unlock-lock-po;after ... fence;po Rx=0
Are you ok going forward like this then?
If not, I might prefer to redefine po-unlock-lock-po into something that works for all its use cases if possible. I think |
po ; [UL] ; (po|co?;rf) ; [LKR] ; po
|might be such a definition but haven't fully thought about it.
best wishes, jonas
| |