On Mon, Jun 30, 2025 at 08:34:01PM -0400, Steven Rostedt wrote:
> On Tue, 10 Jun 2025 11:43:42 +0200
> Nam Cao <nam...@linutronix.de> wrote:
> > +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
