blob: b083974d718cdd5d8113c631018b19cde196aeaf [file] [log] [blame]
sewardjaf44c822007-11-25 14:01:38 +00001/*
2 This file is part of drd, a data race detector.
3
sewardj85642922008-01-14 11:54:56 +00004 Copyright (C) 2006-2008 Bart Van Assche
sewardjaf44c822007-11-25 14:01:38 +00005 bart.vanassche@gmail.com
6
7 This program is free software; you can redistribute it and/or
8 modify it under the terms of the GNU General Public License as
9 published by the Free Software Foundation; either version 2 of the
10 License, or (at your option) any later version.
11
12 This program is distributed in the hope that it will be useful, but
13 WITHOUT ANY WARRANTY; without even the implied warranty of
14 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
15 General Public License for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software
19 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
20 02111-1307, USA.
21
22 The GNU General Public License is contained in the file COPYING.
23*/
24
25
26#include "drd_vc.h"
27#include "pub_tool_basics.h" // Addr, SizeT
28#include "pub_tool_libcassert.h" // tl_assert()
29#include "pub_tool_libcbase.h" // VG_(memset), VG_(memmove)
30#include "pub_tool_libcprint.h" // VG_(printf)
31#include "pub_tool_mallocfree.h" // VG_(malloc), VG_(free)
32#include "pub_tool_threadstate.h" // VG_(get_running_tid)
33
34
35static
36void vc_reserve(VectorClock* const vc, const unsigned new_capacity);
37
38
39void vc_init(VectorClock* const vc,
40 const VCElem* const vcelem,
41 const unsigned size)
42{
43 tl_assert(vc);
44 vc->size = 0;
45 vc->capacity = 0;
46 vc->vc = 0;
47 vc_reserve(vc, size);
48 tl_assert(size == 0 || vc->vc != 0);
49 if (vcelem)
50 {
51 VG_(memcpy)(vc->vc, vcelem, size * sizeof(vcelem[0]));
52 vc->size = size;
53 }
54}
55
56void vc_cleanup(VectorClock* const vc)
57{
58 vc_reserve(vc, 0);
59}
60
bartc46c2322008-02-24 18:26:46 +000061/** Copy constructor -- initializes *new. */
sewardjaf44c822007-11-25 14:01:38 +000062void vc_copy(VectorClock* const new,
63 const VectorClock* const rhs)
64{
65 vc_init(new, rhs->vc, rhs->size);
66}
67
bartc46c2322008-02-24 18:26:46 +000068/** Assignment operator -- *lhs is already a valid vector clock. */
69void vc_assign(VectorClock* const lhs,
70 const VectorClock* const rhs)
71{
72 vc_cleanup(lhs);
73 vc_copy(lhs, rhs);
74}
75
sewardjaf44c822007-11-25 14:01:38 +000076void vc_increment(VectorClock* const vc, ThreadId const threadid)
77{
78 unsigned i;
79 for (i = 0; i < vc->size; i++)
80 {
81 if (vc->vc[i].threadid == threadid)
82 {
83 typeof(vc->vc[i].count) const oldcount = vc->vc[i].count;
84 vc->vc[i].count++;
85 // Check for integer overflow.
86 tl_assert(oldcount < vc->vc[i].count);
87 return;
88 }
89 }
90
91 // The specified thread ID does not yet exist in the vector clock
92 // -- insert it.
93 {
94 VCElem vcelem = { threadid, 1 };
95 VectorClock vc2;
96 vc_init(&vc2, &vcelem, 1);
97 vc_combine(vc, &vc2);
98 vc_cleanup(&vc2);
99 }
100}
101
102/**
sewardjaf44c822007-11-25 14:01:38 +0000103 * @return True if vector clocks vc1 and vc2 are ordered, and false otherwise.
104 * Order is as imposed by thread synchronization actions ("happens before").
105 */
106Bool vc_ordered(const VectorClock* const vc1,
107 const VectorClock* const vc2)
108{
109 return vc_lte(vc1, vc2) || vc_lte(vc2, vc1);
110}
111
bart5bd9f2d2008-03-03 20:31:58 +0000112/** Compute elementwise minimum. */
barta7faf672008-03-06 18:02:37 +0000113void vc_min(VectorClock* const result, const VectorClock* const rhs)
sewardjaf44c822007-11-25 14:01:38 +0000114{
115 unsigned i;
116 unsigned j;
sewardjaf44c822007-11-25 14:01:38 +0000117
118 tl_assert(result);
119 tl_assert(rhs);
120
sewardjaf44c822007-11-25 14:01:38 +0000121 vc_check(result);
122
bart5bd9f2d2008-03-03 20:31:58 +0000123 /* Next, combine both vector clocks into one. */
sewardjaf44c822007-11-25 14:01:38 +0000124 i = 0;
125 for (j = 0; j < rhs->size; j++)
126 {
sewardjaf44c822007-11-25 14:01:38 +0000127 while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
bart5bd9f2d2008-03-03 20:31:58 +0000128 {
129 /* Thread ID is missing in second vector clock. Clear the count. */
130 result->vc[i].count = 0;
sewardjaf44c822007-11-25 14:01:38 +0000131 i++;
bart5bd9f2d2008-03-03 20:31:58 +0000132 }
sewardjaf44c822007-11-25 14:01:38 +0000133 if (i >= result->size)
134 {
barta7faf672008-03-06 18:02:37 +0000135 break;
sewardjaf44c822007-11-25 14:01:38 +0000136 }
barta7faf672008-03-06 18:02:37 +0000137 if (result->vc[i].threadid <= rhs->vc[j].threadid)
sewardjaf44c822007-11-25 14:01:38 +0000138 {
bart5bd9f2d2008-03-03 20:31:58 +0000139 /* The thread ID is present in both vector clocks. Compute the minimum */
140 /* of vc[i].count and vc[j].count. */
sewardjaf44c822007-11-25 14:01:38 +0000141 tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
142 if (rhs->vc[j].count < result->vc[i].count)
143 {
144 result->vc[i].count = rhs->vc[j].count;
145 }
sewardjaf44c822007-11-25 14:01:38 +0000146 }
147 }
148 vc_check(result);
sewardjaf44c822007-11-25 14:01:38 +0000149}
150
151/**
152 * Compute elementwise maximum.
153 */
154void vc_combine(VectorClock* const result,
155 const VectorClock* const rhs)
156{
bartfbbac092008-04-06 14:57:37 +0000157 vc_combine2(result, rhs, -1);
158}
159
160/** Compute elementwise maximum.
161 *
162 * @return True if *result and *rhs are equal, or if *result and *rhs only
163 * differ in the component with thread ID tid.
164 */
165Bool vc_combine2(VectorClock* const result,
166 const VectorClock* const rhs,
167 const ThreadId tid)
168{
sewardjaf44c822007-11-25 14:01:38 +0000169 unsigned i;
170 unsigned j;
171 unsigned shared;
172 unsigned new_size;
bartfbbac092008-04-06 14:57:37 +0000173 Bool almost_equal = True;
sewardjaf44c822007-11-25 14:01:38 +0000174
175 tl_assert(result);
176 tl_assert(rhs);
177
178 // First count the number of shared thread id's.
179 j = 0;
180 shared = 0;
181 for (i = 0; i < result->size; i++)
182 {
183 while (j < rhs->size && rhs->vc[j].threadid < result->vc[i].threadid)
184 j++;
185 if (j >= rhs->size)
186 break;
187 if (result->vc[i].threadid == rhs->vc[j].threadid)
188 shared++;
189 }
190
191 vc_check(result);
192
193 new_size = result->size + rhs->size - shared;
194 if (new_size > result->capacity)
195 vc_reserve(result, new_size);
196
197 vc_check(result);
198
199 // Next, combine both vector clocks into one.
200 i = 0;
201 for (j = 0; j < rhs->size; j++)
202 {
bartfbbac092008-04-06 14:57:37 +0000203 /* First of all, skip those clocks in result->vc[] for which there */
204 /* is no corresponding clock in rhs->vc[]. */
sewardjaf44c822007-11-25 14:01:38 +0000205 while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
bartfbbac092008-04-06 14:57:37 +0000206 {
207 if (result->vc[i].threadid != tid)
208 {
209 almost_equal = False;
210 }
sewardjaf44c822007-11-25 14:01:38 +0000211 i++;
bartfbbac092008-04-06 14:57:37 +0000212 }
213 /* If the end of *result is met, append rhs->vc[j] to *result. */
sewardjaf44c822007-11-25 14:01:38 +0000214 if (i >= result->size)
215 {
216 result->size++;
217 result->vc[i] = rhs->vc[j];
bartfbbac092008-04-06 14:57:37 +0000218 if (result->vc[i].threadid != tid)
219 {
220 almost_equal = False;
221 }
sewardjaf44c822007-11-25 14:01:38 +0000222 }
bartfbbac092008-04-06 14:57:37 +0000223 /* If clock rhs->vc[j] is not in *result, insert it. */
sewardjaf44c822007-11-25 14:01:38 +0000224 else if (result->vc[i].threadid > rhs->vc[j].threadid)
225 {
226 unsigned k;
227 for (k = result->size; k > i; k--)
228 {
229 result->vc[k] = result->vc[k - 1];
230 }
231 result->size++;
232 result->vc[i] = rhs->vc[j];
bartfbbac092008-04-06 14:57:37 +0000233 if (result->vc[i].threadid != tid)
234 {
235 almost_equal = False;
236 }
sewardjaf44c822007-11-25 14:01:38 +0000237 }
bartfbbac092008-04-06 14:57:37 +0000238 /* Otherwise, both *result and *rhs have a clock for thread */
239 /* result->vc[i].threadid == rhs->vc[j].threadid. Compute the maximum. */
sewardjaf44c822007-11-25 14:01:38 +0000240 else
241 {
242 tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
bartfbbac092008-04-06 14:57:37 +0000243 if (result->vc[i].threadid != tid
244 && rhs->vc[j].count != result->vc[i].count)
245 {
246 almost_equal = False;
247 }
sewardjaf44c822007-11-25 14:01:38 +0000248 if (rhs->vc[j].count > result->vc[i].count)
249 {
250 result->vc[i].count = rhs->vc[j].count;
251 }
sewardjaf44c822007-11-25 14:01:38 +0000252 }
253 }
254 vc_check(result);
255 tl_assert(result->size == new_size);
bartfbbac092008-04-06 14:57:37 +0000256
257 return almost_equal;
sewardjaf44c822007-11-25 14:01:38 +0000258}
259
260void vc_print(const VectorClock* const vc)
261{
262 unsigned i;
263
264 tl_assert(vc);
265 VG_(printf)("[");
266 for (i = 0; i < vc->size; i++)
267 {
268 tl_assert(vc->vc);
269 VG_(printf)("%s %d: %d", i > 0 ? "," : "",
270 vc->vc[i].threadid, vc->vc[i].count);
271 }
272 VG_(printf)(" ]");
273}
274
275void vc_snprint(Char* const str, Int const size,
276 const VectorClock* const vc)
277{
278 unsigned i;
bartfdb65582008-04-06 13:03:49 +0000279 unsigned j = 1;
sewardjaf44c822007-11-25 14:01:38 +0000280
281 tl_assert(vc);
282 VG_(snprintf)(str, size, "[");
283 for (i = 0; i < vc->size; i++)
284 {
285 tl_assert(vc->vc);
bartfdb65582008-04-06 13:03:49 +0000286 for ( ; j <= vc->vc[i].threadid; j++)
287 {
288 VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str),
289 "%s %d",
290 i > 0 ? "," : "",
291 (j == vc->vc[i].threadid) ? vc->vc[i].count : 0);
292 }
sewardjaf44c822007-11-25 14:01:38 +0000293 }
294 VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str), " ]");
295}
296
297/**
298 * Invariant test.
299 */
300void vc_check(const VectorClock* const vc)
301{
302 unsigned i;
303 tl_assert(vc->size <= vc->capacity);
304 for (i = 1; i < vc->size; i++)
305 {
306 tl_assert(vc->vc[i-1].threadid < vc->vc[i].threadid);
307 }
308}
309
310/**
311 * Change the size of the memory block pointed at by vc->vc.
312 * Changes capacity, but does not change size. If the size of the memory
313 * block is increased, the newly allocated memory is not initialized.
314 */
315static
316void vc_reserve(VectorClock* const vc, const unsigned new_capacity)
317{
318 tl_assert(vc);
319 if (new_capacity > vc->capacity)
320 {
321 if (vc->vc)
322 {
323 vc->vc = VG_(realloc)(vc->vc, new_capacity * sizeof(vc->vc[0]));
324 }
325 else if (new_capacity > 0)
326 {
327 vc->vc = VG_(malloc)(new_capacity * sizeof(vc->vc[0]));
328 }
329 else
330 {
331 tl_assert(vc->vc == 0 && new_capacity == 0);
332 }
333 vc->capacity = new_capacity;
334 }
335 tl_assert(new_capacity == 0 || vc->vc != 0);
336}
337
338/**
339 * Unit test.
340 */
341void vc_test(void)
342{
343 VectorClock vc1;
344 VCElem vc1elem[] = { { 3, 7 }, { 5, 8 }, };
345 VectorClock vc2;
346 VCElem vc2elem[] = { { 1, 4 }, { 3, 9 }, };
347 VectorClock vc3;
348 VCElem vc4elem[] = { { 1, 3 }, { 2, 1 }, };
349 VectorClock vc4;
350 VCElem vc5elem[] = { { 1, 4 }, };
351 VectorClock vc5;
352
353 vc_init(&vc1, vc1elem, sizeof(vc1elem)/sizeof(vc1elem[0]));
354 vc_init(&vc2, vc2elem, sizeof(vc2elem)/sizeof(vc2elem[0]));
355 vc_init(&vc3, 0, 0);
356 vc_init(&vc4, vc4elem, sizeof(vc4elem)/sizeof(vc4elem[0]));
357 vc_init(&vc5, vc5elem, sizeof(vc5elem)/sizeof(vc5elem[0]));
358
359 vc_combine(&vc3, &vc1);
360 vc_combine(&vc3, &vc2);
361
362 VG_(printf)("vc1: ");
363 vc_print(&vc1);
364 VG_(printf)("\nvc2: ");
365 vc_print(&vc2);
366 VG_(printf)("\nvc3: ");
367 vc_print(&vc3);
368 VG_(printf)("\n");
369 VG_(printf)("vc_lte(vc1, vc2) = %d, vc_lte(vc1, vc3) = %d, vc_lte(vc2, vc3) = %d, vc_lte(", vc_lte(&vc1, &vc2), vc_lte(&vc1, &vc3), vc_lte(&vc2, &vc3));
370 vc_print(&vc4);
371 VG_(printf)(", ");
372 vc_print(&vc5);
373 VG_(printf)(") = %d sw %d\n", vc_lte(&vc4, &vc5), vc_lte(&vc5, &vc4));
374
375 vc_cleanup(&vc1);
376 vc_cleanup(&vc2);
377 vc_cleanup(&vc3);
378}