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

[Boqun Feng <boqun.feng@gmail.com>]

Hi Marco,

On Mon, Mar 09, 2020 at 12:04:05PM -0700, paulmck@kernel.org wrote:
> From: Marco Elver <elver@google.com>
> 
> 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@google.com>
> Suggested-by: Paul E. McKenney <paulmck@kernel.org>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
> ---
>  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
>