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

DEFINITIONS

1. synchronize_srcu

   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 */
  25 bool try_check_zero(struct srcu_struct *sp, int idx, int trycount);
  26 void srcu_flip(struct srcu_struct *sp);
  27 
  28 /* Simpler implementation of synchronize_srcu that ignores batching. */
  29 void 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 }