On Thu, 22 Sep 2022, Yuan Can wrote:

>
> 在 2022/9/21 4:24, Markus Elfring 写道:
> > > > > +@r3@
> > > > > +identifier s, fld;
> > > > > +position p != {r2.p};
> > > > Why do you think that such a SmPL constraint would be required?
> > > >
> > > >
> > > > > +@@
> > > > > +
> > > > > +struct s {
> > > > > +  ...
> > > > > +  struct mutex fld@p;
> > > > > +  ...
> > > > > +};
> > > > Why would the source code search repetition matter here?
> > > He is searching for a structure that is different from the ones matched
> > > previously.
> > How many mutexes (or spin locks) should be initialised before further data
> > processing can be safely performed with corresponding structures?
>
> In my opinion, every mutexes and spin locks needs to be initialised before
> use.

I think that the concern is that you require that some spinlock is
initialized in the file before you are able to find one that is not.  It
could be good to check this with an artificial test case.

julia