[PATCH 0/2] rv/ltl: Support the 'next' operator

[PATCH 0/2] rv/ltl: Support the 'next' operator

[Nam Cao]

Hi,

In the theory of linear temporal logic, there is also the 'next' unary
operator defined as: next time, the operand must be true.

During my initial implementation, I thought kernel RV monitors would not
have a use case for this operator. Therefore I omitted it.

However, me and Gabriele had a conversion off list, and he may have a use
case for this operator.

Therefore, implement the theory completely and add the 'next' operator.

Nam Cao (2):
  rv/ltl: Do not execute the Buchi automaton twice on start condition
  verification/rvgen: Support the 'next' operator

 .../trace/rv/linear_temporal_logic.rst        |  1 +
 include/rv/ltl_monitor.h                      |  4 ++-
 tools/verification/rvgen/rvgen/ltl2ba.py      | 26 +++++++++++++++++++
 3 files changed, 30 insertions(+), 1 deletion(-)

-- 
2.39.5

[PATCH 1/2] rv/ltl: Do not execute the Buchi automaton twice on start condition

[Nam Cao]

On start condition of a Buchi automaton, the automaton is executed twice.

This is fine for now, as all the current LTL operators do not care about
this. But it would break the 'next' operator, which will be introduced in a
follow-up patch.

Prepare for the introduction of the 'next' operator, only execute the
automaton once on start condition.

Signed-off-by: Nam Cao <namcao@linutronix.de>
---
 include/rv/ltl_monitor.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
index 9a583125b566..67031a774e3d 100644
--- a/include/rv/ltl_monitor.h
+++ b/include/rv/ltl_monitor.h
@@ -167,8 +167,10 @@ static void ltl_atom_update(struct task_struct *task, enum ltl_atom atom, bool v
 	ltl_atom_set(mon, atom, value);
 	ltl_atoms_fetch(task, mon);
 
-	if (!rv_ltl_valid_state(mon))
+	if (!rv_ltl_valid_state(mon)) {
 		ltl_attempt_start(task, mon);
+		return;
+	}
 
 	ltl_validate(task, mon);
 }
-- 
2.39.5

[PATCH 2/2] verification/rvgen: Support the 'next' operator

[Nam Cao]

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@linutronix.de>
---
 .../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:
-- 
2.39.5

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

[Gabriele Monaco]

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@linutronix.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:

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

[Nam Cao]

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@linutronix.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

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

[Nam Cao]

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

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

[Nam Cao]

On Mon, Jul 14, 2025 at 02:48:04PM +0200, Nam Cao wrote:
>      RULE = always (((not SCHEDULING) and (next SCHEDULING)) imply (next next SWITCH))

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".

Nam

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

[Gabriele Monaco]

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@redhat.com>

Thanks again,
Gabriele