Re: KTSan

[Dmitry Vyukov]

On Fri, Oct 27, 2017 at 6:49 PM, Andrea Parri <parri....@gmail.com> wrote:
> Hi Dmitry,
>
> I've been reading KTSan documentation I could find online, starting from
>
> https://github.com/google/ktsan/blob/tsan/Documentation/ktsan.txt
>
> I could not find a satisfactory description of the notion of "data race". (?)
>
> What's the (underlying) memory model?
>
> Could you provide me with a list of references?
>
> Looking forward to know more about KTSan,
>
> Andrea
>
> P. S. Speaking of memory models: The reference "Linux-Kernel Memory Model" in
>
> https://github.com/google/ktsan/wiki/READ_ONCE-and-WRITE_ONCE
>
> has been updated:
>
> http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0124r4.html
>
> The model has now its own repository (with further documentation):
>
> https://github.com/aparri/memory-model


+Paul, Andrey and ktsan mailing list

Hi Andrea,

We use the definition of data race provided by C/C++ standards.
We did a reasonable mapping of kernel synchronization primitives onto
C/C++ primitives. E.g. smp_load_acquire/smp_store_release are
translated into atomic_load(acquire)/store(release); rmb/wmb are
translated into atomic_thread_fence(acquire/release), etc. We also did
some creative mapping of rcu/seqlocks/percpu primitives, e.g. call_rcu
happens-before invocation of the callback, etc. In some cases the
mapping may be overly strong, but initially we aimed at just being
close enough without false positives.
The definitions can be changing, but I think the main idea is still
there: synchronization primitives establish HB according to some
rules; and race is unordered by HB accesses. And that's what tsan
"engine" does. Exact rules for synchronization primitives can be
easily altered later.

Hope this helps
Thanks

[Andrea Parri]

Thank you for this information. This does encourage me to dig deeper
into the code/ktsan ;) (e.g., what's a "reasonable mapping of kernel
synchronization primitives onto C/C++"? what's that "creative mapping
of RCU [...]"? and, of course, how could these become relevant for/be
used with the LKMM? Looks like I have places to start ... ;)

Thanks,
Andrea


>
> Hope this helps
> Thanks

[Dmitry Vyukov]

Some more high level info.
KTSAN is a happens-before type, vector-clock based race detector.
The vector clock core is here, see kt_sync_acquire/release:
https://github.com/google/ktsan/blob/tsan/mm/ktsan/sync.c
Then each task and synchronization primitive have an associated vector clock.
And then we have interface functions here, e.g. ktsan_percpu_acquire:
https://github.com/google/ktsan/blob/tsan/mm/ktsan/ktsan.c
But lots of sync primitive annotations use just
ktsan_sync_acquire/release, which directly translate to vector clock
operations.

I think there should be lots of synergy between MM and KTSAN effort.
Though, probably KTSAN won't be able to model some aspects of the
model (notably, data/control dependencies).

To clarify the current status. KTSAN is a working prototype for that
old version of kernel. The project is currently frozen (we have lots
of other work to do, KMSAN is the next tool we are working on right
now). But we want to revive it in some point in future.

Thanks

[Andrea Parri]

Thank you for these references.

>
> I think there should be lots of synergy between MM and KTSAN effort.
> Though, probably KTSAN won't be able to model some aspects of the
> model (notably, data/control dependencies).

Not "too bad", considered the shortcomings the LKMM currently presents in
dealing with such dependencies (c.f., e.g.,

"Faced with all these possibilities [compiler optimizations], the
LMKM basically gives up",

and the discussion in section "A WARNING" from

https://github.com/aparri/memory-model/blob/master/Documentation/explanation.txt ) ...

>
> To clarify the current status. KTSAN is a working prototype for that
> old version of kernel. The project is currently frozen (we have lots
> of other work to do, KMSAN is the next tool we are working on right
> now). But we want to revive it in some point in future.

Thanks,
Andrea


>
> Thanks