On Mon, Jun 30, 2025 at 08:34:01PM -0400, Steven Rostedt wrote:

On Tue, 10 Jun 2025 11:43:42 +0200
Nam Cao [off-list ref] wrote:

quoted

+static void
+ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
+{
+	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
+	bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
+	bool val40 = task_is_rcu || task_is_migration;
+	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
+	bool val41 = futex_lock_pi || val40;
+	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
+	bool val5 = block_on_rt_mutex || val41;
+	bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
+	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
+	bool val32 = abort_sleep || kthread_should_stop;
+	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
+	bool val33 = woken_by_nmi || val32;
+	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
+	bool val34 = woken_by_hardirq || val33;
+	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
+	     mon->atoms);
+	bool val14 = woken_by_equal_or_higher_prio || val34;
+	bool wake = test_bit(LTL_WAKE, mon->atoms);
+	bool val13 = !wake;
+	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
+	bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
+	bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
+	bool val24 = nanosleep_clock_monotonic || nanosleep_clock_tai;
+	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
+	bool val25 = nanosleep_timer_abstime && val24;
+	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
+	bool val18 = clock_nanosleep && val25;
+	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
+	bool val9 = futex_wait || val18;
+	bool val11 = val9 || kernel_thread;
+	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
+	bool val2 = !sleep;
+	bool rt = test_bit(LTL_RT, mon->atoms);
+	bool val1 = !rt;
+	bool val3 = val1 || val2;
+
+	switch (state) {
+	case S0:
+		if (val3)
+			__set_bit(S0, next);
+		if (val11 && val13)
+			__set_bit(S1, next);
+		if (val11 && val14)
+			__set_bit(S4, next);
+		if (val5)
+			__set_bit(S5, next);
+		break;

What's with all the magic numbers?

Can we turn these into enums so they have some meaning for us humans?

I'm not sure what you mean, we can't use enums as variables.

I haven't come up with a good way of (automatically) giving them meaningful
names. They are just intermediate values (e.g. 'and' of other values).
Maybe I should integrate AI in my scripts ;)

There's another option: we could drop all these intermediate variables and
use the atomic propositions directly. So I could hack my scripts:

diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py
index d11840af7f5fd..1d1eeb82ae834 100644
--- a/tools/verification/rvgen/rvgen/ltl2ba.py
+++ b/tools/verification/rvgen/rvgen/ltl2ba.py

@@ -118,11 +118,7 @@ class ASTNode:
         return self.op.expand(self, node, node_set)
 
     def __str__(self):
-        if isinstance(self.op, Literal):
-            return str(self.op.value)
-        if isinstance(self.op, Variable):
-            return self.op.name.lower()
-        return "val" + str(self.id)
+        return str(self.op).lower()
 
     def normalize(self):
         # Get rid of:

@@ -147,6 +143,9 @@ class BinaryOp:
         yield from self.left
         yield from self.right
 
+    def __str__(self):
+        return "(%s %s %s)" % (self.left.op, self.op_str, self.right.op)
+
     def normalize(self):
         raise NotImplementedError
 

@@ -358,6 +357,9 @@ class Variable:
     def __iter__(self):
         yield from ()
 
+    def __str__(self):
+        return self.name
+
     def negate(self):
         new = ASTNode(self)
         return NotOp(new)

diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py
index b8da9094fb4ff..dfa625d130233 100644
--- a/tools/verification/rvgen/rvgen/ltl2k.py
+++ b/tools/verification/rvgen/rvgen/ltl2k.py

@@ -109,17 +109,8 @@ class ltl2k(generator.Monitor):
     def _fill_atom_values(self):
         buf = []
         for node in self.ltl:
-            if node.op.is_temporal():
-                continue
-
             if isinstance(node.op, ltl2ba.Variable):
                 buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (node, node.op.name))
-            elif isinstance(node.op, ltl2ba.AndOp):
-                buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right))
-            elif isinstance(node.op, ltl2ba.OrOp):
-                buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right))
-            elif isinstance(node.op, ltl2ba.NotOp):
-                buf.append("\tbool %s = !%s;" % (node, node.op.child))
         buf.reverse()
 
         buf2 = []

And we would get:

static void
ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)
{
	bool task_is_migration = test_bit(LTL_TASK_IS_MIGRATION, mon->atoms);
	bool task_is_rcu = test_bit(LTL_TASK_IS_RCU, mon->atoms);
	bool futex_lock_pi = test_bit(LTL_FUTEX_LOCK_PI, mon->atoms);
	bool block_on_rt_mutex = test_bit(LTL_BLOCK_ON_RT_MUTEX, mon->atoms);
	bool kthread_should_stop = test_bit(LTL_KTHREAD_SHOULD_STOP, mon->atoms);
	bool abort_sleep = test_bit(LTL_ABORT_SLEEP, mon->atoms);
	bool woken_by_nmi = test_bit(LTL_WOKEN_BY_NMI, mon->atoms);
	bool woken_by_hardirq = test_bit(LTL_WOKEN_BY_HARDIRQ, mon->atoms);
	bool woken_by_equal_or_higher_prio = test_bit(LTL_WOKEN_BY_EQUAL_OR_HIGHER_PRIO,
	     mon->atoms);
	bool wake = test_bit(LTL_WAKE, mon->atoms);
	bool kernel_thread = test_bit(LTL_KERNEL_THREAD, mon->atoms);
	bool nanosleep_clock_tai = test_bit(LTL_NANOSLEEP_CLOCK_TAI, mon->atoms);
	bool nanosleep_clock_monotonic = test_bit(LTL_NANOSLEEP_CLOCK_MONOTONIC, mon->atoms);
	bool nanosleep_timer_abstime = test_bit(LTL_NANOSLEEP_TIMER_ABSTIME, mon->atoms);
	bool clock_nanosleep = test_bit(LTL_CLOCK_NANOSLEEP, mon->atoms);
	bool futex_wait = test_bit(LTL_FUTEX_WAIT, mon->atoms);
	bool sleep = test_bit(LTL_SLEEP, mon->atoms);
	bool rt = test_bit(LTL_RT, mon->atoms);

	switch (state) {
	case S0:
		if ((!rt || !sleep))
			__set_bit(S0, next);
		if (!wake && ((futex_wait || (clock_nanosleep && (nanosleep_timer_abstime &&
		   (nanosleep_clock_monotonic || nanosleep_clock_tai)))) || kernel_thread))
			__set_bit(S1, next);
		if (((futex_wait || (clock_nanosleep && (nanosleep_timer_abstime &&
		   (nanosleep_clock_monotonic || nanosleep_clock_tai)))) || kernel_thread) &&
		   (woken_by_equal_or_higher_prio || (woken_by_hardirq || (woken_by_nmi ||
		   (abort_sleep || kthread_should_stop)))))
			__set_bit(S5, next);
		if ((block_on_rt_mutex || (futex_lock_pi || (task_is_rcu || task_is_migration))))
			__set_bit(S6, next);
		break;


It is just a matter of taste. I will let you pick. Or do you hate this one
as well?

Best regards,
Nam