0b55f123 |
1 | //#define NUMPROCS 5 |
2 | #define NUMPROCS 4 |
3 | #define BUFSIZE 4 |
4 | #define NR_SUBBUFS 2 |
5 | #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS) |
6 | |
7 | byte write_off = 0; |
8 | byte read_off = 0; |
9 | byte events_lost = 0; |
10 | byte deliver = 0; // Number of subbuffers delivered |
11 | byte refcount = 0; |
12 | |
13 | byte commit_count[NR_SUBBUFS]; |
14 | |
15 | proctype switcher() |
16 | { |
17 | int prev_off, new_off, tmp_commit; |
18 | int size; |
19 | |
20 | cmpxchg_loop: |
21 | atomic { |
22 | prev_off = write_off; |
23 | size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE); |
24 | new_off = prev_off + size; |
25 | if |
26 | :: new_off - read_off > BUFSIZE -> |
27 | goto not_needed; |
28 | :: else -> skip |
29 | fi; |
30 | } |
31 | atomic { |
32 | if |
33 | :: prev_off != write_off -> goto cmpxchg_loop |
34 | :: else -> write_off = new_off; |
35 | fi; |
36 | } |
37 | |
38 | atomic { |
39 | tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; |
40 | commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; |
41 | if |
42 | :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++ |
43 | :: else -> skip |
44 | fi; |
45 | } |
46 | not_needed: |
47 | skip; |
48 | } |
49 | |
50 | proctype tracer(byte size) |
51 | { |
52 | int prev_off, new_off, tmp_commit; |
53 | |
54 | cmpxchg_loop: |
55 | atomic { |
56 | prev_off = write_off; |
57 | new_off = prev_off + size; |
58 | } |
59 | atomic { |
60 | if |
61 | :: new_off - read_off > BUFSIZE -> goto lost |
62 | :: else -> skip |
63 | fi; |
64 | } |
65 | atomic { |
66 | if |
67 | :: prev_off != write_off -> goto cmpxchg_loop |
68 | :: else -> write_off = new_off; |
69 | fi; |
70 | } |
71 | |
72 | atomic { |
73 | tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; |
74 | commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; |
75 | if |
76 | :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++ |
77 | :: else -> skip |
78 | fi; |
79 | } |
80 | goto end; |
81 | lost: |
82 | events_lost++; |
83 | end: |
84 | refcount = refcount - 1; |
85 | } |
86 | |
87 | proctype reader() |
88 | { |
89 | //atomic { |
90 | // do |
91 | // :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break; |
92 | // od; |
93 | //} |
94 | // made atomic to use less memory. Not really true. |
95 | atomic { |
96 | do |
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; |
100 | od; |
101 | } |
102 | } |
103 | |
104 | proctype cleaner() |
105 | { |
106 | atomic { |
107 | do |
108 | :: refcount == 0 -> |
109 | run switcher(); |
110 | break; |
111 | od; |
112 | } |
113 | } |
114 | |
115 | init { |
116 | int i = 0; |
117 | int j = 0; |
118 | int sum = 0; |
119 | int commit_sum = 0; |
120 | |
121 | atomic { |
122 | i = 0; |
123 | do |
124 | :: i < NR_SUBBUFS -> |
125 | commit_count[i] = 0; |
126 | i++ |
127 | :: i >= NR_SUBBUFS -> break |
128 | od; |
129 | run reader(); |
130 | run cleaner(); |
131 | i = 0; |
132 | do |
133 | :: i < NUMPROCS -> |
134 | refcount = refcount + 1; |
135 | run tracer(1); |
136 | i++ |
137 | :: i >= NUMPROCS -> break |
138 | od; |
139 | run switcher(); |
140 | } |
141 | atomic { |
142 | assert(write_off - read_off >= 0); |
143 | j = 0; |
144 | commit_sum = 0; |
145 | do |
146 | :: j < NR_SUBBUFS -> |
147 | commit_sum = commit_sum + commit_count[j]; |
148 | j++ |
149 | :: j >= NR_SUBBUFS -> break |
150 | od; |
151 | assert(commit_sum <= write_off); |
152 | //assert(events_lost == 0); |
153 | } |
154 | } |