Re: [PATCH kcsan 17/32] kcsan: Introduce ASSERT_EXCLUSIVE_* macros

From: Boqun Feng
Date: Fri Mar 13 2020 - 04:52:28 EST


Hi Marco,

On Mon, Mar 09, 2020 at 12:04:05PM -0700, paulmck@xxxxxxxxxx wrote:
> From: Marco Elver <elver@xxxxxxxxxx>
>
> Introduces ASSERT_EXCLUSIVE_WRITER and ASSERT_EXCLUSIVE_ACCESS, which
> may be used to assert properties of synchronization logic, where
> violation cannot be detected as a normal data race.
>
> Examples of the reports that may be generated:
>
> ==================================================================
> BUG: KCSAN: assert: race in test_thread / test_thread
>
> write to 0xffffffffab3d1540 of 8 bytes by task 466 on cpu 2:
> test_thread+0x8d/0x111
> debugfs_write.cold+0x32/0x44
> ...
>
> assert no writes to 0xffffffffab3d1540 of 8 bytes by task 464 on cpu 0:
> test_thread+0xa3/0x111
> debugfs_write.cold+0x32/0x44
> ...
> ==================================================================
>
> ==================================================================
> BUG: KCSAN: assert: race in test_thread / test_thread
>
> assert no accesses to 0xffffffffab3d1540 of 8 bytes by task 465 on cpu 1:
> test_thread+0xb9/0x111
> debugfs_write.cold+0x32/0x44
> ...
>
> read to 0xffffffffab3d1540 of 8 bytes by task 464 on cpu 0:
> test_thread+0x77/0x111
> debugfs_write.cold+0x32/0x44
> ...
> ==================================================================
>
> Signed-off-by: Marco Elver <elver@xxxxxxxxxx>
> Suggested-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
> Signed-off-by: Paul E. McKenney <paulmck@xxxxxxxxxx>
> ---
> include/linux/kcsan-checks.h | 40 ++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 40 insertions(+)
>
> diff --git a/include/linux/kcsan-checks.h b/include/linux/kcsan-checks.h
> index 5dcadc2..cf69617 100644
> --- a/include/linux/kcsan-checks.h
> +++ b/include/linux/kcsan-checks.h
> @@ -96,4 +96,44 @@ static inline void kcsan_check_access(const volatile void *ptr, size_t size,
> kcsan_check_access(ptr, size, KCSAN_ACCESS_ATOMIC | KCSAN_ACCESS_WRITE)
> #endif
>
> +/**
> + * ASSERT_EXCLUSIVE_WRITER - assert no other threads are writing @var
> + *
> + * Assert that there are no other threads writing @var; other readers are
> + * allowed. This assertion can be used to specify properties of concurrent code,
> + * where violation cannot be detected as a normal data race.
> + *

I like the idea that we can assert no other writers, however I think
assertions like ASSERT_EXCLUSIVE_WRITER() are a little limited. For
example, if we have the following code:

preempt_disable();
do_sth();
raw_cpu_write(var, 1);
do_sth_else();
preempt_enable();

we can add the assert to detect another potential writer like:

preempt_disable();
do_sth();
ASSERT_EXCLUSIVE_WRITER(var);
raw_cpu_write(var, 1);
do_sth_else();
preempt_enable();

, but, if I understand how KCSAN works correctly, it only works if the
another writer happens when the ASSERT_EXCLUSIVE_WRITER(var) is called,
IOW, it can only detect another writer between do_sth() and
raw_cpu_write(). But our intent is to prevent other writers for the
whole preemption-off section. With this assertion introduced, people may
end up with code like:

preempt_disable();
ASSERT_EXCLUSIVE_WRITER(var);
do_sth();
ASSERT_EXCLUSIVE_WRITER(var);
raw_cpu_write(var, 1);
ASSERT_EXCLUSIVE_WRITER(var);
do_sth_else();
ASSERT_EXCLUSIVE_WRITER(var);
preempt_enable();

and that is horrible...

So how about making a pair of annotations
ASSERT_EXCLUSIVE_WRITER_BEGIN() and ASSERT_EXCLUSIVE_WRITER_END(), so
that we can write code like:

preempt_disable();
ASSERT_EXCLUSIVE_WRITER_BEGIN(var);
do_sth();
raw_cpu_write(var, 1);
do_sth_else();
ASSERT_EXCLUSIVE_WRITER_END(var);
preempt_enable();

ASSERT_EXCLUSIVE_WRITER_BEGIN() could be a rough version of watchpoint
setting up and ASSERT_EXCLUSIVE_WRITER_END() could be watchpoint
removing. So I think it's feasible.

Thoughts?

Regards,
Boqun

> + * For example, if a per-CPU variable is only meant to be written by a single
> + * CPU, but may be read from other CPUs; in this case, reads and writes must be
> + * marked properly, however, if an off-CPU WRITE_ONCE() races with the owning
> + * CPU's WRITE_ONCE(), would not constitute a data race but could be a harmful
> + * race condition. Using this macro allows specifying this property in the code
> + * and catch such bugs.
> + *
> + * @var variable to assert on
> + */
> +#define ASSERT_EXCLUSIVE_WRITER(var) \
> + __kcsan_check_access(&(var), sizeof(var), KCSAN_ACCESS_ASSERT)
> +
> +/**
> + * ASSERT_EXCLUSIVE_ACCESS - assert no other threads are accessing @var
> + *
> + * Assert that no other thread is accessing @var (no readers nor writers). This
> + * assertion can be used to specify properties of concurrent code, where
> + * violation cannot be detected as a normal data race.
> + *
> + * For example, in a reference-counting algorithm where exclusive access is
> + * expected after the refcount reaches 0. We can check that this property
> + * actually holds as follows:
> + *
> + * if (refcount_dec_and_test(&obj->refcnt)) {
> + * ASSERT_EXCLUSIVE_ACCESS(*obj);
> + * safely_dispose_of(obj);
> + * }
> + *
> + * @var variable to assert on
> + */
> +#define ASSERT_EXCLUSIVE_ACCESS(var) \
> + __kcsan_check_access(&(var), sizeof(var), KCSAN_ACCESS_WRITE | KCSAN_ACCESS_ASSERT)
> +
> #endif /* _LINUX_KCSAN_CHECKS_H */
> --
> 2.9.5
>