+++ /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