Re: [PATCH v2 13/22] rv: Add support for LTL monitors

[Nam Cao]

On Fri, Apr 11, 2025 at 01:17:30PM +0200, Gabriele Monaco wrote:
> On Fri, 2025-04-11 at 09:37 +0200, Nam Cao wrote:
> > +struct ltl_monitor {
> > +#ifdef CONFIG_RV_LTL_MONITOR
> > +	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> > +	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> > +	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> > +#endif
> > +};
> 
> Mmh, we have a lot of those ifdefs in quite inappropriate places, but I
> think we can do better than this.
> 
> What about something like:
> 
> #ifdef CONFIG_RV_LTL_MONITOR
> 
> struct ltl_monitor {
> 	DECLARE_BITMAP(states, RV_MAX_BA_STATES);
> 	DECLARE_BITMAP(atoms, RV_MAX_LTL_ATOM);
> 	DECLARE_BITMAP(unknown_atoms, RV_MAX_LTL_ATOM);
> };
> 
> static inline bool rv_ltl_valid_state(struct ltl_monitor *mon)
> {
> 	...
> }
> 
> static inline bool rv_ltl_all_atoms_known(struct ltl_monitor *mon)
> {
> 	...
> }
> 
> #else
> 
> /*
>  * Leave the struct empty not to use up space
>  * In a later patch we could do the same for DAs..
>  */
> struct ltl_monitor { };
> 
> #endif

I have no preference for either, so sure!

> > diff --git a/include/rv/ltl_monitor.h b/include/rv/ltl_monitor.h
> > new file mode 100644
> > index 000000000000..78f5a1197665
> > --- /dev/null
> > +++ b/include/rv/ltl_monitor.h
> 
> You hate macros don't you? :)

YES!

> Anyway I really like your approach, very neat.

Thank you! I'm very happy to have found a way to escape the macros.

> > +static struct ltl_monitor *ltl_get_monitor(struct task_struct *task)
> > +{
> > +	return &task->rv[ltl_monitor_slot].ltl_mon;
> > +}
> 
> This means ltl monitors only support per-task, right?

Yes.

> It shouldn't take much effort putting an ifdef chain here and defining e.g.
> PER_CPU in the header file to choose a different get_monitor.
> Or directly an ltl_monitor_implicit.h

Yes, either can work.

> I think this patch is ready without it, just trying to brainstorm how we could
> potentially extend this.
> 
> I need more time to play with these, but it looks promising.

Thank you,
Nam