diff options
Diffstat (limited to '')
-rw-r--r-- | tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h | 93 |
1 files changed, 93 insertions, 0 deletions
diff --git a/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h new file mode 100644 index 000000000..27e67a3f2 --- /dev/null +++ b/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h @@ -0,0 +1,93 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +#ifndef PERCPU_H +#define PERCPU_H + +#include <stddef.h> +#include "bug_on.h" +#include "preempt.h" + +#define __percpu + +/* Maximum size of any percpu data. */ +#define PERCPU_OFFSET (4 * sizeof(long)) + +/* Ignore alignment, as CBMC doesn't care about false sharing. */ +#define alloc_percpu(type) __alloc_percpu(sizeof(type), 1) + +static inline void *__alloc_percpu(size_t size, size_t align) +{ + BUG(); + return NULL; +} + +static inline void free_percpu(void *ptr) +{ + BUG(); +} + +#define per_cpu_ptr(ptr, cpu) \ + ((typeof(ptr)) ((char *) (ptr) + PERCPU_OFFSET * cpu)) + +#define __this_cpu_inc(pcp) __this_cpu_add(pcp, 1) +#define __this_cpu_dec(pcp) __this_cpu_sub(pcp, 1) +#define __this_cpu_sub(pcp, n) __this_cpu_add(pcp, -(typeof(pcp)) (n)) + +#define this_cpu_inc(pcp) this_cpu_add(pcp, 1) +#define this_cpu_dec(pcp) this_cpu_sub(pcp, 1) +#define this_cpu_sub(pcp, n) this_cpu_add(pcp, -(typeof(pcp)) (n)) + +/* Make CBMC use atomics to work around bug. */ +#ifdef RUN +#define THIS_CPU_ADD_HELPER(ptr, x) (*(ptr) += (x)) +#else +/* + * Split the atomic into a read and a write so that it has the least + * possible ordering. + */ +#define THIS_CPU_ADD_HELPER(ptr, x) \ + do { \ + typeof(ptr) this_cpu_add_helper_ptr = (ptr); \ + typeof(ptr) this_cpu_add_helper_x = (x); \ + typeof(*ptr) this_cpu_add_helper_temp; \ + __CPROVER_atomic_begin(); \ + this_cpu_add_helper_temp = *(this_cpu_add_helper_ptr); \ + __CPROVER_atomic_end(); \ + this_cpu_add_helper_temp += this_cpu_add_helper_x; \ + __CPROVER_atomic_begin(); \ + *(this_cpu_add_helper_ptr) = this_cpu_add_helper_temp; \ + __CPROVER_atomic_end(); \ + } while (0) +#endif + +/* + * For some reason CBMC needs an atomic operation even though this is percpu + * data. + */ +#define __this_cpu_add(pcp, n) \ + do { \ + BUG_ON(preemptible()); \ + THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), thread_cpu_id), \ + (typeof(pcp)) (n)); \ + } while (0) + +#define this_cpu_add(pcp, n) \ + do { \ + int this_cpu_add_impl_cpu = get_cpu(); \ + THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), this_cpu_add_impl_cpu), \ + (typeof(pcp)) (n)); \ + put_cpu(); \ + } while (0) + +/* + * This will cause a compiler warning because of the cast from char[][] to + * type*. This will cause a compile time error if type is too big. + */ +#define DEFINE_PER_CPU(type, name) \ + char name[NR_CPUS][PERCPU_OFFSET]; \ + typedef char percpu_too_big_##name \ + [sizeof(type) > PERCPU_OFFSET ? -1 : 1] + +#define for_each_possible_cpu(cpu) \ + for ((cpu) = 0; (cpu) < NR_CPUS; ++(cpu)) + +#endif |