linux/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/preempt.c
<<
>>
Prefs
   1// SPDX-License-Identifier: GPL-2.0
   2#include <config.h>
   3
   4#include "preempt.h"
   5
   6#include "assume.h"
   7#include "locks.h"
   8
   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
  21
  22/*
  23 * Simulate disabling preemption by locking a particular cpu. NR_CPUS
  24 * should be the actual number of cpus, not just the maximum.
  25 */
  26struct lock_impl cpu_preemption_locks[NR_CPUS] = {
  27        CPU_PREEMPTION_LOCKS_INIT0
  28#if (NR_CPUS - 1) & 1
  29        , CPU_PREEMPTION_LOCKS_INIT0
  30#endif
  31#if (NR_CPUS - 1) & 2
  32        , CPU_PREEMPTION_LOCKS_INIT1
  33#endif
  34#if (NR_CPUS - 1) & 4
  35        , CPU_PREEMPTION_LOCKS_INIT2
  36#endif
  37#if (NR_CPUS - 1) & 8
  38        , CPU_PREEMPTION_LOCKS_INIT3
  39#endif
  40#if (NR_CPUS - 1) & 16
  41        , CPU_PREEMPTION_LOCKS_INIT4
  42#endif
  43#if (NR_CPUS - 1) & 32
  44        , CPU_PREEMPTION_LOCKS_INIT5
  45#endif
  46};
  47
  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
  54
  55__thread int thread_cpu_id;
  56__thread int preempt_disable_count;
  57
  58void preempt_disable(void)
  59{
  60        BUG_ON(preempt_disable_count < 0 || preempt_disable_count == INT_MAX);
  61
  62        if (preempt_disable_count++)
  63                return;
  64
  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]);
  69}
  70
  71void preempt_enable(void)
  72{
  73        BUG_ON(preempt_disable_count < 1);
  74
  75        if (--preempt_disable_count)
  76                return;
  77
  78        lock_impl_unlock(&cpu_preemption_locks[thread_cpu_id]);
  79}
  80