5 #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
10 byte deliver = 0; // Number of subbuffers delivered
13 byte commit_count[NR_SUBBUFS];
15 byte buffer_use_count[BUFSIZE];
19 int prev_off, new_off, tmp_commit;
25 size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
26 new_off = prev_off + size;
28 :: new_off - read_off > BUFSIZE ->
35 :: prev_off != write_off -> goto cmpxchg_loop
36 :: else -> write_off = new_off;
41 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
42 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
44 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
52 proctype tracer(byte size)
54 int prev_off, new_off, tmp_commit;
61 new_off = prev_off + size;
65 :: new_off - read_off > BUFSIZE -> goto lost
71 :: prev_off != write_off -> goto cmpxchg_loop
72 :: else -> write_off = new_off;
77 buffer_use_count[(prev_off + i) % BUFSIZE]
78 = buffer_use_count[(prev_off + i) % BUFSIZE] + 1;
85 assert(buffer_use_count[j] < 2);
87 :: j >= BUFSIZE -> break
92 // writing to buffer...
98 buffer_use_count[(prev_off + i) % BUFSIZE]
99 = buffer_use_count[(prev_off + i) % BUFSIZE] - 1;
101 :: i >= size -> break
103 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
104 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
106 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
114 refcount = refcount - 1;
123 // :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break;
127 :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0 && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] % SUBBUF_SIZE == 0 ->
131 :: i < SUBBUF_SIZE ->
132 buffer_use_count[(read_off + i) % BUFSIZE]
133 = buffer_use_count[(read_off + i) % BUFSIZE] + 1;
135 :: i >= SUBBUF_SIZE -> break
141 assert(buffer_use_count[j] < 2);
143 :: j >= BUFSIZE -> break
146 // reading from buffer...
151 :: i < SUBBUF_SIZE ->
152 buffer_use_count[(read_off + i) % BUFSIZE]
153 = buffer_use_count[(read_off + i) % BUFSIZE] - 1;
155 :: i >= SUBBUF_SIZE -> break
157 read_off = read_off + SUBBUF_SIZE;
159 :: read_off >= (NUMPROCS - events_lost) -> break;
186 :: i >= NR_SUBBUFS -> break
191 buffer_use_count[i] = 0;
193 :: i >= BUFSIZE -> break
200 refcount = refcount + 1;
203 :: i >= NUMPROCS -> break
208 assert(write_off - read_off >= 0);
213 commit_sum = commit_sum + commit_count[j];
215 :: j >= NR_SUBBUFS -> break
217 assert(commit_sum <= write_off);
221 assert(buffer_use_count[j] < 2);
223 :: j >= BUFSIZE -> break
226 //assert(events_lost == 0);