bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 1 | /* -*- mode: C; c-basic-offset: 3; -*- */ |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 2 | /* |
bart | 86562bd | 2009-02-16 19:43:56 +0000 | [diff] [blame] | 3 | This file is part of drd, a thread error detector. |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 4 | |
bart | 86562bd | 2009-02-16 19:43:56 +0000 | [diff] [blame] | 5 | Copyright (C) 2006-2009 Bart Van Assche <bart.vanassche@gmail.com>. |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 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 | #ifndef __DRD_VC_H |
| 27 | #define __DRD_VC_H |
| 28 | |
| 29 | |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 30 | /* |
| 31 | * DRD vector clock implementation: |
| 32 | * - One counter per thread. |
| 33 | * - A vector clock is implemented as multiple pairs of (thread id, counter). |
| 34 | * - Pairs are stored in an array sorted by thread id. |
| 35 | * |
| 36 | * Semantics: |
| 37 | * - Each time a thread performs an action that implies an ordering between |
| 38 | * intra-thread events, the counter of that thread is incremented. |
| 39 | * - Vector clocks are compared by comparing all counters of all threads. |
| 40 | * - When a thread synchronization action is performed that guarantees that |
| 41 | * new actions of the current thread are executed after the actions of the |
bart | 31b983d | 2010-02-21 14:52:59 +0000 | [diff] [blame] | 42 | * other thread, the vector clock of the synchronization object and the |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 43 | * current thread are combined (by taking the component-wise maximum). |
| 44 | * - A vector clock is incremented during actions such as |
| 45 | * pthread_create(), pthread_mutex_unlock(), sem_post(). (Actions where |
| 46 | * an inter-thread ordering "arrow" starts). |
| 47 | */ |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 48 | |
| 49 | |
bart | 8f822af | 2009-06-08 18:20:42 +0000 | [diff] [blame] | 50 | #include "pub_tool_basics.h" /* Addr, SizeT */ |
| 51 | #include "drd_basics.h" /* DrdThreadId */ |
| 52 | #include "pub_tool_libcassert.h" /* tl_assert() */ |
| 53 | |
| 54 | |
| 55 | #define VC_PREALLOCATED 8 |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 56 | |
| 57 | |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 58 | /** Vector clock element. */ |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 59 | typedef struct |
| 60 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 61 | DrdThreadId threadid; |
| 62 | UInt count; |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 63 | } VCElem; |
| 64 | |
| 65 | typedef struct |
| 66 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 67 | unsigned capacity; /**< number of elements allocated for array vc. */ |
| 68 | unsigned size; /**< number of elements used of array vc. */ |
| 69 | VCElem* vc; /**< vector clock elements. */ |
bart | 8f822af | 2009-06-08 18:20:42 +0000 | [diff] [blame] | 70 | VCElem preallocated[VC_PREALLOCATED]; |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 71 | } VectorClock; |
| 72 | |
| 73 | |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 74 | void DRD_(vc_init)(VectorClock* const vc, |
| 75 | const VCElem* const vcelem, |
| 76 | const unsigned size); |
| 77 | void DRD_(vc_cleanup)(VectorClock* const vc); |
| 78 | void DRD_(vc_copy)(VectorClock* const new, const VectorClock* const rhs); |
| 79 | void DRD_(vc_assign)(VectorClock* const lhs, const VectorClock* const rhs); |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 80 | void DRD_(vc_increment)(VectorClock* const vc, DrdThreadId const tid); |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 81 | static __inline__ |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 82 | Bool DRD_(vc_lte)(const VectorClock* const vc1, |
| 83 | const VectorClock* const vc2); |
| 84 | Bool DRD_(vc_ordered)(const VectorClock* const vc1, |
| 85 | const VectorClock* const vc2); |
| 86 | void DRD_(vc_min)(VectorClock* const result, |
| 87 | const VectorClock* const rhs); |
| 88 | void DRD_(vc_combine)(VectorClock* const result, |
| 89 | const VectorClock* const rhs); |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 90 | void DRD_(vc_print)(const VectorClock* const vc); |
bart | 8f822af | 2009-06-08 18:20:42 +0000 | [diff] [blame] | 91 | char* DRD_(vc_aprint)(const VectorClock* const vc); |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 92 | void DRD_(vc_check)(const VectorClock* const vc); |
| 93 | void DRD_(vc_test)(void); |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 94 | |
| 95 | |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 96 | |
| 97 | /** |
| 98 | * @return True if all thread id's that are present in vc1 also exist in |
| 99 | * vc2, and if additionally all corresponding counters in v2 are higher or |
| 100 | * equal. |
| 101 | */ |
| 102 | static __inline__ |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 103 | Bool DRD_(vc_lte)(const VectorClock* const vc1, const VectorClock* const vc2) |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 104 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 105 | unsigned i; |
| 106 | unsigned j = 0; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 107 | |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 108 | for (i = 0; i < vc1->size; i++) |
| 109 | { |
| 110 | while (j < vc2->size && vc2->vc[j].threadid < vc1->vc[i].threadid) |
| 111 | { |
| 112 | j++; |
| 113 | } |
| 114 | if (j >= vc2->size || vc2->vc[j].threadid > vc1->vc[i].threadid) |
| 115 | return False; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 116 | #ifdef ENABLE_DRD_CONSISTENCY_CHECKS |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 117 | /* This assert statement has been commented out because of performance */ |
| 118 | /* reasons.*/ |
| 119 | tl_assert(j < vc2->size && vc2->vc[j].threadid == vc1->vc[i].threadid); |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 120 | #endif |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame] | 121 | if (vc1->vc[i].count > vc2->vc[j].count) |
| 122 | return False; |
| 123 | } |
| 124 | return True; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 125 | } |
| 126 | |
| 127 | |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 128 | #endif /* __DRD_VC_H */ |