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 |
| 42 | * other thread, the vector clock of the synchronization object and the |
| 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 | |
| 50 | #include "pub_tool_basics.h" // Addr, SizeT |
| 51 | |
| 52 | |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 53 | /** Vector clock element. */ |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 54 | typedef struct |
| 55 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 56 | DrdThreadId threadid; |
| 57 | UInt count; |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 58 | } VCElem; |
| 59 | |
| 60 | typedef struct |
| 61 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 62 | unsigned capacity; /**< number of elements allocated for array vc. */ |
| 63 | unsigned size; /**< number of elements used of array vc. */ |
| 64 | VCElem* vc; /**< vector clock elements. */ |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 65 | } VectorClock; |
| 66 | |
| 67 | |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 68 | void DRD_(vc_init)(VectorClock* const vc, |
| 69 | const VCElem* const vcelem, |
| 70 | const unsigned size); |
| 71 | void DRD_(vc_cleanup)(VectorClock* const vc); |
| 72 | void DRD_(vc_copy)(VectorClock* const new, const VectorClock* const rhs); |
| 73 | void DRD_(vc_assign)(VectorClock* const lhs, const VectorClock* const rhs); |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 74 | void DRD_(vc_increment)(VectorClock* const vc, DrdThreadId const tid); |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 75 | static __inline__ |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 76 | Bool DRD_(vc_lte)(const VectorClock* const vc1, |
| 77 | const VectorClock* const vc2); |
| 78 | Bool DRD_(vc_ordered)(const VectorClock* const vc1, |
| 79 | const VectorClock* const vc2); |
| 80 | void DRD_(vc_min)(VectorClock* const result, |
| 81 | const VectorClock* const rhs); |
| 82 | void DRD_(vc_combine)(VectorClock* const result, |
| 83 | const VectorClock* const rhs); |
| 84 | Bool DRD_(vc_combine2)(VectorClock* const result, |
| 85 | const VectorClock* const rhs, |
| 86 | const DrdThreadId tid); |
| 87 | void DRD_(vc_print)(const VectorClock* const vc); |
| 88 | void DRD_(vc_snprint)(Char* const str, const Int size, |
| 89 | const VectorClock* const vc); |
| 90 | void DRD_(vc_check)(const VectorClock* const vc); |
| 91 | void DRD_(vc_test)(void); |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 92 | |
| 93 | |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 94 | |
| 95 | /** |
| 96 | * @return True if all thread id's that are present in vc1 also exist in |
| 97 | * vc2, and if additionally all corresponding counters in v2 are higher or |
| 98 | * equal. |
| 99 | */ |
| 100 | static __inline__ |
bart | 41b226c | 2009-02-14 16:55:19 +0000 | [diff] [blame] | 101 | Bool DRD_(vc_lte)(const VectorClock* const vc1, const VectorClock* const vc2) |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 102 | { |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 103 | unsigned i; |
| 104 | unsigned j = 0; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 105 | |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 106 | for (i = 0; i < vc1->size; i++) |
| 107 | { |
| 108 | while (j < vc2->size && vc2->vc[j].threadid < vc1->vc[i].threadid) |
| 109 | { |
| 110 | j++; |
| 111 | } |
| 112 | if (j >= vc2->size || vc2->vc[j].threadid > vc1->vc[i].threadid) |
| 113 | return False; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 114 | #ifdef ENABLE_DRD_CONSISTENCY_CHECKS |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 115 | /* This assert statement has been commented out because of performance */ |
| 116 | /* reasons.*/ |
| 117 | tl_assert(j < vc2->size && vc2->vc[j].threadid == vc1->vc[i].threadid); |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 118 | #endif |
bart | bedfd23 | 2009-03-26 19:07:15 +0000 | [diff] [blame^] | 119 | if (vc1->vc[i].count > vc2->vc[j].count) |
| 120 | return False; |
| 121 | } |
| 122 | return True; |
bart | fa1b293 | 2008-06-22 13:05:00 +0000 | [diff] [blame] | 123 | } |
| 124 | |
| 125 | |
sewardj | af44c82 | 2007-11-25 14:01:38 +0000 | [diff] [blame] | 126 | #endif /* __DRD_VC_H */ |