LXR linux/tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync

   1// SPDX-License-Identifier: GPL-2.0
   2#include <config.h>
   3
   4#include <assert.h>
   5#include <errno.h>
   6#include <inttypes.h>
   7#include <pthread.h>
   8#include <stddef.h>
   9#include <string.h>
  10#include <sys/types.h>
  11
  12#include "int_typedefs.h"
  13
  14#include "barriers.h"
  15#include "bug_on.h"
  16#include "locks.h"
  17#include "misc.h"
  18#include "preempt.h"
  19#include "percpu.h"
  20#include "workqueues.h"
  21
  22#include <linux/srcu.h>
  23
  24/* Functions needed from modify_srcu.c */
  25bool try_check_zero(struct srcu_struct *sp, int idx, int trycount);
  26void srcu_flip(struct srcu_struct *sp);
  27
  28/* Simpler implementation of synchronize_srcu that ignores batching. */
  29void synchronize_srcu(struct srcu_struct *sp)
  30{
  31        int idx;
  32        /*
  33         * This code assumes that try_check_zero will succeed anyway,
  34         * so there is no point in multiple tries.
  35         */
  36        const int trycount = 1;
  37
  38        might_sleep();
  39
  40        /* Ignore the lock, as multiple writers aren't working yet anyway. */
  41
  42        idx = 1 ^ (sp->completed & 1);
  43
  44        /* For comments see srcu_advance_batches. */
  45
  46        assume(try_check_zero(sp, idx, trycount));
  47
  48        srcu_flip(sp);
  49
  50        assume(try_check_zero(sp, idx^1, trycount));
  51}
  52