trunk/verif/nico-md-merge/models/model_03.spin

   1 /* LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v2
   2  * Created for the Spin validator.
   3  * Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
   4  * October 2008
   5
   6  * TODO : create test cases that will generate an overflow on the offset and
   7  * counter type. Counter types smaller than a byte should be used.
   8
   9  * Promela only has unsigned char, no signed char.
  10  * Because detection of difference < 0 depends on a signed type, but we want
  11  * compactness, check also for the values being higher than half of the unsigned
  12  * char range (and consider them negative). The model, by design, does not use
  13  * offsets or counts higher than 127 because we would then have to use a larger
  14  * type (short or int).
  15  */
  16 #define HALF_UCHAR (255/2)
  17
  18 /* NUMPROCS 4 : causes event loss with some reader timings.
  19  * e.g. 3 events, 1 switch, 1 event (lost, buffer full), read 1 subbuffer
  20  */
  21 #define NUMPROCS 4
  22
  23 /* NUMPROCS 3 : does not cause event loss because buffers are big enough.
  24  * #define NUMPROCS 3
  25  * e.g. 3 events, 1 switch, read 1 subbuffer
  26  */
  27
  28 #define NUMSWITCH 1
  29 #ifndef BUFSIZE
  30 #define BUFSIZE 4
  31 #endif
  32 #define NR_SUBBUFS 2
  33 #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
  34
  35 /* Writer counters
  36 */
  37 byte write_off = 0;
  38 byte commit_count[NR_SUBBUFS];
  39
  40 /* <formal_verif> */
  41 byte _commit_sum;
  42 /* </formal_verif> */
  43
  44 /* Reader counters
  45 */
  46 byte read_off = 0;
  47
  48 byte events_lost = 0;
  49 byte refcount = 0;
  50
  51 bool deliver = 0;
  52
  53 //#ifdef RACE_TEST
  54 /* buffer slot in-use bit. Detects racy use (more than a single process
  55  * accessing a slot at any given step).
  56  */
  57 bool buffer_use[BUFSIZE];
  58 //#endif
  59
  60 /* Proceed to a sub-subber switch is needed.
  61  * Used in a periodical timer interrupt to fill and ship the current subbuffer
  62  * to the reader so we can guarantee a steady flow. If a subbuffer is
  63  * completely empty, do not switch.
  64  * Also used as "finalize" operation to complete the last subbuffer after
  65  * all writers have finished so the last subbuffer can be read by the reader.
  66  */
  67 proctype switcher()
  68 {
  69   byte prev_off, new_off, tmp_commit;
  70   byte size;
  71
  72 cmpxchg_loop:
  73   atomic {
  74     prev_off = write_off;
  75     size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
  76     new_off = prev_off + size;
  77     if
  78       :: (new_off - read_off > BUFSIZE && new_off - read_off < HALF_UCHAR)
  79          || size == SUBBUF_SIZE ->
  80          refcount = refcount - 1;
  81          goto not_needed;
  82       :: else -> skip
  83     fi;
  84   }
  85   atomic {
  86     if
  87       :: prev_off != write_off -> goto cmpxchg_loop
  88       :: else -> write_off = new_off;
  89     fi;
  90   }
  91
  92   atomic {
  93     tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
  94     /* <formal_verif> */
  95     _commit_sum = _commit_sum - commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE]
  96                   + tmp_commit;
  97     /* </formal_verif> */
  98     commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
  99     if
 100       :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE -
 101          tmp_commit
 102          -> deliver = 1
 103       :: else
 104          -> skip
 105     fi;
 106     refcount = refcount - 1;
 107   }
 108 not_needed:
 109   skip;
 110 }
 111
 112 /* tracer
 113  * Writes 1 byte of information in the buffer at the current
 114  * "write_off" position and then increment the commit_count of the sub-buffer
 115  * the information has been written to.
 116  */
 117 proctype tracer()
 118 {
 119   byte size = 1;
 120   byte prev_off, new_off, tmp_commit;
 121   byte i, j;
 122
 123 cmpxchg_loop:
 124   atomic {
 125     prev_off = write_off;
 126     new_off = prev_off + size;
 127   }
 128   atomic {
 129     if
 130       :: new_off - read_off > BUFSIZE && new_off - read_off < HALF_UCHAR ->
 131          goto lost
 132       :: else -> skip
 133     fi;
 134   }
 135   atomic {
 136     if
 137       :: prev_off != write_off -> goto cmpxchg_loop
 138       :: else -> write_off = new_off;
 139     fi;
 140     i = 0;
 141     do
 142       :: i < size ->
 143          assert(buffer_use[(prev_off + i) % BUFSIZE] == 0);
 144          buffer_use[(prev_off + i) % BUFSIZE] = 1;
 145          i++
 146       :: i >= size -> break
 147     od;
 148   }
 149
 150   /* writing to buffer...
 151   */
 152
 153   atomic {
 154     i = 0;
 155     do
 156       :: i < size ->
 157          buffer_use[(prev_off + i) % BUFSIZE] = 0;
 158          i++
 159       :: i >= size -> break
 160     od;
 161     tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
 162     /* <formal_verif> */
 163     _commit_sum = _commit_sum - commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE]
 164                   + tmp_commit;
 165     /* </formal_verif> */
 166     commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
 167     if
 168       :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE -
 169          tmp_commit
 170          -> deliver = 1
 171       :: else
 172          -> skip
 173     fi;
 174   }
 175   atomic {
 176     goto end;
 177 lost:
 178     events_lost++;
 179 end:
 180     refcount = refcount - 1;
 181   }
 182 }
 183
 184 /* reader
 185  * Read the information sub-buffer per sub-buffer when available.
 186  *
 187  * Reads the information as soon as it is ready, or may be delayed by
 188  * an asynchronous delivery. Being modeled as a process insures all cases
 189  * (scheduled very quickly or very late, causing event loss) are covered.
 190  * Only one reader per buffer (normally ensured by a mutex). This is modeled
 191  * by using a single reader process.
 192  */
 193 proctype reader()
 194 {
 195   byte i, j;
 196
 197   do
 198     :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0
 199        && (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) < HALF_UCHAR
 200        && (commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE]
 201            - SUBBUF_SIZE - (((read_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS)
 202            == 0) ->
 203        atomic {
 204          i = 0;
 205          do
 206            :: i < SUBBUF_SIZE ->
 207               assert(buffer_use[(read_off + i) % BUFSIZE] == 0);
 208               buffer_use[(read_off + i) % BUFSIZE] = 1;
 209               i++
 210            :: i >= SUBBUF_SIZE -> break
 211          od;
 212        }
 213
 214        /* reading from buffer...
 215        */
 216
 217        atomic {
 218          i = 0;
 219          do
 220            :: i < SUBBUF_SIZE ->
 221               buffer_use[(read_off + i) % BUFSIZE] = 0;
 222               i++
 223            :: i >= SUBBUF_SIZE -> break
 224          od;
 225          read_off = read_off + SUBBUF_SIZE;
 226        }
 227     :: read_off >= (NUMPROCS - events_lost) -> break;
 228   od;
 229 }
 230
 231 /* Waits for all tracer and switcher processes to finish before finalizing
 232  * the buffer. Only after that will the reader be allowed to read the
 233  * last subbuffer.
 234  */
 235 proctype cleaner()
 236 {
 237   atomic {
 238     do
 239       :: refcount == 0 ->
 240          refcount = refcount + 1;
 241          run switcher();  /* Finalize the last sub-buffer so it can be read. */
 242          break;
 243     od;
 244   }
 245 }
 246
 247 init {
 248   byte i = 0;
 249   byte j = 0;
 250   byte sum = 0;
 251   byte commit_sum = 0;
 252
 253   atomic {
 254     i = 0;
 255     do
 256       :: i < NR_SUBBUFS ->
 257          commit_count[i] = 0;
 258          i++
 259       :: i >= NR_SUBBUFS -> break
 260     od;
 261     /* <formal_verif> */
 262     _commit_sum = 0;
 263     /* </formal_verif> */
 264     i = 0;
 265     do
 266       :: i < BUFSIZE ->
 267          buffer_use[i] = 0;
 268          i++
 269       :: i >= BUFSIZE -> break
 270     od;
 271     run reader();
 272     run cleaner();
 273     i = 0;
 274     do
 275       :: i < NUMPROCS ->
 276          refcount = refcount + 1;
 277          run tracer();
 278          i++
 279       :: i >= NUMPROCS -> break
 280     od;
 281     i = 0;
 282     do
 283       :: i < NUMSWITCH ->
 284          refcount = refcount + 1;
 285          run switcher();
 286          i++
 287       :: i >= NUMSWITCH -> break
 288     od;
 289   }
 290 }
 291