move everything out of trunk

[lttv.git] / trunk / verif / lttng / buffer.spin.bkp1

diff --git a/trunk/verif/lttng/buffer.spin.bkp1 b/trunk/verif/lttng/buffer.spin.bkp1
deleted file mode 100644 (file)
index 8a0ad29..0000000
--- a/trunk/verif/lttng/buffer.spin.bkp1
+++ /dev/null
@@ -1,154 +0,0 @@
-//#define NUMPROCS 5
-#define NUMPROCS 4
-#define BUFSIZE 4
-#define NR_SUBBUFS 2
-#define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
-
-byte write_off = 0;
-byte read_off = 0;
-byte events_lost = 0;
-byte deliver = 0; // Number of subbuffers delivered
-byte refcount = 0;
-
-byte commit_count[NR_SUBBUFS];
-
-proctype switcher()
-{
-  int prev_off, new_off, tmp_commit;
-  int size;
-
-cmpxchg_loop:
-  atomic {
-    prev_off = write_off;
-    size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
-    new_off = prev_off + size;
-    if
-    :: new_off - read_off > BUFSIZE ->
-      goto not_needed;
-    :: else -> skip
-    fi;
-  }
-  atomic {
-    if
-    :: prev_off != write_off -> goto cmpxchg_loop
-    :: else -> write_off = new_off;
-    fi;
-  }
-
-  atomic {
-    tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
-    commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
-    if
-    :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
-    :: else -> skip
-    fi;
-  }
-not_needed:
-  skip;
-}
-
-proctype tracer(byte size)
-{
-  int prev_off, new_off, tmp_commit;
-
-cmpxchg_loop:
-  atomic {
-    prev_off = write_off;
-    new_off = prev_off + size;
-  }
-  atomic {
-    if
-    :: new_off - read_off > BUFSIZE -> goto lost
-    :: else -> skip
-    fi;
-  }
-  atomic {
-    if
-    :: prev_off != write_off -> goto cmpxchg_loop
-    :: else -> write_off = new_off;
-    fi;
-  }
-
-  atomic {
-    tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
-    commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
-    if
-    :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
-    :: else -> skip
-    fi;
-  }
-  goto end;
-lost:
-  events_lost++;
-end:
-  refcount = refcount - 1;
-}
-
-proctype reader()
-{
-    //atomic {
-    //  do
-    //  :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break;
-    //  od;
-    //}
- // made atomic to use less memory. Not really true.
- atomic {
-    do
-    :: write_off - read_off >= SUBBUF_SIZE && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] % SUBBUF_SIZE == 0 ->
-      read_off = read_off + SUBBUF_SIZE;
-    :: read_off >= (NUMPROCS - events_lost) -> break;
-    od;
-  }
-}
-
-proctype cleaner()
-{
-  atomic {
-    do
-    :: refcount == 0 ->
-      run switcher();
-      break;
-    od;
-  }
-}
-
-init {
-  int i = 0;
-  int j = 0;
-  int sum = 0;
-  int commit_sum = 0;
-
-  atomic {
-    i = 0;
-    do
-    :: i < NR_SUBBUFS ->
-      commit_count[i] = 0;
-      i++
-    :: i >= NR_SUBBUFS -> break
-    od;
-    run reader();
-    run cleaner();
-    i = 0;
-    do
-    :: i < NUMPROCS ->
-      refcount = refcount + 1;
-      run tracer(1);
-      i++
-    :: i >= NUMPROCS -> break
-    od;
-    run switcher();
-  }
-  atomic {
-    assert(write_off - read_off >= 0);
-    j = 0;
-    commit_sum = 0;
-    do
-    :: j < NR_SUBBUFS ->
-      commit_sum = commit_sum + commit_count[j];
-      j++
-    :: j >= NR_SUBBUFS -> break
-    od;
-    assert(commit_sum <= write_off);
-    //assert(events_lost == 0);
-  }
-}