5 #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS)
10 byte deliver = 0; // Number of subbuffers delivered
13 byte commit_count[NR_SUBBUFS];
17 int prev_off, new_off, tmp_commit;
23 size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE);
24 new_off = prev_off + size;
26 :: new_off - read_off > BUFSIZE ->
33 :: prev_off != write_off -> goto cmpxchg_loop
34 :: else -> write_off = new_off;
39 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
40 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
42 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
50 proctype tracer(byte size)
52 int prev_off, new_off, tmp_commit;
57 new_off = prev_off + size;
61 :: new_off - read_off > BUFSIZE -> goto lost
67 :: prev_off != write_off -> goto cmpxchg_loop
68 :: else -> write_off = new_off;
73 tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size;
74 commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit;
76 :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++
84 refcount = refcount - 1;
91 // :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break;
94 // made atomic to use less memory. Not really true.
97 :: write_off - read_off >= SUBBUF_SIZE && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] % SUBBUF_SIZE == 0 ->
98 read_off = read_off + SUBBUF_SIZE;
99 :: read_off >= (NUMPROCS - events_lost) -> break;
127 :: i >= NR_SUBBUFS -> break
134 refcount = refcount + 1;
137 :: i >= NUMPROCS -> break
142 assert(write_off - read_off >= 0);
147 commit_sum = commit_sum + commit_count[j];
149 :: j >= NR_SUBBUFS -> break
151 assert(commit_sum <= write_off);
152 //assert(events_lost == 0);