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 
__alloc_percpu(size_t size,size_t align)17 static inline void *__alloc_percpu(size_t size, size_t align)
18 {
19 	BUG();
20 	return NULL;
21 }
22 
free_percpu(void * ptr)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
94