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 93
