blob: 7f14f1a2704b9c9ca4dfeed3295efeb1f9f1ef53 [file] [log] [blame]
sewardjaf44c822007-11-25 14:01:38 +00001/*
bart86562bd2009-02-16 19:43:56 +00002 This file is part of drd, a thread error detector.
sewardjaf44c822007-11-25 14:01:38 +00003
bart86562bd2009-02-16 19:43:56 +00004 Copyright (C) 2006-2009 Bart Van Assche <bart.vanassche@gmail.com>.
sewardjaf44c822007-11-25 14:01:38 +00005
6 This program is free software; you can redistribute it and/or
7 modify it under the terms of the GNU General Public License as
8 published by the Free Software Foundation; either version 2 of the
9 License, or (at your option) any later version.
10
11 This program is distributed in the hope that it will be useful, but
12 WITHOUT ANY WARRANTY; without even the implied warranty of
13 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
14 General Public License for more details.
15
16 You should have received a copy of the GNU General Public License
17 along with this program; if not, write to the Free Software
18 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
19 02111-1307, USA.
20
21 The GNU General Public License is contained in the file COPYING.
22*/
23
24
25#include "drd_vc.h"
26#include "pub_tool_basics.h" // Addr, SizeT
27#include "pub_tool_libcassert.h" // tl_assert()
bart41b226c2009-02-14 16:55:19 +000028#include "pub_tool_libcbase.h" // VG_(memcpy)
sewardjaf44c822007-11-25 14:01:38 +000029#include "pub_tool_libcprint.h" // VG_(printf)
30#include "pub_tool_mallocfree.h" // VG_(malloc), VG_(free)
sewardjaf44c822007-11-25 14:01:38 +000031
32
bart41b226c2009-02-14 16:55:19 +000033/* Local function declarations. */
34
sewardjaf44c822007-11-25 14:01:38 +000035static
bart41b226c2009-02-14 16:55:19 +000036void DRD_(vc_reserve)(VectorClock* const vc, const unsigned new_capacity);
sewardjaf44c822007-11-25 14:01:38 +000037
38
bart41b226c2009-02-14 16:55:19 +000039/* Function definitions. */
40
41/**
42 * Initialize the memory 'vc' points at as a vector clock with size 'size'.
43 * If the pointer 'vcelem' is not null, it is assumed to be an array with
44 * 'size' elements and it becomes the initial value of the vector clock.
45 */
46void DRD_(vc_init)(VectorClock* const vc,
47 const VCElem* const vcelem,
48 const unsigned size)
sewardjaf44c822007-11-25 14:01:38 +000049{
50 tl_assert(vc);
51 vc->size = 0;
52 vc->capacity = 0;
53 vc->vc = 0;
bart41b226c2009-02-14 16:55:19 +000054 DRD_(vc_reserve)(vc, size);
sewardjaf44c822007-11-25 14:01:38 +000055 tl_assert(size == 0 || vc->vc != 0);
56 if (vcelem)
57 {
58 VG_(memcpy)(vc->vc, vcelem, size * sizeof(vcelem[0]));
59 vc->size = size;
60 }
61}
62
bart41b226c2009-02-14 16:55:19 +000063/** Reset vc to the empty vector clock. */
64void DRD_(vc_cleanup)(VectorClock* const vc)
sewardjaf44c822007-11-25 14:01:38 +000065{
bart41b226c2009-02-14 16:55:19 +000066 DRD_(vc_reserve)(vc, 0);
sewardjaf44c822007-11-25 14:01:38 +000067}
68
bartc46c2322008-02-24 18:26:46 +000069/** Copy constructor -- initializes *new. */
bart41b226c2009-02-14 16:55:19 +000070void DRD_(vc_copy)(VectorClock* const new, const VectorClock* const rhs)
sewardjaf44c822007-11-25 14:01:38 +000071{
bart41b226c2009-02-14 16:55:19 +000072 DRD_(vc_init)(new, rhs->vc, rhs->size);
sewardjaf44c822007-11-25 14:01:38 +000073}
74
bartc46c2322008-02-24 18:26:46 +000075/** Assignment operator -- *lhs is already a valid vector clock. */
bart41b226c2009-02-14 16:55:19 +000076void DRD_(vc_assign)(VectorClock* const lhs, const VectorClock* const rhs)
bartc46c2322008-02-24 18:26:46 +000077{
bart41b226c2009-02-14 16:55:19 +000078 DRD_(vc_cleanup)(lhs);
79 DRD_(vc_copy)(lhs, rhs);
bartc46c2322008-02-24 18:26:46 +000080}
81
bart41b226c2009-02-14 16:55:19 +000082/** Increment the clock of thread 'tid' in vector clock 'vc'. */
83void DRD_(vc_increment)(VectorClock* const vc, DrdThreadId const tid)
sewardjaf44c822007-11-25 14:01:38 +000084{
85 unsigned i;
86 for (i = 0; i < vc->size; i++)
87 {
bart41b226c2009-02-14 16:55:19 +000088 if (vc->vc[i].threadid == tid)
sewardjaf44c822007-11-25 14:01:38 +000089 {
90 typeof(vc->vc[i].count) const oldcount = vc->vc[i].count;
91 vc->vc[i].count++;
92 // Check for integer overflow.
93 tl_assert(oldcount < vc->vc[i].count);
94 return;
95 }
96 }
97
bart41b226c2009-02-14 16:55:19 +000098 /*
99 * The specified thread ID does not yet exist in the vector clock
100 * -- insert it.
101 */
sewardjaf44c822007-11-25 14:01:38 +0000102 {
bart41b226c2009-02-14 16:55:19 +0000103 const VCElem vcelem = { tid, 1 };
sewardjaf44c822007-11-25 14:01:38 +0000104 VectorClock vc2;
bart41b226c2009-02-14 16:55:19 +0000105 DRD_(vc_init)(&vc2, &vcelem, 1);
106 DRD_(vc_combine)(vc, &vc2);
107 DRD_(vc_cleanup)(&vc2);
sewardjaf44c822007-11-25 14:01:38 +0000108 }
109}
110
111/**
sewardjaf44c822007-11-25 14:01:38 +0000112 * @return True if vector clocks vc1 and vc2 are ordered, and false otherwise.
113 * Order is as imposed by thread synchronization actions ("happens before").
114 */
bart41b226c2009-02-14 16:55:19 +0000115Bool DRD_(vc_ordered)(const VectorClock* const vc1,
116 const VectorClock* const vc2)
sewardjaf44c822007-11-25 14:01:38 +0000117{
bart41b226c2009-02-14 16:55:19 +0000118 return DRD_(vc_lte)(vc1, vc2) || DRD_(vc_lte)(vc2, vc1);
sewardjaf44c822007-11-25 14:01:38 +0000119}
120
bart5bd9f2d2008-03-03 20:31:58 +0000121/** Compute elementwise minimum. */
bart41b226c2009-02-14 16:55:19 +0000122void DRD_(vc_min)(VectorClock* const result, const VectorClock* const rhs)
sewardjaf44c822007-11-25 14:01:38 +0000123{
124 unsigned i;
125 unsigned j;
sewardjaf44c822007-11-25 14:01:38 +0000126
127 tl_assert(result);
128 tl_assert(rhs);
129
bart41b226c2009-02-14 16:55:19 +0000130 DRD_(vc_check)(result);
sewardjaf44c822007-11-25 14:01:38 +0000131
bart5bd9f2d2008-03-03 20:31:58 +0000132 /* Next, combine both vector clocks into one. */
sewardjaf44c822007-11-25 14:01:38 +0000133 i = 0;
134 for (j = 0; j < rhs->size; j++)
135 {
sewardjaf44c822007-11-25 14:01:38 +0000136 while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
bart5bd9f2d2008-03-03 20:31:58 +0000137 {
138 /* Thread ID is missing in second vector clock. Clear the count. */
139 result->vc[i].count = 0;
sewardjaf44c822007-11-25 14:01:38 +0000140 i++;
bart5bd9f2d2008-03-03 20:31:58 +0000141 }
sewardjaf44c822007-11-25 14:01:38 +0000142 if (i >= result->size)
143 {
barta7faf672008-03-06 18:02:37 +0000144 break;
sewardjaf44c822007-11-25 14:01:38 +0000145 }
barta7faf672008-03-06 18:02:37 +0000146 if (result->vc[i].threadid <= rhs->vc[j].threadid)
sewardjaf44c822007-11-25 14:01:38 +0000147 {
bart5bd9f2d2008-03-03 20:31:58 +0000148 /* The thread ID is present in both vector clocks. Compute the minimum */
149 /* of vc[i].count and vc[j].count. */
sewardjaf44c822007-11-25 14:01:38 +0000150 tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
151 if (rhs->vc[j].count < result->vc[i].count)
152 {
153 result->vc[i].count = rhs->vc[j].count;
154 }
sewardjaf44c822007-11-25 14:01:38 +0000155 }
156 }
bart41b226c2009-02-14 16:55:19 +0000157 DRD_(vc_check)(result);
sewardjaf44c822007-11-25 14:01:38 +0000158}
159
160/**
161 * Compute elementwise maximum.
162 */
bart41b226c2009-02-14 16:55:19 +0000163void DRD_(vc_combine)(VectorClock* const result, const VectorClock* const rhs)
sewardjaf44c822007-11-25 14:01:38 +0000164{
bart41b226c2009-02-14 16:55:19 +0000165 DRD_(vc_combine2)(result, rhs, -1);
bartfbbac092008-04-06 14:57:37 +0000166}
167
bart41b226c2009-02-14 16:55:19 +0000168/**
169 * Compute elementwise maximum.
bartfbbac092008-04-06 14:57:37 +0000170 *
bart41b226c2009-02-14 16:55:19 +0000171 * @return True if *result and *rhs are equal, or if *result and *rhs only
172 * differ in the component with thread ID tid.
bartfbbac092008-04-06 14:57:37 +0000173 */
bart41b226c2009-02-14 16:55:19 +0000174Bool DRD_(vc_combine2)(VectorClock* const result,
175 const VectorClock* const rhs,
176 const DrdThreadId tid)
bartfbbac092008-04-06 14:57:37 +0000177{
sewardjaf44c822007-11-25 14:01:38 +0000178 unsigned i;
179 unsigned j;
180 unsigned shared;
181 unsigned new_size;
bartfbbac092008-04-06 14:57:37 +0000182 Bool almost_equal = True;
sewardjaf44c822007-11-25 14:01:38 +0000183
184 tl_assert(result);
185 tl_assert(rhs);
186
187 // First count the number of shared thread id's.
188 j = 0;
189 shared = 0;
190 for (i = 0; i < result->size; i++)
191 {
192 while (j < rhs->size && rhs->vc[j].threadid < result->vc[i].threadid)
193 j++;
194 if (j >= rhs->size)
195 break;
196 if (result->vc[i].threadid == rhs->vc[j].threadid)
197 shared++;
198 }
199
bart41b226c2009-02-14 16:55:19 +0000200 DRD_(vc_check)(result);
sewardjaf44c822007-11-25 14:01:38 +0000201
202 new_size = result->size + rhs->size - shared;
203 if (new_size > result->capacity)
bart41b226c2009-02-14 16:55:19 +0000204 DRD_(vc_reserve)(result, new_size);
sewardjaf44c822007-11-25 14:01:38 +0000205
bart41b226c2009-02-14 16:55:19 +0000206 DRD_(vc_check)(result);
sewardjaf44c822007-11-25 14:01:38 +0000207
208 // Next, combine both vector clocks into one.
209 i = 0;
210 for (j = 0; j < rhs->size; j++)
211 {
bartfbbac092008-04-06 14:57:37 +0000212 /* First of all, skip those clocks in result->vc[] for which there */
213 /* is no corresponding clock in rhs->vc[]. */
sewardjaf44c822007-11-25 14:01:38 +0000214 while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid)
bartfbbac092008-04-06 14:57:37 +0000215 {
216 if (result->vc[i].threadid != tid)
217 {
218 almost_equal = False;
219 }
sewardjaf44c822007-11-25 14:01:38 +0000220 i++;
bartfbbac092008-04-06 14:57:37 +0000221 }
222 /* If the end of *result is met, append rhs->vc[j] to *result. */
sewardjaf44c822007-11-25 14:01:38 +0000223 if (i >= result->size)
224 {
225 result->size++;
226 result->vc[i] = rhs->vc[j];
bartfbbac092008-04-06 14:57:37 +0000227 if (result->vc[i].threadid != tid)
228 {
229 almost_equal = False;
230 }
sewardjaf44c822007-11-25 14:01:38 +0000231 }
bartfbbac092008-04-06 14:57:37 +0000232 /* If clock rhs->vc[j] is not in *result, insert it. */
sewardjaf44c822007-11-25 14:01:38 +0000233 else if (result->vc[i].threadid > rhs->vc[j].threadid)
234 {
235 unsigned k;
236 for (k = result->size; k > i; k--)
237 {
238 result->vc[k] = result->vc[k - 1];
239 }
240 result->size++;
241 result->vc[i] = rhs->vc[j];
bartfbbac092008-04-06 14:57:37 +0000242 if (result->vc[i].threadid != tid)
243 {
244 almost_equal = False;
245 }
sewardjaf44c822007-11-25 14:01:38 +0000246 }
bartfbbac092008-04-06 14:57:37 +0000247 /* Otherwise, both *result and *rhs have a clock for thread */
248 /* result->vc[i].threadid == rhs->vc[j].threadid. Compute the maximum. */
sewardjaf44c822007-11-25 14:01:38 +0000249 else
250 {
251 tl_assert(result->vc[i].threadid == rhs->vc[j].threadid);
bartfbbac092008-04-06 14:57:37 +0000252 if (result->vc[i].threadid != tid
253 && rhs->vc[j].count != result->vc[i].count)
254 {
255 almost_equal = False;
256 }
sewardjaf44c822007-11-25 14:01:38 +0000257 if (rhs->vc[j].count > result->vc[i].count)
258 {
259 result->vc[i].count = rhs->vc[j].count;
260 }
sewardjaf44c822007-11-25 14:01:38 +0000261 }
262 }
bart41b226c2009-02-14 16:55:19 +0000263 DRD_(vc_check)(result);
sewardjaf44c822007-11-25 14:01:38 +0000264 tl_assert(result->size == new_size);
bartfbbac092008-04-06 14:57:37 +0000265
266 return almost_equal;
sewardjaf44c822007-11-25 14:01:38 +0000267}
268
bart41b226c2009-02-14 16:55:19 +0000269/** Print the contents of vector clock 'vc'. */
270void DRD_(vc_print)(const VectorClock* const vc)
sewardjaf44c822007-11-25 14:01:38 +0000271{
272 unsigned i;
273
274 tl_assert(vc);
275 VG_(printf)("[");
276 for (i = 0; i < vc->size; i++)
277 {
278 tl_assert(vc->vc);
279 VG_(printf)("%s %d: %d", i > 0 ? "," : "",
280 vc->vc[i].threadid, vc->vc[i].count);
281 }
282 VG_(printf)(" ]");
283}
284
bart41b226c2009-02-14 16:55:19 +0000285/**
286 * Print the contents of vector clock 'vc' to the character array 'str' that
287 * has 'size' elements.
288 */
289void DRD_(vc_snprint)(Char* const str, const Int size,
290 const VectorClock* const vc)
sewardjaf44c822007-11-25 14:01:38 +0000291{
292 unsigned i;
bartfdb65582008-04-06 13:03:49 +0000293 unsigned j = 1;
sewardjaf44c822007-11-25 14:01:38 +0000294
295 tl_assert(vc);
296 VG_(snprintf)(str, size, "[");
297 for (i = 0; i < vc->size; i++)
298 {
299 tl_assert(vc->vc);
bartfdb65582008-04-06 13:03:49 +0000300 for ( ; j <= vc->vc[i].threadid; j++)
301 {
302 VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str),
303 "%s %d",
304 i > 0 ? "," : "",
305 (j == vc->vc[i].threadid) ? vc->vc[i].count : 0);
306 }
sewardjaf44c822007-11-25 14:01:38 +0000307 }
308 VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str), " ]");
309}
310
311/**
312 * Invariant test.
bart41b226c2009-02-14 16:55:19 +0000313 *
314 * The function below tests whether the following two conditions are
315 * satisfied:
316 * - size <= capacity.
317 * - Vector clock elements are stored in thread ID order.
318 *
319 * If one of these conditions is not met, an assertion failure is triggered.
sewardjaf44c822007-11-25 14:01:38 +0000320 */
bart41b226c2009-02-14 16:55:19 +0000321void DRD_(vc_check)(const VectorClock* const vc)
sewardjaf44c822007-11-25 14:01:38 +0000322{
323 unsigned i;
324 tl_assert(vc->size <= vc->capacity);
325 for (i = 1; i < vc->size; i++)
326 {
327 tl_assert(vc->vc[i-1].threadid < vc->vc[i].threadid);
328 }
329}
330
331/**
332 * Change the size of the memory block pointed at by vc->vc.
333 * Changes capacity, but does not change size. If the size of the memory
334 * block is increased, the newly allocated memory is not initialized.
335 */
336static
bart41b226c2009-02-14 16:55:19 +0000337void DRD_(vc_reserve)(VectorClock* const vc, const unsigned new_capacity)
sewardjaf44c822007-11-25 14:01:38 +0000338{
339 tl_assert(vc);
340 if (new_capacity > vc->capacity)
341 {
342 if (vc->vc)
343 {
sewardj9c606bd2008-09-18 18:12:50 +0000344 vc->vc = VG_(realloc)("drd.vc.vr.1",
345 vc->vc, new_capacity * sizeof(vc->vc[0]));
sewardjaf44c822007-11-25 14:01:38 +0000346 }
347 else if (new_capacity > 0)
348 {
sewardj9c606bd2008-09-18 18:12:50 +0000349 vc->vc = VG_(malloc)("drd.vc.vr.2",
350 new_capacity * sizeof(vc->vc[0]));
sewardjaf44c822007-11-25 14:01:38 +0000351 }
352 else
353 {
354 tl_assert(vc->vc == 0 && new_capacity == 0);
355 }
356 vc->capacity = new_capacity;
357 }
358 tl_assert(new_capacity == 0 || vc->vc != 0);
359}
360
bart41b226c2009-02-14 16:55:19 +0000361#if 0
sewardjaf44c822007-11-25 14:01:38 +0000362/**
363 * Unit test.
364 */
bart41b226c2009-02-14 16:55:19 +0000365void DRD_(vc_test)(void)
sewardjaf44c822007-11-25 14:01:38 +0000366{
367 VectorClock vc1;
368 VCElem vc1elem[] = { { 3, 7 }, { 5, 8 }, };
369 VectorClock vc2;
370 VCElem vc2elem[] = { { 1, 4 }, { 3, 9 }, };
371 VectorClock vc3;
372 VCElem vc4elem[] = { { 1, 3 }, { 2, 1 }, };
373 VectorClock vc4;
374 VCElem vc5elem[] = { { 1, 4 }, };
375 VectorClock vc5;
376
377 vc_init(&vc1, vc1elem, sizeof(vc1elem)/sizeof(vc1elem[0]));
378 vc_init(&vc2, vc2elem, sizeof(vc2elem)/sizeof(vc2elem[0]));
379 vc_init(&vc3, 0, 0);
380 vc_init(&vc4, vc4elem, sizeof(vc4elem)/sizeof(vc4elem[0]));
381 vc_init(&vc5, vc5elem, sizeof(vc5elem)/sizeof(vc5elem[0]));
382
383 vc_combine(&vc3, &vc1);
384 vc_combine(&vc3, &vc2);
385
386 VG_(printf)("vc1: ");
387 vc_print(&vc1);
388 VG_(printf)("\nvc2: ");
389 vc_print(&vc2);
390 VG_(printf)("\nvc3: ");
391 vc_print(&vc3);
392 VG_(printf)("\n");
393 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));
394 vc_print(&vc4);
395 VG_(printf)(", ");
396 vc_print(&vc5);
397 VG_(printf)(") = %d sw %d\n", vc_lte(&vc4, &vc5), vc_lte(&vc5, &vc4));
398
399 vc_cleanup(&vc1);
400 vc_cleanup(&vc2);
401 vc_cleanup(&vc3);
402}
bart41b226c2009-02-14 16:55:19 +0000403#endif