Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 23.128.96.18 as permitted sender) client-ip=23.128.96.18;
Date:   Mon, 21 Jun 2021 12:30:37 +0200
From:   Marco Elver <elver@google.com>
To:     Daniel Bristot de Oliveira <bristot@redhat.com>
Cc:     "Paul E. McKenney" <paulmck@kernel.org>,
        Dmitry Vyukov <dvyukov@google.com>,
        syzkaller <syzkaller@googlegroups.com>,
        kasan-dev <kasan-dev@googlegroups.com>,
        LKML <linux-kernel@vger.kernel.org>
Subject: Re: Functional Coverage via RV? (was: "Learning-based Controlled
 Concurrency Testing")
Message-ID: <YNBqTVFpvpXUbG4z@elver.google.com>
References: <20210517164411.GH4441@paulmck-ThinkPad-P17-Gen-1>
 <CANpmjNPbXmm9jQcquyrNGv4M4+KW_DgcrXHsgDtH=tYQ6=RU4Q@mail.gmail.com>
 <20210518204226.GR4441@paulmck-ThinkPad-P17-Gen-1>
 <CANpmjNN+nS1CAz=0vVdJLAr_N+zZxqp3nm5cxCCiP-SAx3uSyA@mail.gmail.com>
 <20210519185305.GC4441@paulmck-ThinkPad-P17-Gen-1>
 <CANpmjNMskihABCyNo=cK5c0vbNBP=fcUO5-ZqBJCiO4XGM47DA@mail.gmail.com>
 <CANpmjNMPvAucMQoZeLQAP_WiwiLT6XBoss=EZ4xAbrHnMwdt5g@mail.gmail.com>
 <c179dc74-662d-567f-0285-fcfce6adf0a5@redhat.com>
 <YMyC/Dy7XoxTeIWb@elver.google.com>
 <35852e24-9b19-a442-694c-42eb4b5a4387@redhat.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <35852e24-9b19-a442-694c-42eb4b5a4387@redhat.com>
User-Agent: Mutt/2.0.5 (2021-01-21)
Precedence: bulk

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.

> 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".
 
> 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.

> > 
> > 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.
 
> > 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