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] [thread-next>] [day] [month] [year] [list]

Message-ID: <20250714124208.qVXvUVqp@linutronix.de>
Date: Mon, 14 Jul 2025 14:42:08 +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:18:05PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-07-11 at 15:17 +0200, Nam Cao wrote:
> > The 'next' operator is a unary operator. It is defined as: "next
> > time, the
> > operand must be true".
> > 
> > Support this operator. For RV monitors, "next time" means the next
> > invocation of ltl_validate().
> > 
> > Signed-off-by: Nam Cao <namcao@...utronix.de>
> 
> Hi Nam,
> 
> thanks for the series, I did a very stupid test like this:
> 
>   RULE = always (SCHEDULING imply next SWITCH)
> 
> Despite the monitor working or not, the generator created code that
> doesn't build, specifically:
> 
> 1. It creates a variable named switch
>   - sure I could change the name, but perhaps we could prepend
> something to make sure local variables are not C keywords

Right. Maybe we can prefix them with "ltl_".

> 2. It created unused variables in ltl_start
>   - _fill_atom_values creates all variables but _fill_start uses only
> those where the .init field is true (maybe the model is wrong though)

Not sure what you mean by .init field, but yes the scripts always generate
all variables, even if they are unused. Let me change the scripts.

> Now, this specific model reports errors without the sched_switch_vain
> tracepoint which I'm introducing in another patch.
> 
> For it to work, I have to define it in such a way that scheduling
> becomes true at schedule_entry and becomes false right after the
> switch:
> 
> schedule_entry
> 	SCHEDULING=true
> 
> sched_switch
> 	SWITCH=true
> 
> schedule_exit
> 	SCHEDULING=false
> 	SWITCH=false
> 
> If I understood correctly that's intended behaviour since swapping the
> assignments in schedule_exit (or doing a pulse in sched_switch) would
> add another event when scheduling is true, which is against the next
> requirement.

Yes.

> 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))

because I think the parser understood your rule as:

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

Defining an operator precedence rules is on my TODO list. Unfortunately no
theory defines this AFAIK, so it is not obvious how should they be defined.

> but the parser got the two SCHEDULING as two different atoms, so I
> guess I did something I was not supposed to do..

This is just the parser's shortcoming. Currently it thinks that they are
different variables.

> Is the next operator only meaningful for atoms that are mutually
> exclusive (e.g. RED next GREEN, if GREEN is true RED turns to false)
> and/or when playing with ltl_atom_set without triggering validations?
> 
> What am I missing here?

I hope the above already answered your questions. Let me know if anything
is unclear.

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

Best regards,
Nam