--- /dev/null
+/* LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v2
+ * Created for the Spin validator.
+ * Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
+ * October 2008
+
+ * TODO : create test cases that will generate an overflow on the offset and
+ * counter type. Counter types smaller than a byte should be used.
+
+ * Promela only has unsigned char, no signed char.
+ * Because detection of difference < 0 depends on a signed type, but we want
+ * compactness, check also for the values being higher than half of the unsigned
+ * char range (and consider them negative). The model, by design, does not use
+ * offsets or counts higher than 127 because we would then have to use a larger
+ * type (short or int).
+ */
+#define HALF_UCHAR (255/2)
+
+/* NUMPROCS 4 : causes event loss with some reader timings.
+ * e.g. 3 events, 1 switch, 1 event (lost, buffer full), read 1 subbuffer
+ */
+#define NUMPROCS 4
+
+/* NUMPROCS 3 : does not cause event loss because buffers are big enough.
+ * #define NUMPROCS 3
+ * e.g. 3 events, 1 switch, read 1 subbuffer
+ */
+
+#define NUMSWITCH 1
+#define BUFSIZE 4
+#define NR_SUBBUFS 2
+#define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
+
+/* Writer counters
+*/
+byte write_off = 0;
+byte commit_count[NR_SUBBUFS];
+
+/* Reader counters
+*/
+byte read_off = 0;
+
+byte events_lost = 0;
+byte refcount = 0;
+
+bool deliver = 0;
+
+/* buffer slot in-use bit. Detects racy use (more than a single process
+ * accessing a slot at any given step).
+ */
+bool buffer_use[BUFSIZE];
+
+/* Proceed to a sub-subber switch is needed.
+ * Used in a periodical timer interrupt to fill and ship the current subbuffer
+ * to the reader so we can guarantee a steady flow. If a subbuffer is
+ * completely empty, do not switch.
+ * Also used as "finalize" operation to complete the last subbuffer after
+ * all writers have finished so the last subbuffer can be read by the reader.
+ */
+proctype switcher()
+{
+ byte prev_off, new_off, tmp_commit;
+ byte 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 && new_off - read_off < HALF_UCHAR)
+ || size == SUBBUF_SIZE ->
+ refcount = refcount - 1;
+ 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
+ :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE -
+ tmp_commit
+ -> deliver = 1
+ :: else
+ -> skip
+ fi;
+ refcount = refcount - 1;
+ }
+not_needed:
+ skip;
+}
+
+/* tracer
+ * Writes 1 byte of information in the buffer at the current
+ * "write_off" position and then increment the commit_count of the sub-buffer
+ * the information has been written to.
+ */
+proctype tracer()
+{
+ byte size = 1;
+ byte prev_off, new_off, tmp_commit;
+ byte i, j;
+
+cmpxchg_loop:
+ atomic {
+ prev_off = write_off;
+ new_off = prev_off + size;
+ }
+ atomic {
+ if
+ :: new_off - read_off > BUFSIZE && new_off - read_off < HALF_UCHAR ->
+ goto lost
+ :: else -> skip
+ fi;
+ }
+ atomic {
+ if
+ :: prev_off != write_off -> goto cmpxchg_loop
+ :: else -> write_off = new_off;
+ fi;
+ i = 0;
+ do
+ :: i < size ->
+ assert(buffer_use[(prev_off + i) % BUFSIZE] == 0);
+ buffer_use[(prev_off + i) % BUFSIZE] = 1;
+ i++
+ :: i >= size -> break
+ od;
+ }
+
+ /* writing to buffer...
+ */
+
+ atomic {
+ i = 0;
+ do
+ :: i < size ->
+ buffer_use[(prev_off + i) % BUFSIZE] = 0;
+ i++
+ :: i >= size -> break
+ od;
+ tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
+ commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
+ if
+ :: (((prev_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS) + SUBBUF_SIZE -
+ tmp_commit
+ -> deliver = 1
+ :: else
+ -> skip
+ fi;
+ }
+ atomic {
+ goto end;
+lost:
+ events_lost++;
+end:
+ refcount = refcount - 1;
+ }
+}
+
+/* reader
+ * Read the information sub-buffer per sub-buffer when available.
+ *
+ * Reads the information as soon as it is ready, or may be delayed by
+ * an asynchronous delivery. Being modeled as a process insures all cases
+ * (scheduled very quickly or very late, causing event loss) are covered.
+ * Only one reader per buffer (normally ensured by a mutex). This is modeled
+ * by using a single reader process.
+ */
+proctype reader()
+{
+ byte i, j;
+
+ do
+ :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0
+ && (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) < HALF_UCHAR
+ && (commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE]
+ - SUBBUF_SIZE - (((read_off / BUFSIZE) * BUFSIZE) / NR_SUBBUFS)
+ == 0) ->
+ atomic {
+ i = 0;
+ do
+ :: i < SUBBUF_SIZE ->
+ assert(buffer_use[(read_off + i) % BUFSIZE] == 0);
+ buffer_use[(read_off + i) % BUFSIZE] = 1;
+ i++
+ :: i >= SUBBUF_SIZE -> break
+ od;
+ }
+
+ /* reading from buffer...
+ */
+
+ atomic {
+ i = 0;
+ do
+ :: i < SUBBUF_SIZE ->
+ buffer_use[(read_off + i) % BUFSIZE] = 0;
+ i++
+ :: i >= SUBBUF_SIZE -> break
+ od;
+ read_off = read_off + SUBBUF_SIZE;
+ }
+ :: read_off >= (NUMPROCS - events_lost) -> break;
+ od;
+}
+
+/* Waits for all tracer and switcher processes to finish before finalizing
+ * the buffer. Only after that will the reader be allowed to read the
+ * last subbuffer.
+ */
+proctype cleaner()
+{
+ atomic {
+ do
+ :: refcount == 0 ->
+ refcount = refcount + 1;
+ run switcher(); /* Finalize the last sub-buffer so it can be read. */
+ break;
+ od;
+ }
+}
+
+init {
+ byte i = 0;
+ byte j = 0;
+ byte sum = 0;
+ byte commit_sum = 0;
+
+ atomic {
+ i = 0;
+ do
+ :: i < NR_SUBBUFS ->
+ commit_count[i] = 0;
+ i++
+ :: i >= NR_SUBBUFS -> break
+ od;
+ i = 0;
+ do
+ :: i < BUFSIZE ->
+ buffer_use[i] = 0;
+ i++
+ :: i >= BUFSIZE -> break
+ od;
+ run reader();
+ run cleaner();
+ i = 0;
+ do
+ :: i < NUMPROCS ->
+ refcount = refcount + 1;
+ run tracer();
+ i++
+ :: i >= NUMPROCS -> break
+ od;
+ i = 0;
+ do
+ :: i < NUMSWITCH ->
+ refcount = refcount + 1;
+ run switcher();
+ i++
+ :: i >= NUMSWITCH -> break
+ od;
+ }
+
+ /* Assertions.
+ */
+ atomic {
+ /* The writer head must always be superior or equal to the reader head.
+ */
+ assert(write_off - read_off >= 0 && write_off - read_off < HALF_UCHAR);
+ j = 0;
+ commit_sum = 0;
+ do
+ :: j < NR_SUBBUFS ->
+ commit_sum = commit_sum + commit_count[j];
+ /* The commit count of a particular subbuffer must always be higher
+ * or equal to the retrieve_count of this subbuffer.
+ * assert(commit_count[j] - retrieve_count[j] >= 0 &&
+ * commit_count[j] - retrieve_count[j] < HALF_UCHAR);
+ */
+ j++
+ :: j >= NR_SUBBUFS -> break
+ od;
+ /* The sum of all subbuffer commit counts must always be lower or equal
+ * to the writer head, because space must be reserved before it is
+ * written to and then committed.
+ */
+ assert(write_off - commit_sum >= 0 && write_off - commit_sum < HALF_UCHAR);
+
+ /* If we have less writers than the buffer space available, we should
+ * not lose events
+ */
+ assert(NUMPROCS + NUMSWITCH > BUFSIZE || events_lost == 0);
+ }
+}
+
projects / lttv.git / blobdiff