1 // SPDX-License-Identifier: GPL-2.0
9 /* Support NR_CPUS of at most 64 */
10 #define CPU_PREEMPTION_LOCKS_INIT0 LOCK_IMPL_INITIALIZER
11 #define CPU_PREEMPTION_LOCKS_INIT1 \
12 CPU_PREEMPTION_LOCKS_INIT0, CPU_PREEMPTION_LOCKS_INIT0
13 #define CPU_PREEMPTION_LOCKS_INIT2 \
14 CPU_PREEMPTION_LOCKS_INIT1, CPU_PREEMPTION_LOCKS_INIT1
15 #define CPU_PREEMPTION_LOCKS_INIT3 \
16 CPU_PREEMPTION_LOCKS_INIT2, CPU_PREEMPTION_LOCKS_INIT2
17 #define CPU_PREEMPTION_LOCKS_INIT4 \
18 CPU_PREEMPTION_LOCKS_INIT3, CPU_PREEMPTION_LOCKS_INIT3
19 #define CPU_PREEMPTION_LOCKS_INIT5 \
20 CPU_PREEMPTION_LOCKS_INIT4, CPU_PREEMPTION_LOCKS_INIT4
23 * Simulate disabling preemption by locking a particular cpu. NR_CPUS
24 * should be the actual number of cpus, not just the maximum.
26 struct lock_impl cpu_preemption_locks[NR_CPUS] = {
27 CPU_PREEMPTION_LOCKS_INIT0
29 , CPU_PREEMPTION_LOCKS_INIT0
32 , CPU_PREEMPTION_LOCKS_INIT1
35 , CPU_PREEMPTION_LOCKS_INIT2
38 , CPU_PREEMPTION_LOCKS_INIT3
40 #if (NR_CPUS - 1) & 16
41 , CPU_PREEMPTION_LOCKS_INIT4
43 #if (NR_CPUS - 1) & 32
44 , CPU_PREEMPTION_LOCKS_INIT5
48 #undef CPU_PREEMPTION_LOCKS_INIT0
49 #undef CPU_PREEMPTION_LOCKS_INIT1
50 #undef CPU_PREEMPTION_LOCKS_INIT2
51 #undef CPU_PREEMPTION_LOCKS_INIT3
52 #undef CPU_PREEMPTION_LOCKS_INIT4
53 #undef CPU_PREEMPTION_LOCKS_INIT5
55 __thread int thread_cpu_id;
56 __thread int preempt_disable_count;
58 void preempt_disable(void)
60 BUG_ON(preempt_disable_count < 0 || preempt_disable_count == INT_MAX);
62 if (preempt_disable_count++)
65 thread_cpu_id = nondet_int();
66 assume(thread_cpu_id >= 0);
67 assume(thread_cpu_id < NR_CPUS);
68 lock_impl_lock(&cpu_preemption_locks[thread_cpu_id]);
71 void preempt_enable(void)
73 BUG_ON(preempt_disable_count < 1);
75 if (--preempt_disable_count)
78 lock_impl_unlock(&cpu_preemption_locks[thread_cpu_id]);