Messages in this thread | | | Subject | Re: Functional Coverage via RV? (was: "Learning-based Controlled Concurrency Testing") | From | Daniel Bristot de Oliveira <> | Date | Mon, 21 Jun 2021 21:25:49 +0200 |
| |
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 >
| |