On Fri, May 24, 2024 at 08:09:28PM +0200, Jonas Oberhauser wrote:
>
>
> Am 5/24/2024 um 4:53 PM schrieb Alan Stern:
> > Question: Since R and RMW have different lists of allowable tags, how
> > does herd7 decide which tags are allowed for an event that is in both
> > the R and RMW sets?
>
> After looking over the patch draft for herd7 written by Hernan [1], my best
> guess is: it doen't. It seems that after herd7 detects you are using LKMM it
> simply drops all tags except 'acquire on read and 'release on store.
> Everything else becomes 'once (and 'mb adds some F[mb] sometimes).
Okay, yes, this is the sort of thing we would like to move away from.
> That means that if one were to go through with the earlier suggestion to
> distinguish between the smp_mb() Mb and the cmpxchg() Mb, e.g. by calling
> the latter RmwMb, current herd7 would always erase the RmwMb tag because it
> is not called "acquire" or "release".
> The same would happen of course if you introduced an RmwAcquire tag.
>
> So there are several options:
>
> - treat the tags as a syntactic thing which is always present, and
> specify their meaning purely in the cat file, analogous to what you
> have defined above. This is personally my favorite solution. To
> implement this in herd7 we would simply remove all the current special
> cases for the LKMM barriers, which I like.
>
> However then we need to actually define the behavior of herd if
> an inappropriate tag (like release on a load) is provided. Since the
> restriction is actually mostly enforced by the .def file - by simply
> not providing a smp_store_acquire() etc. -, that only concerns RMWs,
> where xchg_acquire() would apply the Acquire tag to the write also.
>
> The easiest solution is to simply remove the syntax for specifying
> restrictions - it seems it is not doing much right now anyways - and
> do the filtering inside .bell, with things like
>
> (* only writes can have Release tags *)
> let Release = Release & W \ (RMW \ rng(rmw))
>
> One good thing about this way is that it would work even without
> modifying herd, since it is in a sense idempotent with the
> transformations done by herd.
This seems like a good approach.
> FWIW, in our internal weak memory model in Dresden we did exactly this,
> and use REL for the syntax and Rel for the semantic release ordering to
> make the distinction more clear, with things like:
>
> let Acq = (ACQ | SC) & (R | F)
> let Rel = (REL | SC) & (W | F)
>
> (SC is our equivalent to LKMM's Mb)
Definitely, the syntactic markers should be easily distinguished (by
case would be a good way) from the semantic classes used in the model.
> - treat the tags as semantic markers that are only present or not under
> some circumstances, and define the semantics fully based on the present
> tags. The circumstances are currently hardcoded in herd7, but we should
> move them out with some syntax like __cmpxchg{acquire}{once}.
>
> This requires touching the parser and of course still has the issue
> with the acquire tag appearing on the store as well.
>
> - provide a full syntax for defining the event sequence that is
> expected. For example, for a cmpxchg we could do
>
> cmpxchg = { F[success-cmpxchg]; c = R&RMW[once]; if (c==v) {
> W&RMW[once]; } F[success-cmpxchg] }
>
> and then define in .bell that a success-cmpxchg is an mb if it is
> directly next to a cmpxchg that succeeds.
>
> The advantage is that you can customize the representation to whatever
> kernel devs thing is the most intuitive. The downside is that it
> requires major rewrites to herd7, someone to think about a reasonable
> language for specifying this etc.
Let's avoid major rewrites to herd7.
Alan
