1b32f58018498ea2225959b0ba11c18f0c433deefEvgeniy Stepanov/* -*- mode: C; c-basic-offset: 3; indent-tabs-mode: nil; -*- */
2ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown/*
3ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  This file is part of drd, a thread error detector.
4ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
5b32f58018498ea2225959b0ba11c18f0c433deefEvgeniy Stepanov  Copyright (C) 2006-2011 Bart Van Assche <bvanassche@acm.org>.
6ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
7ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  This program is free software; you can redistribute it and/or
8ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  modify it under the terms of the GNU General Public License as
9ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  published by the Free Software Foundation; either version 2 of the
10ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  License, or (at your option) any later version.
11ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
12ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  This program is distributed in the hope that it will be useful, but
13ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  WITHOUT ANY WARRANTY; without even the implied warranty of
14ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
15ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  General Public License for more details.
16ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
17ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  You should have received a copy of the GNU General Public License
18ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  along with this program; if not, write to the Free Software
19ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
20ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  02111-1307, USA.
21ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
22ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown  The GNU General Public License is contained in the file COPYING.
23ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown*/
24ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
25ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
26ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#ifndef __DRD_VC_H
27ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#define __DRD_VC_H
28ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
29ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
30ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown/*
31ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * DRD vector clock implementation:
32ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - One counter per thread.
33ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - A vector clock is implemented as multiple pairs of (thread id, counter).
34ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - Pairs are stored in an array sorted by thread id.
35ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *
36ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * Semantics:
37ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - Each time a thread performs an action that implies an ordering between
38ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   intra-thread events, the counter of that thread is incremented.
39ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - Vector clocks are compared by comparing all counters of all threads.
40ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - When a thread synchronization action is performed that guarantees that
41ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   new actions of the current thread are executed after the actions of the
42ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   other thread, the vector clock of the synchronization object and the
43ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   current thread are combined (by taking the component-wise maximum).
44ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * - A vector clock is incremented during actions such as
45ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   pthread_create(), pthread_mutex_unlock(), sem_post(). (Actions where
46ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *   an inter-thread ordering "arrow" starts).
47ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown */
48ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
49ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
50ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#include "pub_tool_basics.h"     /* Addr, SizeT */
51ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#include "drd_basics.h"          /* DrdThreadId */
52ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#include "pub_tool_libcassert.h" /* tl_assert() */
53ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
54ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
55ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#define VC_PREALLOCATED 8
56ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
57ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
58ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown/** Vector clock element. */
59ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Browntypedef struct
60ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown{
61ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   DrdThreadId threadid;
62ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   UInt        count;
63ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown} VCElem;
64ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
65ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Browntypedef struct
66ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown{
67ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   unsigned capacity; /**< number of elements allocated for array vc. */
68ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   unsigned size;     /**< number of elements used of array vc. */
69ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   VCElem*  vc;       /**< vector clock elements. */
70ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   VCElem   preallocated[VC_PREALLOCATED];
71ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown} VectorClock;
72ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
73ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
74ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_init)(VectorClock* const vc,
75ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                   const VCElem* const vcelem,
76ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                   const unsigned size);
77ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_cleanup)(VectorClock* const vc);
78ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_copy)(VectorClock* const new, const VectorClock* const rhs);
79ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_assign)(VectorClock* const lhs, const VectorClock* const rhs);
80ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_increment)(VectorClock* const vc, DrdThreadId const tid);
81ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownstatic __inline__
82ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff BrownBool DRD_(vc_lte)(const VectorClock* const vc1,
83ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                  const VectorClock* const vc2);
84ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff BrownBool DRD_(vc_ordered)(const VectorClock* const vc1,
85ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                      const VectorClock* const vc2);
86ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_min)(VectorClock* const result,
87ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                  const VectorClock* const rhs);
88ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_combine)(VectorClock* const result,
89ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown                      const VectorClock* const rhs);
90ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_print)(const VectorClock* const vc);
91ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownchar* DRD_(vc_aprint)(const VectorClock* const vc);
92ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_check)(const VectorClock* const vc);
93ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownvoid DRD_(vc_test)(void);
94ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
95ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
96ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
97ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown/**
98ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown * @return True if all thread id's that are present in vc1 also exist in
99ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *    vc2, and if additionally all corresponding counters in v2 are higher or
100ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown *    equal.
101ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown */
102ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brownstatic __inline__
103ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff BrownBool DRD_(vc_lte)(const VectorClock* const vc1, const VectorClock* const vc2)
104ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown{
105ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   unsigned i;
106ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   unsigned j = 0;
107ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
108ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   for (i = 0; i < vc1->size; i++)
109ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   {
110ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown      while (j < vc2->size && vc2->vc[j].threadid < vc1->vc[i].threadid)
111ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown         j++;
112ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown      if (j >= vc2->size || vc2->vc[j].threadid > vc1->vc[i].threadid)
113ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown         return False;
114ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#ifdef ENABLE_DRD_CONSISTENCY_CHECKS
115ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown      /*
116ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown       * This assert statement has been commented out because of performance
117ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown       * reasons.
118ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown       */
119ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown      tl_assert(j < vc2->size && vc2->vc[j].threadid == vc1->vc[i].threadid);
120ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#endif
121ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown      if (vc1->vc[i].count > vc2->vc[j].count)
122ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown         return False;
123ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   }
124ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown   return True;
125ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown}
126ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
127ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown
128ed07e00d438c74b7a23c01bfffde77e3968305e4Jeff Brown#endif /* __DRD_VC_H */
129