verif/lttng/buffer.spin.missing_retrieve_count

   1 //#define NUMPROCS 5
   2 #define NUMPROCS 4
   3 #define BUFSIZE 4
   4 #define NR_SUBBUFS 2
   5 #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
   6
   7 byte write_off = 0;
   8 byte read_off = 0;
   9 byte events_lost = 0;
  10 byte deliver = 0; // Number of subbuffers delivered
  11 byte refcount = 0;
  12
  13 byte commit_count[NR_SUBBUFS];
  14
  15 byte buffer_use_count[BUFSIZE];
  16
  17 proctype switcher()
  18 {
  19   int prev_off, new_off, tmp_commit;
  20   int size;
  21
  22 cmpxchg_loop:
  23   atomic {
  24     prev_off = write_off;
  25     size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
  26     new_off = prev_off + size;
  27     if
  28     :: new_off - read_off > BUFSIZE ->
  29       goto not_needed;
  30     :: else -> skip
  31     fi;
  32   }
  33   atomic {
  34     if
  35     :: prev_off != write_off -> goto cmpxchg_loop
  36     :: else -> write_off = new_off;
  37     fi;
  38   }
  39
  40   atomic {
  41     tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
  42     commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
  43     if
  44     :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
  45     :: else -> skip
  46     fi;
  47   }
  48 not_needed:
  49   skip;
  50 }
  51
  52 proctype tracer(byte size)
  53 {
  54   int prev_off, new_off, tmp_commit;
  55   int i;
  56   int j;
  57
  58 cmpxchg_loop:
  59   atomic {
  60     prev_off = write_off;
  61     new_off = prev_off + size;
  62   }
  63   atomic {
  64     if
  65     :: new_off - read_off > BUFSIZE -> goto lost
  66     :: else -> skip
  67     fi;
  68   }
  69   atomic {
  70     if
  71     :: prev_off != write_off -> goto cmpxchg_loop
  72     :: else -> write_off = new_off;
  73     fi;
  74     i = 0;
  75     do
  76     :: i < size ->
  77       buffer_use_count[(prev_off + i) % BUFSIZE]
  78         = buffer_use_count[(prev_off + i) % BUFSIZE] + 1;
  79       i++
  80     :: i >= size -> break
  81     od;
  82   }
  83     do
  84     :: j < BUFSIZE ->
  85       assert(buffer_use_count[j] < 2);
  86       j++
  87     :: j >= BUFSIZE -> break
  88     od;
  89
  90
  91
  92   // writing to buffer...
  93
  94   atomic {
  95     i = 0;
  96     do
  97     :: i < size ->
  98       buffer_use_count[(prev_off + i) % BUFSIZE]
  99         = buffer_use_count[(prev_off + i) % BUFSIZE] - 1;
 100       i++
 101     :: i >= size -> break
 102     od;
 103     tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
 104     commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
 105     if
 106     :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
 107     :: else -> skip
 108     fi;
 109   }
 110   goto end;
 111 lost:
 112   events_lost++;
 113 end:
 114   refcount = refcount - 1;
 115 }
 116
 117 proctype reader()
 118 {
 119   int i;
 120   int j;
 121     //atomic {
 122     //  do
 123     //  :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break;
 124     //  od;
 125     //}
 126   do
 127   :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0 && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] % SUBBUF_SIZE == 0 ->
 128     atomic {
 129       i = 0;
 130       do
 131       :: i < SUBBUF_SIZE ->
 132         buffer_use_count[(read_off + i) % BUFSIZE]
 133           = buffer_use_count[(read_off + i) % BUFSIZE] + 1;
 134         i++
 135       :: i >= SUBBUF_SIZE -> break
 136       od;
 137     }
 138     j = 0;
 139     do
 140     :: j < BUFSIZE ->
 141       assert(buffer_use_count[j] < 2);
 142       j++
 143     :: j >= BUFSIZE -> break
 144     od;
 145
 146     // reading from buffer...
 147
 148     atomic {
 149       i = 0;
 150       do
 151       :: i < SUBBUF_SIZE ->
 152         buffer_use_count[(read_off + i) % BUFSIZE]
 153           = buffer_use_count[(read_off + i) % BUFSIZE] - 1;
 154         i++
 155       :: i >= SUBBUF_SIZE -> break
 156       od;
 157       read_off = read_off + SUBBUF_SIZE;
 158     }
 159   :: read_off >= (NUMPROCS - events_lost) -> break;
 160   od;
 161 }
 162
 163 proctype cleaner()
 164 {
 165   atomic {
 166     do
 167     :: refcount == 0 ->
 168       run switcher();
 169       break;
 170     od;
 171   }
 172 }
 173
 174 init {
 175   int i = 0;
 176   int j = 0;
 177   int sum = 0;
 178   int commit_sum = 0;
 179
 180   atomic {
 181     i = 0;
 182     do
 183     :: i < NR_SUBBUFS ->
 184       commit_count[i] = 0;
 185       i++
 186     :: i >= NR_SUBBUFS -> break
 187     od;
 188     i = 0;
 189     do
 190     :: i < BUFSIZE ->
 191       buffer_use_count[i] = 0;
 192       i++
 193     :: i >= BUFSIZE -> break
 194     od;
 195     run reader();
 196     run cleaner();
 197     i = 0;
 198     do
 199     :: i < NUMPROCS ->
 200       refcount = refcount + 1;
 201       run tracer(1);
 202       i++
 203     :: i >= NUMPROCS -> break
 204     od;
 205     run switcher();
 206   }
 207   atomic {
 208     assert(write_off - read_off >= 0);
 209     j = 0;
 210     commit_sum = 0;
 211     do
 212     :: j < NR_SUBBUFS ->
 213       commit_sum = commit_sum + commit_count[j];
 214       j++
 215     :: j >= NR_SUBBUFS -> break
 216     od;
 217     assert(commit_sum <= write_off);
 218     j = 0;
 219     do
 220     :: j < BUFSIZE ->
 221       assert(buffer_use_count[j] < 2);
 222       j++
 223     :: j >= BUFSIZE -> break
 224     od;
 225
 226     //assert(events_lost == 0);
 227   }
 228 }