On Mon, Jan 23, 2023 at 07:25:48PM +0100, Jonas Oberhauser wrote: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
Alright, after some synchronization in the other parts of this thread I amWouldn't it need to have po|co? Consider:
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:How should we resolve this?
On 1/18/2023 8:52 PM, Alan Stern wrote:What about the ordering given through
On Tue, Jan 17, 2023 at 08:31:59PM +0100, Jonas Oberhauser wrote:You can leave it here, but it is already covered by two other parts: the
- ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |Shouldn't the po case of (co | po) remain intact here?
- ([M] ; po ; [UL] ; (co | po) ; [LKW] ;
- fencerel(After-unlock-lock) ; [M])
+ ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M])
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.
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.
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)
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.