linux-kernel - Re: [PATCH 2/2] verification/rvgen: Support the 'next' operator

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: Windows password security audit tool. GUI, reports in PDF.

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

Message-ID: <f9c8b5d5a0eeb3f1ebae601383ddb984f9df91ad.camel@redhat.com>
Date: Mon, 14 Jul 2025 15:56:21 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>
Cc: Steven Rostedt <rostedt@...dmis.org>, John Ogness	
 <john.ogness@...utronix.de>, Masami Hiramatsu <mhiramat@...nel.org>,
 Mathieu Desnoyers <mathieu.desnoyers@...icios.com>,
 linux-trace-kernel@...r.kernel.org, 	linux-kernel@...r.kernel.org
Subject: Re: [PATCH 2/2] verification/rvgen: Support the 'next' operator

On Mon, 2025-07-14 at 14:48 +0200, Nam Cao wrote:
> On Mon, Jul 14, 2025 at 02:42:10PM +0200, Nam Cao wrote:
> > On Mon, Jul 14, 2025 at 02:18:05PM +0200, Gabriele Monaco wrote:
> > > Now I can't think of a way to rewrite the model to allow a pulse
> > > in
> > > sched_switch, that is /whenever scheduling turns to true, the
> > > next
> > > event is a switch/ instead of /any time scheduling is true, the
> > > next
> > > event is a switch/.
> > > 
> > > I tried something like:
> > >   RULE = always ((not SCHEDULING and next SCHEDULING) imply next
> > > SWITCH)
> > 
> > Be careful of operator precedence. This rule is also what I would
> > suggest,
> > but you need parentheses:
> > 
> >     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> > (next SWITCH))
> 
> Actually no, this also does not work. You need double 'next':
> 
>      RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply
> (next next SWITCH))
> 

Thanks! This one seems to work.

> Not sure what you mean by .init field

I meant in ltl2k there's this condition for variable usage but not for
variable definition. I'm not sure exactly what it stands for.
  _fill_start():
	...
	if not node.init:
		continue

But I guess you got what I meant already.

> Btw, I think this "(not X) and (next X)" seems very useful. So we
> could
> define a helper for this, perhaps something like "rising_edge".

Yeah good idea! I see myself mixing up in the future otherwise..
I guess you'd need to define also a falling_edge for its counterpart.
Or perhaps making it more compact as just rising/falling (with good
documentation or references to somewhere defining it).

Also we need to make clear this operator takes 2 instances, so whatever
happens after (next) it needs a double next.

Maybe it gets complicated but in the future we might have also some
nextN (next2, next3, etc. with a sensible limit not to explode the
generated code) or something along the line.

> Thanks for the report, I will post some patches to address these
> problems
> with the scripts.

Great, thanks!
I'd say since those are unrelated and the next works as intended, feel
free to add

Tested-by: Gabriele Monaco <gmonaco@...hat.com>

Thanks again,
Gabriele