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 for Android: free password hash cracker in your pocket

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

Message-ID: <20250714124802.kjqjNWmr@linutronix.de>
Date: Mon, 14 Jul 2025 14:48:02 +0200
From: Nam Cao <namcao@...utronix.de>
To: Gabriele Monaco <gmonaco@...hat.com>
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, 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))

Or if you want to allow some other things to happen inbetween, then:

     RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (SCHEDULING until SWITCH))

Best regards,
Nam