linux-kernel - Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite for Android: free password hash cracker in your pocket

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <20230125215818.GR2948950@paulmck-ThinkPad-P17-Gen-1>
Date:   Wed, 25 Jan 2023 13:58:18 -0800
From:   "Paul E. McKenney" <paulmck@...nel.org>
To:     Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc:     Alan Stern <stern@...land.harvard.edu>,
        Andrea Parri <parri.andrea@...il.com>,
        Jonas Oberhauser <jonas.oberhauser@...wei.com>,
        Peter Zijlstra <peterz@...radead.org>, will <will@...nel.org>,
        "boqun.feng" <boqun.feng@...il.com>, npiggin <npiggin@...il.com>,
        dhowells <dhowells@...hat.com>,
        "j.alglave" <j.alglave@....ac.uk>,
        "luc.maranget" <luc.maranget@...ia.fr>, akiyks <akiyks@...il.com>,
        dlustig <dlustig@...dia.com>, joel <joel@...lfernandes.org>,
        urezki <urezki@...il.com>,
        quic_neeraju <quic_neeraju@...cinc.com>,
        frederic <frederic@...nel.org>,
        Kernel development list <linux-kernel@...r.kernel.org>
Subject: Re: [Patch 2/2] tools/memory-model: Provide exact SRCU semantics

On Wed, Jan 25, 2023 at 10:04:29PM +0100, Jonas Oberhauser wrote:
> On 1/25/2023 9:21 PM, Alan Stern wrote:
> > LKMM has long provided only approximate handling of SRCU read-side
> > critical sections.  This has not been a pressing problem because LKMM's
> > traditional handling is correct for the common cases of non-overlapping
> > and properly nested critical sections.  However, LKMM's traditional
> > handling of partially overlapping critical sections incorrectly fuses
> > them into one large critical section.

[ . . . ]

> >   synchronize_srcu(X)  { __srcu{sync-srcu}(X); }
> >   synchronize_srcu_expedited(X)  { __srcu{sync-srcu}(X); }
> > Index: usb-devel/tools/memory-model/lock.cat
> > ===================================================================
> > --- usb-devel.orig/tools/memory-model/lock.cat
> > +++ usb-devel/tools/memory-model/lock.cat
> > @@ -36,9 +36,9 @@ let RU = try RU with emptyset
> >   (* Treat RL as a kind of LF: a read with no ordering properties *)
> >   let LF = LF | RL
> > -(* There should be no ordinary R or W accesses to spinlocks *)
> > -let ALL-LOCKS = LKR | LKW | UL | LF | RU
> > -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
> > +(* There should be no ordinary R or W accesses to spinlocks or SRCU structs *)
> > +let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Sync-srcu
> > +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
> 
> Since this was pointed out by Boqun, would it be appropriate to mention him
> in the patch somehow?

Would you be willing to list who contributed what?  Once you and Alan
come to agreement on the list, I would be happy to wordsmith a version
into the commit log.

							Thanx, Paul

> >   (* Link Lock-Reads to their RMW-partner Lock-Writes *)
> >   let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
> 
> Thanks for your patience,
> jonas
>