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

INCLUDED FROM

DEFINITIONS

1. __alloc_percpu
2. free_percpu

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