Re: [PATCH V4 00/20] The Runtime Verification (RV) interface

[Daniel Bristot de Oliveira]

On 6/22/22 09:24, Song Liu wrote:
> This is interesting work!
> 
> I applied the series on top of commit 78ca55889a549a9a194c6ec666836329b774ab6d
> in upstream. Then, I got some compile/link error for CONFIG_RV_MON_WIP and
> CONFIG_RV_MON_SAFE_WTD. I was able to compile the kernel with these two
> configs disabled.

I rebased the code and... it compiled. Maybe it was missing some
config options that I forgot to set as "depends on" in the Kconfig.

Can you check if it was the same problem automatically reported?

Any further information here would help. I will revisit this.

However, I hit the some issue with monitors/wwnr/enabled :
> 
>     [root@eth50-1 ~]# cd /sys/kernel/debug/tracing/rv/
>     [root@eth50-1 rv]# cat available_monitors
>     wwnr
>     [root@eth50-1 rv]# echo wwnr > enabled_monitors
>     [root@eth50-1 rv]# cd monitors/
>     [root@eth50-1 monitors]# cd wwnr/
>     [root@eth50-1 wwnr]# ls
>     desc  enable  reactors
>     [root@eth50-1 wwnr]# cat enable
>     1
>     [root@eth50-1 wwnr]# echo 0 > enable   <<< hangs
> 
> The last echo command hangs forever on a qemu vm. I haven't figured out why
> this happens though.

I could reproduce it. It is an error in the return code of monitor_enable_write_data(),
I fixed it locally (return retval ? retval : count; // needs more test), and
will add it to the next version. Thanks!

> I also have a more general question: can we do RV with BPF and simplify the
> work? AFAICT, the idea of RV is to maintain a state machine based on events.
> If something unexpected happens, call the reactor.
> 
> IIUC, BPF has most of these building blocks ready for use. With BPF, we
> can ship many RV monitors without much kernel changes.

I am aware of bpftrace and bpf + libbpf, and I have a PoC tool doing most of the
work I do in C/kernel in C/bpf.

>From the cover letter:

"Things kept for a second moment (after this patchset):
[...]
	- dot2bpf"

The point is that there are use-cases in which the users need the code in 
C. One of those is the work being done in the Linux Foundation Elisa group.
There will be more formalism, like timed automata... which will require
infra-structure that is easily accessible in C... including synchronization,
and reactors that are available only in C on "per use-cases" basis - for
example on embedded devices.

On the other hand, there is ongoing research on asynchronous RV in which
I am only using BPF on the instrumentation side, for more complex formalism
running the processing in user-space (but for a different use-case,
with different timing and logical properties).

I see C and BPF (and rust?...) as complementary tools that I can use, and
we will have them all :-).

In this first series, I am adding the DA monitor in the kernel (motivated
by Elisa), and the basic kernel interface. After that, I will add the dot2bpf
for the cases in which BPF is a viable option... other formalism... other
extensions from Elisa... and so on... collecting these methods in a single
place.

-- Daniel

> Thanks,
> Song