tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h

   1 #ifndef PERCPU_H
   2 #define PERCPU_H
   3
   4 #include <stddef.h>
   5 #include "bug_on.h"
   6 #include "preempt.h"
   7
   8 #define __percpu
   9
  10 /* Maximum size of any percpu data. */
  11 #define PERCPU_OFFSET (4 * sizeof(long))
  12
  13 /* Ignore alignment, as CBMC doesn't care about false sharing. */
  14 #define alloc_percpu(type) __alloc_percpu(sizeof(type), 1)
  15
  16 static inline void *__alloc_percpu(size_t size, size_t align)
  17 {
  18         BUG();
  19         return NULL;
  20 }
  21
  22 static inline void free_percpu(void *ptr)
  23 {
  24         BUG();
  25 }
  26
  27 #define per_cpu_ptr(ptr, cpu) \
  28         ((typeof(ptr)) ((char *) (ptr) + PERCPU_OFFSET * cpu))
  29
  30 #define __this_cpu_inc(pcp) __this_cpu_add(pcp, 1)
  31 #define __this_cpu_dec(pcp) __this_cpu_sub(pcp, 1)
  32 #define __this_cpu_sub(pcp, n) __this_cpu_add(pcp, -(typeof(pcp)) (n))
  33
  34 #define this_cpu_inc(pcp) this_cpu_add(pcp, 1)
  35 #define this_cpu_dec(pcp) this_cpu_sub(pcp, 1)
  36 #define this_cpu_sub(pcp, n) this_cpu_add(pcp, -(typeof(pcp)) (n))
  37
  38 /* Make CBMC use atomics to work around bug. */
  39 #ifdef RUN
  40 #define THIS_CPU_ADD_HELPER(ptr, x) (*(ptr) += (x))
  41 #else
  42 /*
  43  * Split the atomic into a read and a write so that it has the least
  44  * possible ordering.
  45  */
  46 #define THIS_CPU_ADD_HELPER(ptr, x) \
  47         do { \
  48                 typeof(ptr) this_cpu_add_helper_ptr = (ptr); \
  49                 typeof(ptr) this_cpu_add_helper_x = (x); \
  50                 typeof(*ptr) this_cpu_add_helper_temp; \
  51                 __CPROVER_atomic_begin(); \
  52                 this_cpu_add_helper_temp = *(this_cpu_add_helper_ptr); \
  53                 __CPROVER_atomic_end(); \
  54                 this_cpu_add_helper_temp += this_cpu_add_helper_x; \
  55                 __CPROVER_atomic_begin(); \
  56                 *(this_cpu_add_helper_ptr) = this_cpu_add_helper_temp; \
  57                 __CPROVER_atomic_end(); \
  58         } while (0)
  59 #endif
  60
  61 /*
  62  * For some reason CBMC needs an atomic operation even though this is percpu
  63  * data.
  64  */
  65 #define __this_cpu_add(pcp, n) \
  66         do { \
  67                 BUG_ON(preemptible()); \
  68                 THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), thread_cpu_id), \
  69                                     (typeof(pcp)) (n)); \
  70         } while (0)
  71
  72 #define this_cpu_add(pcp, n) \
  73         do { \
  74                 int this_cpu_add_impl_cpu = get_cpu(); \
  75                 THIS_CPU_ADD_HELPER(per_cpu_ptr(&(pcp), this_cpu_add_impl_cpu), \
  76                                     (typeof(pcp)) (n)); \
  77                 put_cpu(); \
  78         } while (0)
  79
  80 /*
  81  * This will cause a compiler warning because of the cast from char[][] to
  82  * type*. This will cause a compile time error if type is too big.
  83  */
  84 #define DEFINE_PER_CPU(type, name) \
  85         char name[NR_CPUS][PERCPU_OFFSET]; \
  86         typedef char percpu_too_big_##name \
  87                 [sizeof(type) > PERCPU_OFFSET ? -1 : 1]
  88
  89 #define for_each_possible_cpu(cpu) \
  90         for ((cpu) = 0; (cpu) < NR_CPUS; ++(cpu))
  91
  92 #endif