8 /* Support NR_CPUS of at most 64 */
9 #define CPU_PREEMPTION_LOCKS_INIT0 LOCK_IMPL_INITIALIZER
10 #define CPU_PREEMPTION_LOCKS_INIT1 \
11 CPU_PREEMPTION_LOCKS_INIT0, CPU_PREEMPTION_LOCKS_INIT0
12 #define CPU_PREEMPTION_LOCKS_INIT2 \
13 CPU_PREEMPTION_LOCKS_INIT1, CPU_PREEMPTION_LOCKS_INIT1
14 #define CPU_PREEMPTION_LOCKS_INIT3 \
15 CPU_PREEMPTION_LOCKS_INIT2, CPU_PREEMPTION_LOCKS_INIT2
16 #define CPU_PREEMPTION_LOCKS_INIT4 \
17 CPU_PREEMPTION_LOCKS_INIT3, CPU_PREEMPTION_LOCKS_INIT3
18 #define CPU_PREEMPTION_LOCKS_INIT5 \
19 CPU_PREEMPTION_LOCKS_INIT4, CPU_PREEMPTION_LOCKS_INIT4
22 * Simulate disabling preemption by locking a particular cpu. NR_CPUS
23 * should be the actual number of cpus, not just the maximum.
25 struct lock_impl cpu_preemption_locks[NR_CPUS] = {
26 CPU_PREEMPTION_LOCKS_INIT0
28 , CPU_PREEMPTION_LOCKS_INIT0
31 , CPU_PREEMPTION_LOCKS_INIT1
34 , CPU_PREEMPTION_LOCKS_INIT2
37 , CPU_PREEMPTION_LOCKS_INIT3
39 #if (NR_CPUS - 1) & 16
40 , CPU_PREEMPTION_LOCKS_INIT4
42 #if (NR_CPUS - 1) & 32
43 , CPU_PREEMPTION_LOCKS_INIT5
47 #undef CPU_PREEMPTION_LOCKS_INIT0
48 #undef CPU_PREEMPTION_LOCKS_INIT1
49 #undef CPU_PREEMPTION_LOCKS_INIT2
50 #undef CPU_PREEMPTION_LOCKS_INIT3
51 #undef CPU_PREEMPTION_LOCKS_INIT4
52 #undef CPU_PREEMPTION_LOCKS_INIT5
54 __thread int thread_cpu_id;
55 __thread int preempt_disable_count;
57 void preempt_disable(void)
59 BUG_ON(preempt_disable_count < 0 || preempt_disable_count == INT_MAX);
61 if (preempt_disable_count++)
64 thread_cpu_id = nondet_int();
65 assume(thread_cpu_id >= 0);
66 assume(thread_cpu_id < NR_CPUS);
67 lock_impl_lock(&cpu_preemption_locks[thread_cpu_id]);
70 void preempt_enable(void)
72 BUG_ON(preempt_disable_count < 1);
74 if (--preempt_disable_count)
77 lock_impl_unlock(&cpu_preemption_locks[thread_cpu_id]);