2
This file is part of drd, a data race detector.
4
Copyright (C) 2006-2007 Bart Van Assche
5
bart.vanassche@gmail.com
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.
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.
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
22
The GNU General Public License is contained in the file COPYING.
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)
36
void vc_reserve(VectorClock* const vc, const unsigned new_capacity);
39
void vc_init(VectorClock* const vc,
40
const VCElem* const vcelem,
48
tl_assert(size == 0 || vc->vc != 0);
51
VG_(memcpy)(vc->vc, vcelem, size * sizeof(vcelem[0]));
56
void vc_cleanup(VectorClock* const vc)
62
* Copy constructor -- initializes 'new'.
64
void vc_copy(VectorClock* const new,
65
const VectorClock* const rhs)
67
vc_init(new, rhs->vc, rhs->size);
70
void vc_increment(VectorClock* const vc, ThreadId const threadid)
73
for (i = 0; i < vc->size; i++)
75
if (vc->vc[i].threadid == threadid)
77
typeof(vc->vc[i].count) const oldcount = vc->vc[i].count;
79
// Check for integer overflow.
80
tl_assert(oldcount < vc->vc[i].count);
85
// The specified thread ID does not yet exist in the vector clock
88
VCElem vcelem = { threadid, 1 };
90
vc_init(&vc2, &vcelem, 1);
97
* @return True if all thread id's that are present in vc1 also exist in
98
* vc2, and if additionally all corresponding counters in v2 are higher or
101
Bool vc_lte(const VectorClock* const vc1,
102
const VectorClock* const vc2)
106
for (i = 0; i < vc1->size; i++)
108
while (j < vc2->size && vc2->vc[j].threadid < vc1->vc[i].threadid)
112
if (j >= vc2->size || vc2->vc[j].threadid > vc1->vc[i].threadid)
114
tl_assert(j < vc2->size && vc2->vc[j].threadid == vc1->vc[i].threadid);
115
if (vc1->vc[i].count > vc2->vc[j].count)
122
* @return True if vector clocks vc1 and vc2 are ordered, and false otherwise.
123
* Order is as imposed by thread synchronization actions ("happens before").
125
Bool vc_ordered(const VectorClock* const vc1,
126
const VectorClock* const vc2)
128
return vc_lte(vc1, vc2) || vc_lte(vc2, vc1);
132
* Compute elementwise minimum.
134
void vc_min(VectorClock* const result,
135
const VectorClock* const rhs)
145
// First count the number of shared thread id's.
148
for (i = 0; i < result->size; i++)
150
while (j < rhs->size && rhs->vc[j].threadid < result->vc[i].threadid)
154
if (result->vc[i].threadid == rhs->vc[j].threadid)
160
new_size = result->size + rhs->size - shared;
161
if (new_size > result->capacity)
162
vc_reserve(result, new_size);
166
// Next, combine both vector clocks into one.
168
for (j = 0; j < rhs->size; j++)
172
while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
174
if (i >= result->size)
177
result->vc[i] = rhs->vc[j];
180
else if (result->vc[i].threadid > rhs->vc[j].threadid)
183
for (k = result->size; k > i; k--)
185
result->vc[k] = result->vc[k - 1];
188
result->vc[i] = rhs->vc[j];
193
tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
194
if (rhs->vc[j].count < result->vc[i].count)
196
result->vc[i].count = rhs->vc[j].count;
202
tl_assert(result->size == new_size);
206
* Compute elementwise maximum.
208
void vc_combine(VectorClock* const result,
209
const VectorClock* const rhs)
219
// First count the number of shared thread id's.
222
for (i = 0; i < result->size; i++)
224
while (j < rhs->size && rhs->vc[j].threadid < result->vc[i].threadid)
228
if (result->vc[i].threadid == rhs->vc[j].threadid)
234
new_size = result->size + rhs->size - shared;
235
if (new_size > result->capacity)
236
vc_reserve(result, new_size);
240
// Next, combine both vector clocks into one.
242
for (j = 0; j < rhs->size; j++)
246
while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
248
if (i >= result->size)
251
result->vc[i] = rhs->vc[j];
254
else if (result->vc[i].threadid > rhs->vc[j].threadid)
257
for (k = result->size; k > i; k--)
259
result->vc[k] = result->vc[k - 1];
262
result->vc[i] = rhs->vc[j];
267
tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
268
if (rhs->vc[j].count > result->vc[i].count)
270
result->vc[i].count = rhs->vc[j].count;
276
tl_assert(result->size == new_size);
279
void vc_print(const VectorClock* const vc)
285
for (i = 0; i < vc->size; i++)
288
VG_(printf)("%s %d: %d", i > 0 ? "," : "",
289
vc->vc[i].threadid, vc->vc[i].count);
294
void vc_snprint(Char* const str, Int const size,
295
const VectorClock* const vc)
300
VG_(snprintf)(str, size, "[");
301
for (i = 0; i < vc->size; i++)
304
VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str),
305
"%s %d: %d", i > 0 ? "," : "",
306
vc->vc[i].threadid, vc->vc[i].count);
308
VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str), " ]");
314
void vc_check(const VectorClock* const vc)
317
tl_assert(vc->size <= vc->capacity);
318
for (i = 1; i < vc->size; i++)
320
tl_assert(vc->vc[i-1].threadid < vc->vc[i].threadid);
325
* Change the size of the memory block pointed at by vc->vc.
326
* Changes capacity, but does not change size. If the size of the memory
327
* block is increased, the newly allocated memory is not initialized.
330
void vc_reserve(VectorClock* const vc, const unsigned new_capacity)
333
if (new_capacity > vc->capacity)
337
vc->vc = VG_(realloc)(vc->vc, new_capacity * sizeof(vc->vc[0]));
339
else if (new_capacity > 0)
341
vc->vc = VG_(malloc)(new_capacity * sizeof(vc->vc[0]));
345
tl_assert(vc->vc == 0 && new_capacity == 0);
347
vc->capacity = new_capacity;
349
tl_assert(new_capacity == 0 || vc->vc != 0);
358
VCElem vc1elem[] = { { 3, 7 }, { 5, 8 }, };
360
VCElem vc2elem[] = { { 1, 4 }, { 3, 9 }, };
362
VCElem vc4elem[] = { { 1, 3 }, { 2, 1 }, };
364
VCElem vc5elem[] = { { 1, 4 }, };
367
vc_init(&vc1, vc1elem, sizeof(vc1elem)/sizeof(vc1elem[0]));
368
vc_init(&vc2, vc2elem, sizeof(vc2elem)/sizeof(vc2elem[0]));
370
vc_init(&vc4, vc4elem, sizeof(vc4elem)/sizeof(vc4elem[0]));
371
vc_init(&vc5, vc5elem, sizeof(vc5elem)/sizeof(vc5elem[0]));
373
vc_combine(&vc3, &vc1);
374
vc_combine(&vc3, &vc2);
376
VG_(printf)("vc1: ");
378
VG_(printf)("\nvc2: ");
380
VG_(printf)("\nvc3: ");
383
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));
387
VG_(printf)(") = %d sw %d\n", vc_lte(&vc4, &vc5), vc_lte(&vc5, &vc4));