LXR linux/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/percpu.h

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