Thread (23 messages) 23 messages, 5 authors, 2025-04-02

Re: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor

From: Nam Cao <hidden>
Date: 2025-03-12 14:30:08
Also in: lkml

On Wed, Mar 12, 2025 at 07:47:50AM +0100, Gabriele Monaco wrote:
On Tue, 2025-03-11 at 18:05 +0100, Nam Cao wrote:
quoted
-/*
- * Futher monitor types are expected, so make this a union.
- */
 union rv_task_monitor {
-	struct da_monitor da_mon;
+	struct da_monitor	da_mon;
+	struct ltl_monitor	ltl_mon;
 };
This adds quite some memory overhead if we have multiple per-task
monitors (we might in the future) and we don't use this ltl monitors.
What about keeping it conditionally compiled out?
You could define the struct only if e.g. CONFIG_RV_LTL_MONITORS is set,
select it with any LTL monitor via Kconfig, then glue it somehow to
have it readable.
Good point.
quoted
diff --git a/tools/verification/ltl2ba/generate.py
b/tools/verification/ltl2ba/generate.py
new file mode 100755
index 000000000000..52d5b3618e64
--- /dev/null
+++ b/tools/verification/ltl2ba/generate.py
You may want to rename this script to something more unique, just in
case one day we decide to make it possible to install this generator on
the system (like dot2k/dot2c).
Acked. Inspired by the dot2k name, maybe something like ltl2k.
quoted
+ * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_%%MODEL_NAME%%_init() must have been
called with a positive
+ * data_size.
+ */
+static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor
*mon)
+{
+	return &mon->data;
+}
Do we need all those functions defined here? We could have them
generated by the pre-processor just like with DA monitors.

Having a ltl_monitor.h defining all common utility functions and
variables (here I'm assuming most are, indeed, common) may save a lot
of maintenance.
I avoided macros like with DA monitors, they are hard to grep. But your
point on maintenance is true from my experience working on this series..

Pre-processor it is then.
Also I would rearrange monitors sources a bit differently, like putting
everything that doesn't need manual intervention (states and atoms
lists) in the header, remaining functions that may need tracepoint
wiring or more complex stuff can stay in a single c file, a bit like
current da monitors.

I see there seems to be more manual work in the main C file (e.g.
rtapp_block.c), but I think it would look cleaner if all other code was
generated by the preprocessor in a common header and all lists/inlined
functions created by the script stay in a separate header (why not call
it rtapp_block.h?).

What do you think?
Sounds better, let me give me a try.

Thanks so much for the suggestions,
Nam
Keyboard shortcuts
hback out one level
jnext message in thread
kprevious message in thread
ldrill in
Escclose help / fold thread tree
?toggle this help