| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 1 | /* | 
| bart | 86562bd | 2009-02-16 19:43:56 +0000 | [diff] [blame^] | 2 |   This file is part of drd, a thread error detector. | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 3 |  | 
| bart | 86562bd | 2009-02-16 19:43:56 +0000 | [diff] [blame^] | 4 |   Copyright (C) 2006-2009 Bart Van Assche <bart.vanassche@gmail.com>. | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 5 |  | 
 | 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() | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 28 | #include "pub_tool_libcbase.h"    // VG_(memcpy) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 29 | #include "pub_tool_libcprint.h"   // VG_(printf) | 
 | 30 | #include "pub_tool_mallocfree.h"  // VG_(malloc), VG_(free) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 31 |  | 
 | 32 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 33 | /* Local function declarations. */ | 
 | 34 |  | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 35 | static | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 36 | void DRD_(vc_reserve)(VectorClock* const vc, const unsigned new_capacity); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 37 |  | 
 | 38 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 39 | /* 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 |  */ | 
 | 46 | void DRD_(vc_init)(VectorClock* const vc, | 
 | 47 |                    const VCElem* const vcelem, | 
 | 48 |                    const unsigned size) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 49 | { | 
 | 50 |   tl_assert(vc); | 
 | 51 |   vc->size = 0; | 
 | 52 |   vc->capacity = 0; | 
 | 53 |   vc->vc = 0; | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 54 |   DRD_(vc_reserve)(vc, size); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 55 |   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 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 63 | /** Reset vc to the empty vector clock. */ | 
 | 64 | void DRD_(vc_cleanup)(VectorClock* const vc) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 65 | { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 66 |   DRD_(vc_reserve)(vc, 0); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 67 | } | 
 | 68 |  | 
| bart | c46c232 | 2008-02-24 18:26:46 +0000 | [diff] [blame] | 69 | /** Copy constructor -- initializes *new. */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 70 | void DRD_(vc_copy)(VectorClock* const new, const VectorClock* const rhs) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 71 | { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 72 |   DRD_(vc_init)(new, rhs->vc, rhs->size); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 73 | } | 
 | 74 |  | 
| bart | c46c232 | 2008-02-24 18:26:46 +0000 | [diff] [blame] | 75 | /** Assignment operator -- *lhs is already a valid vector clock. */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 76 | void DRD_(vc_assign)(VectorClock* const lhs, const VectorClock* const rhs) | 
| bart | c46c232 | 2008-02-24 18:26:46 +0000 | [diff] [blame] | 77 | { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 78 |   DRD_(vc_cleanup)(lhs); | 
 | 79 |   DRD_(vc_copy)(lhs, rhs); | 
| bart | c46c232 | 2008-02-24 18:26:46 +0000 | [diff] [blame] | 80 | } | 
 | 81 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 82 | /** Increment the clock of thread 'tid' in vector clock 'vc'. */ | 
 | 83 | void DRD_(vc_increment)(VectorClock* const vc, DrdThreadId const tid) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 84 | { | 
 | 85 |   unsigned i; | 
 | 86 |   for (i = 0; i < vc->size; i++) | 
 | 87 |   { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 88 |     if (vc->vc[i].threadid == tid) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 89 |     { | 
 | 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 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 98 |   /* | 
 | 99 |    * The specified thread ID does not yet exist in the vector clock | 
 | 100 |    * -- insert it. | 
 | 101 |    */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 102 |   { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 103 |     const VCElem vcelem = { tid, 1 }; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 104 |     VectorClock vc2; | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 105 |     DRD_(vc_init)(&vc2, &vcelem, 1); | 
 | 106 |     DRD_(vc_combine)(vc, &vc2); | 
 | 107 |     DRD_(vc_cleanup)(&vc2); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 108 |   } | 
 | 109 | } | 
 | 110 |  | 
 | 111 | /** | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 112 |  * @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 |  */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 115 | Bool DRD_(vc_ordered)(const VectorClock* const vc1, | 
 | 116 |                       const VectorClock* const vc2) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 117 | { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 118 |   return DRD_(vc_lte)(vc1, vc2) || DRD_(vc_lte)(vc2, vc1); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 119 | } | 
 | 120 |  | 
| bart | 5bd9f2d | 2008-03-03 20:31:58 +0000 | [diff] [blame] | 121 | /** Compute elementwise minimum. */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 122 | void DRD_(vc_min)(VectorClock* const result, const VectorClock* const rhs) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 123 | { | 
 | 124 |   unsigned i; | 
 | 125 |   unsigned j; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 126 |  | 
 | 127 |   tl_assert(result); | 
 | 128 |   tl_assert(rhs); | 
 | 129 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 130 |   DRD_(vc_check)(result); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 131 |  | 
| bart | 5bd9f2d | 2008-03-03 20:31:58 +0000 | [diff] [blame] | 132 |   /* Next, combine both vector clocks into one. */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 133 |   i = 0; | 
 | 134 |   for (j = 0; j < rhs->size; j++) | 
 | 135 |   { | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 136 |     while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid) | 
| bart | 5bd9f2d | 2008-03-03 20:31:58 +0000 | [diff] [blame] | 137 |     { | 
 | 138 |       /* Thread ID is missing in second vector clock. Clear the count. */ | 
 | 139 |       result->vc[i].count = 0; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 140 |       i++; | 
| bart | 5bd9f2d | 2008-03-03 20:31:58 +0000 | [diff] [blame] | 141 |     } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 142 |     if (i >= result->size) | 
 | 143 |     { | 
| bart | a7faf67 | 2008-03-06 18:02:37 +0000 | [diff] [blame] | 144 |       break; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 145 |     } | 
| bart | a7faf67 | 2008-03-06 18:02:37 +0000 | [diff] [blame] | 146 |     if (result->vc[i].threadid <= rhs->vc[j].threadid) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 147 |     { | 
| bart | 5bd9f2d | 2008-03-03 20:31:58 +0000 | [diff] [blame] | 148 |       /* The thread ID is present in both vector clocks. Compute the minimum */ | 
 | 149 |       /* of vc[i].count and vc[j].count. */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 150 |       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 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 155 |     } | 
 | 156 |   } | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 157 |   DRD_(vc_check)(result); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 158 | } | 
 | 159 |  | 
 | 160 | /** | 
 | 161 |  * Compute elementwise maximum. | 
 | 162 |  */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 163 | void DRD_(vc_combine)(VectorClock* const result, const VectorClock* const rhs) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 164 | { | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 165 |   DRD_(vc_combine2)(result, rhs, -1); | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 166 | } | 
 | 167 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 168 | /** | 
 | 169 |  * Compute elementwise maximum. | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 170 |  * | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 171 |  * @return True if *result and *rhs are equal, or if *result and *rhs only | 
 | 172 |  *         differ in the component with thread ID tid. | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 173 |  */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 174 | Bool DRD_(vc_combine2)(VectorClock* const result, | 
 | 175 |                        const VectorClock* const rhs, | 
 | 176 |                        const DrdThreadId tid) | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 177 | { | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 178 |   unsigned i; | 
 | 179 |   unsigned j; | 
 | 180 |   unsigned shared; | 
 | 181 |   unsigned new_size; | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 182 |   Bool     almost_equal = True; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 183 |  | 
 | 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 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 200 |   DRD_(vc_check)(result); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 201 |  | 
 | 202 |   new_size = result->size + rhs->size - shared; | 
 | 203 |   if (new_size > result->capacity) | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 204 |     DRD_(vc_reserve)(result, new_size); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 205 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 206 |   DRD_(vc_check)(result); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 207 |  | 
 | 208 |   // Next, combine both vector clocks into one. | 
 | 209 |   i = 0; | 
 | 210 |   for (j = 0; j < rhs->size; j++) | 
 | 211 |   { | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 212 |     /* First of all, skip those clocks in result->vc[] for which there */ | 
 | 213 |     /* is no corresponding clock in rhs->vc[].                         */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 214 |     while (i < result->size && result->vc[i].threadid < rhs->vc[j].threadid) | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 215 |     { | 
 | 216 |       if (result->vc[i].threadid != tid) | 
 | 217 |       { | 
 | 218 |         almost_equal = False; | 
 | 219 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 220 |       i++; | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 221 |     } | 
 | 222 |     /* If the end of *result is met, append rhs->vc[j] to *result. */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 223 |     if (i >= result->size) | 
 | 224 |     { | 
 | 225 |       result->size++; | 
 | 226 |       result->vc[i] = rhs->vc[j]; | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 227 |       if (result->vc[i].threadid != tid) | 
 | 228 |       { | 
 | 229 |         almost_equal = False; | 
 | 230 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 231 |     } | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 232 |     /* If clock rhs->vc[j] is not in *result, insert it. */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 233 |     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]; | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 242 |       if (result->vc[i].threadid != tid) | 
 | 243 |       { | 
 | 244 |         almost_equal = False; | 
 | 245 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 246 |     } | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 247 |     /* Otherwise, both *result and *rhs have a clock for thread            */ | 
 | 248 |     /* result->vc[i].threadid == rhs->vc[j].threadid. Compute the maximum. */ | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 249 |     else | 
 | 250 |     { | 
 | 251 |       tl_assert(result->vc[i].threadid == rhs->vc[j].threadid); | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 252 |       if (result->vc[i].threadid != tid | 
 | 253 |           && rhs->vc[j].count != result->vc[i].count) | 
 | 254 |       { | 
 | 255 |         almost_equal = False; | 
 | 256 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 257 |       if (rhs->vc[j].count > result->vc[i].count) | 
 | 258 |       { | 
 | 259 |         result->vc[i].count = rhs->vc[j].count; | 
 | 260 |       } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 261 |     } | 
 | 262 |   } | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 263 |   DRD_(vc_check)(result); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 264 |   tl_assert(result->size == new_size); | 
| bart | fbbac09 | 2008-04-06 14:57:37 +0000 | [diff] [blame] | 265 |  | 
 | 266 |   return almost_equal; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 267 | } | 
 | 268 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 269 | /** Print the contents of vector clock 'vc'. */ | 
 | 270 | void DRD_(vc_print)(const VectorClock* const vc) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 271 | { | 
 | 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 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 285 | /** | 
 | 286 |  * Print the contents of vector clock 'vc' to the character array 'str' that | 
 | 287 |  * has 'size' elements. | 
 | 288 |  */ | 
 | 289 | void DRD_(vc_snprint)(Char* const str, const Int size, | 
 | 290 |                       const VectorClock* const vc) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 291 | { | 
 | 292 |   unsigned i; | 
| bart | fdb6558 | 2008-04-06 13:03:49 +0000 | [diff] [blame] | 293 |   unsigned j = 1; | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 294 |  | 
 | 295 |   tl_assert(vc); | 
 | 296 |   VG_(snprintf)(str, size, "["); | 
 | 297 |   for (i = 0; i < vc->size; i++) | 
 | 298 |   { | 
 | 299 |     tl_assert(vc->vc); | 
| bart | fdb6558 | 2008-04-06 13:03:49 +0000 | [diff] [blame] | 300 |     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 |     } | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 307 |   } | 
 | 308 |   VG_(snprintf)(str + VG_(strlen)(str), size - VG_(strlen)(str), " ]"); | 
 | 309 | } | 
 | 310 |  | 
 | 311 | /** | 
 | 312 |  * Invariant test. | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 313 |  * | 
 | 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. | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 320 |  */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 321 | void DRD_(vc_check)(const VectorClock* const vc) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 322 | { | 
 | 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 |  */ | 
 | 336 | static | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 337 | void DRD_(vc_reserve)(VectorClock* const vc, const unsigned new_capacity) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 338 | { | 
 | 339 |   tl_assert(vc); | 
 | 340 |   if (new_capacity > vc->capacity) | 
 | 341 |   { | 
 | 342 |     if (vc->vc) | 
 | 343 |     { | 
| sewardj | 9c606bd | 2008-09-18 18:12:50 +0000 | [diff] [blame] | 344 |       vc->vc = VG_(realloc)("drd.vc.vr.1", | 
 | 345 |                             vc->vc, new_capacity * sizeof(vc->vc[0])); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 346 |     } | 
 | 347 |     else if (new_capacity > 0) | 
 | 348 |     { | 
| sewardj | 9c606bd | 2008-09-18 18:12:50 +0000 | [diff] [blame] | 349 |       vc->vc = VG_(malloc)("drd.vc.vr.2", | 
 | 350 |                            new_capacity * sizeof(vc->vc[0])); | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 351 |     } | 
 | 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 |  | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 361 | #if 0 | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 362 | /** | 
 | 363 |  * Unit test. | 
 | 364 |  */ | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 365 | void DRD_(vc_test)(void) | 
| sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 366 | { | 
 | 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 | } | 
| bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 403 | #endif |