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;
MIME-Version: 1.0
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> <YNBqTVFpvpXUbG4z@elver.google.com>
In-Reply-To: <YNBqTVFpvpXUbG4z@elver.google.com>
From:   Dmitry Vyukov <dvyukov@google.com>
Date:   Tue, 22 Jun 2021 07:17:13 +0200
Message-ID: <CACT4Y+ZJvcYpiCUO6ioaz3ieQKU=X8NBCQLsFpQqEGosJfW9zw@mail.gmail.com>
Subject: Re: Functional Coverage via RV? (was: "Learning-based Controlled
 Concurrency Testing")
To:     Marco Elver <elver@google.com>
Cc:     Daniel Bristot de Oliveira <bristot@redhat.com>,
        "Paul E. McKenney" <paulmck@kernel.org>,
        syzkaller <syzkaller@googlegroups.com>,
        kasan-dev <kasan-dev@googlegroups.com>,
        LKML <linux-kernel@vger.kernel.org>
Content-Type: text/plain; charset="UTF-8"
Precedence: bulk

On Mon, Jun 21, 2021 at 12:30 PM Marco Elver <elver@google.com> 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.
>
> > 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.

If we do this, we need to watch out for compiler optimizations. In
both clang and gcc KCOV pass runs in the middle of the middle-end
after some optimizations. It's possible that some trivial branches are
merged back into unconditional code already (e.g. table/conditional
moves).


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