Re: Functional Coverage via RV? (was: "Learning-based Controlled Concurrency Testing")

[Daniel Bristot de Oliveira]

On 6/21/21 12:30 PM, Marco Elver wrote:
> On Mon, Jun 21, 2021 at 10:23AM +0200, Daniel Bristot de Oliveira wrote:
> [...]
>>> Yes, unlike code/structural coverage (which is what we have today via
>>> KCOV) functional coverage checks if some interesting states were reached
>>> (e.g. was buffer full/empty, did we observe transition a->b etc.).
>>
>> So you want to observe a given a->b transition, not that B was visited?
> 
> An a->b transition would imply that a and b were visited.

HA! let's try again with a less abstract example...


  |   +------------ on --+----------------+
  v   ^                  +--------v       v
+========+               |        +===========+>--- suspend ---->+===========+
|  OFF   |               +- on --<|     ON    |                  | SUSPENDED |
+========+ <------ shutdown -----<+===========+<----- on -------<+===========+
    ^                                    v                             v
    +--------------- off ----------------+-----------------------------+

Do you care about:

1) states [OFF|ON|SUSPENDED] being visited a # of times; or
2) the occurrence of the [on|suspend|off] events a # of times; or
3) the language generated by the "state machine"; like:

   the occurrence of *"on -> suspend -> on -> off"*

         which is != of

   the occurrence of *"on -> on -> suspend -> off"*

         although the same events and states occurred the same # of times
?

RV can give you all... but the way to inform this might be different.

>> I still need to understand what you are aiming to verify, and what is the
>> approach that you would like to use to express the specifications of the systems...
>>
>> Can you give me a simple example?
> 
> The older discussion started around a discussion how to get the fuzzer
> into more interesting states in complex concurrent algorithms. But
> otherwise I have no idea ... we were just brainstorming and got to the
> point where it looked like "functional coverage" would improve automated
> test generation in general. And then I found RV which pretty much can
> specify "functional coverage" and almost gets that information to KCOV
> "for free".

I think we will end up having an almost for free solution, but worth the price.

>> so, you want to have a different function for every transition so KCOV can
>> observe that?
> 
> Not a different function, just distinct "basic blocks". KCOV uses
> compiler instrumentation, and a sequence of non-branching instructions
> denote one point of coverage; at the next branch (conditional or otherwise)
> it then records which branch was taken and therefore we know which code
> paths were covered.

ah, got it. But can't KCOV be extended with another source of information?

>>>
>>> From what I can tell this doesn't quite happen today, because
>>> automaton::function is a lookup table as an array.
>>
>> It is a the transition function of the formal automaton definition. Check this:
>>
>> https://bristot.me/wp-content/uploads/2020/01/JSA_preprint.pdf
>>
>> page 9.
>>
>> Could this just
>>> become a generated function with a switch statement? Because then I
>>> think we'd pretty much have all the ingredients we need.
>>
>> a switch statement that would.... call a different function for each transition?
> 
> No, just a switch statement that returns the same thing as it does
> today. But KCOV wouldn't see different different coverage with the
> current version because it's all in one basic block because it looks up
> the next state given the current state out of the array. If it was a
> switch statement doing the same thing, the compiler will turn the thing
> into conditional branches and KCOV then knows which code path
> (effectively the transition) was covered.

[ the answer for this points will depend on your answer from my first question
on this email so... I will reply it later ].

-- Daniel

>>> Then:
>>>
>>> 1. Create RV models for states of interests not covered by normal code
>>>    coverage of code under test.
>>>
>>> 2. Enable KCOV for everything.
>>>
>>> 3. KCOV's coverage of the RV model will tell us if we reached the
>>>    desired "functional coverage" (and can be used by e.g. syzbot to
>>>    generate better tests without any additional changes because it
>>>    already talks to KCOV).
>>>
>>> Thoughts?
>>>
>>> Thanks,
>>> -- Marco
>