2 // LTTng ltt-tracer.c atomic lockless buffering scheme Promela model v1
3 // Created for the Spin validator.
4 // Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
7 // TODO : create test cases that will generate an overflow on the offset and
8 // counter type. Counter types smaller than a byte should be used.
10 // Promela only has unsigned char, no signed char.
11 // Because detection of difference < 0 depends on a signed type, but we want
12 // compactness, check also for the values being higher than half of the unsigned
13 // char range (and consider them negative). The model, by design, does not use
14 // offsets or counts higher than 127 because we would then have to use a larger
15 // type (short or int).
16 #define HALF_UCHAR (255/2)
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
22 // NUMPROCS 3 : does not cause event loss because buffers are big enough.
24 // e.g. 3 events, 1 switch, read 1 subbuffer
29 #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
33 byte commit_count[NR_SUBBUFS];
37 byte retrieve_count[NR_SUBBUFS];
44 // buffer slot in-use bit. Detects racy use (more than a single process
45 // accessing a slot at any given step).
46 bool buffer_use[BUFSIZE];
48 // Proceed to a sub-subber switch is needed.
49 // Used in a periodical timer interrupt to fill and ship the current subbuffer
50 // to the reader so we can guarantee a steady flow. If a subbuffer is
51 // completely empty, don't switch.
52 // Also used as "finalize" operation to complete the last subbuffer after
53 // all writers have finished so the last subbuffer can be read by the reader.
56 byte prev_off, new_off, tmp_commit;
62 size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
63 new_off = prev_off + size;
65 :: (new_off - read_off > BUFSIZE && new_off - read_off < HALF_UCHAR)
66 || size == SUBBUF_SIZE ->
67 refcount = refcount - 1;
74 :: prev_off != write_off -> goto cmpxchg_loop
75 :: else -> write_off = new_off;
80 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
81 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
83 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1
86 refcount = refcount - 1;
93 // Writes 1 byte of information in the buffer at the current
94 // "write_off" position and then increment the commit_count of the sub-buffer
95 // the information has been written to.
99 byte prev_off, new_off, tmp_commit;
104 prev_off = write_off;
105 new_off = prev_off + size;
109 :: new_off - read_off > BUFSIZE && new_off - read_off < HALF_UCHAR ->
116 :: prev_off != write_off -> goto cmpxchg_loop
117 :: else -> write_off = new_off;
122 assert(buffer_use[(prev_off + i) % BUFSIZE] == 0);
123 buffer_use[(prev_off + i) % BUFSIZE] = 1;
125 :: i >= size -> break
129 // writing to buffer...
135 buffer_use[(prev_off + i) % BUFSIZE] = 0;
137 :: i >= size -> break
139 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
140 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
142 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver = 1;
151 refcount = refcount - 1;
156 // Read the information sub-buffer per sub-buffer when available.
158 // Reads the information as soon as it is ready, or may be delayed by
159 // an asynchronous delivery. Being modeled as a process insures all cases
160 // (scheduled very quickly or very late, causing event loss) are covered.
161 // Only one reader per buffer (normally ensured by a mutex). This is modeled
162 // by using a single reader process.
167 byte lwrite_off, lcommit_count;
170 :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0
171 && (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) < HALF_UCHAR
172 && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE]
173 - retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE]
178 :: i < SUBBUF_SIZE ->
179 assert(buffer_use[(read_off + i) % BUFSIZE] == 0);
180 buffer_use[(read_off + i) % BUFSIZE] = 1;
182 :: i >= SUBBUF_SIZE -> break
185 // reading from buffer...
187 // Since there is only one reader per buffer at any given time,
188 // we don't care about retrieve_count vs read_off ordering :
189 // combined use of retrieve_count and read_off are made atomic by a
194 :: i < SUBBUF_SIZE ->
195 buffer_use[(read_off + i) % BUFSIZE] = 0;
197 :: i >= SUBBUF_SIZE -> break
199 tmp_retrieve = retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE]
201 retrieve_count[(read_off % BUFSIZE) / SUBBUF_SIZE] = tmp_retrieve;
202 read_off = read_off + SUBBUF_SIZE;
204 :: read_off >= (NUMPROCS - events_lost) -> break;
208 // Waits for all tracer and switcher processes to finish before finalizing
209 // the buffer. Only after that will the reader be allowed to read the
216 refcount = refcount + 1;
217 run switcher(); // Finalize the last sub-buffer so it can be read.
234 retrieve_count[i] = 0;
236 :: i >= NR_SUBBUFS -> break
243 :: i >= BUFSIZE -> break
250 refcount = refcount + 1;
253 :: i >= NUMPROCS -> break
258 refcount = refcount + 1;
261 :: i >= NUMSWITCH -> break
266 // The writer head must always be superior or equal to the reader head.
267 assert(write_off - read_off >= 0 && write_off - read_off < HALF_UCHAR);
272 commit_sum = commit_sum + commit_count[j];
273 // The commit count of a particular subbuffer must always be higher
274 // or equal to the retrieve_count of this subbuffer.
275 assert(commit_count[j] - retrieve_count[j] >= 0 &&
276 commit_count[j] - retrieve_count[j] < HALF_UCHAR);
278 :: j >= NR_SUBBUFS -> break
280 // The sum of all subbuffer commit counts must always be lower or equal
281 // to the writer head, because space must be reserved before it is
282 // written to and then committed.
283 assert(write_off - commit_sum >= 0 && write_off - commit_sum < HALF_UCHAR);
285 // If we have less writers than the buffer space available, we should
287 assert(NUMPROCS + NUMSWITCH > BUFSIZE || events_lost == 0);