tools/testing/selftests/rcutorture/formal/srcu-cbmc/src/simple_sync_srcu.c

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