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: <7f4409eae10023a804d24ad2a9c67d368db152cb.camel@redhat.com>
Date: Mon, 14 Jul 2025 14:18:05 +0200
From: Gabriele Monaco <gmonaco@...hat.com>
To: Nam Cao <namcao@...utronix.de>, 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 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

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)

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.

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)
but the parser got the two SCHEDULING as two different atoms, so I
guess I did something I was not supposed to do..

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?

Thanks,
Gabriele

> ---
>  .../trace/rv/linear_temporal_logic.rst        |  1 +
>  tools/verification/rvgen/rvgen/ltl2ba.py      | 26
> +++++++++++++++++++
>  2 files changed, 27 insertions(+)
> 
> diff --git a/Documentation/trace/rv/linear_temporal_logic.rst
> b/Documentation/trace/rv/linear_temporal_logic.rst
> index 57f107fcf6dd..9eee09d9cacf 100644
> --- a/Documentation/trace/rv/linear_temporal_logic.rst
> +++ b/Documentation/trace/rv/linear_temporal_logic.rst
> @@ -41,6 +41,7 @@ Operands (opd):
>  Unary Operators (unop):
>      always
>      eventually
> +    next
>      not
>  
>  Binary Operators (binop):
> diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py
> b/tools/verification/rvgen/rvgen/ltl2ba.py
> index d11840af7f5f..f14e6760ac3d 100644
> --- a/tools/verification/rvgen/rvgen/ltl2ba.py
> +++ b/tools/verification/rvgen/rvgen/ltl2ba.py
> @@ -19,6 +19,7 @@ from ply.yacc import yacc
>  # Unary Operators (unop):
>  #       always
>  #       eventually
> +#       next
>  #       not
>  #
>  # Binary Operators (binop):
> @@ -35,6 +36,7 @@ tokens = (
>     'UNTIL',
>     'ALWAYS',
>     'EVENTUALLY',
> +   'NEXT',
>     'VARIABLE',
>     'LITERAL',
>     'NOT',
> @@ -48,6 +50,7 @@ t_OR = r'or'
>  t_IMPLY = r'imply'
>  t_UNTIL = r'until'
>  t_ALWAYS = r'always'
> +t_NEXT = r'next'
>  t_EVENTUALLY = r'eventually'
>  t_VARIABLE = r'[A-Z_0-9]+'
>  t_LITERAL = r'true|false'
> @@ -327,6 +330,26 @@ class AlwaysOp(UnaryOp):
>          # ![]F == <>(!F)
>          return EventuallyOp(self.child.negate()).normalize()
>  
> +class NextOp(UnaryOp):
> +    def normalize(self):
> +        return self
> +
> +    def _is_temporal(self):
> +        return True
> +
> +    def negate(self):
> +        # not (next A) == next (not A)
> +        self.child = self.child.negate()
> +        return self
> +
> +    @staticmethod
> +    def expand(n: ASTNode, node: GraphNode, node_set) ->
> set[GraphNode]:
> +        tmp = GraphNode(node.incoming,
> +                        node.new,
> +                        node.old | {n},
> +                        node.next | {n.op.child})
> +        return tmp.expand(node_set)
> +
>  class NotOp(UnaryOp):
>      def __str__(self):
>          return "!" + str(self.child)
> @@ -452,12 +475,15 @@ def p_unop(p):
>      '''
>      unop : ALWAYS ltl
>           | EVENTUALLY ltl
> +         | NEXT ltl
>           | NOT ltl
>      '''
>      if p[1] == "always":
>          op = AlwaysOp(p[2])
>      elif p[1] == "eventually":
>          op = EventuallyOp(p[2])
> +    elif p[1] == "next":
> +        op = NextOp(p[2])
>      elif p[1] == "not":
>          op = NotOp(p[2])
>      else: