helgrind/libhb.h

   1
   2 /*--------------------------------------------------------------------*/
   3 /*--- LibHB: a library for implementing and checking               ---*/
   4 /*--- the happens-before relationship in concurrent programs.      ---*/
   5 /*---                                                 libhb_main.c ---*/
   6 /*--------------------------------------------------------------------*/
   7
   8 /*
   9    This file is part of LibHB, a library for implementing and checking
  10    the happens-before relationship in concurrent programs.
  11
  12    Copyright (C) 2008-2017 OpenWorks Ltd
  13       info@open-works.co.uk
  14
  15    This program is free software; you can redistribute it and/or
  16    modify it under the terms of the GNU General Public License as
  17    published by the Free Software Foundation; either version 2 of the
  18    License, or (at your option) any later version.
  19
  20    This program is distributed in the hope that it will be useful, but
  21    WITHOUT ANY WARRANTY; without even the implied warranty of
  22    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  23    General Public License for more details.
  24
  25    You should have received a copy of the GNU General Public License
  26    along with this program; if not, see <http://www.gnu.org/licenses/>.
  27
  28    The GNU General Public License is contained in the file COPYING.
  29 */
  30
  31 #ifndef __LIBHB_H
  32 #define __LIBHB_H
  33
  34 /* Abstract to user: thread identifiers */
  35 /* typedef  struct _Thr  Thr; */ /* now in hg_lock_n_thread.h */
  36
  37 /* Abstract to user: synchronisation objects */
  38 /* typedef  struct _SO  SO; */ /* now in hg_lock_n_thread.h */
  39
  40 /* Initialise library; returns Thr* for root thread.  'shadow_alloc'
  41    should never return NULL, instead it should simply not return if
  42    they encounter an out-of-memory condition. */
  43 Thr* libhb_init (
  44         void        (*get_stacktrace)( Thr*, Addr*, UWord ),
  45         ExeContext* (*get_EC)( Thr* )
  46      );
  47
  48 /* Shut down the library, and print stats (in fact that's _all_
  49    this is for.) */
  50 void libhb_shutdown ( Bool show_stats );
  51
  52 /* Thread creation: returns Thr* for new thread */
  53 Thr* libhb_create ( Thr* parent );
  54
  55 /* Thread async exit */
  56 void libhb_async_exit      ( Thr* exitter );
  57 void libhb_joinedwith_done ( Thr* exitter );
  58
  59 /* Synchronisation objects (abstract to caller) */
  60
  61 /* Allocate a new one (alloc'd by library) */
  62 SO* libhb_so_alloc ( void );
  63
  64 /* Dealloc one */
  65 void libhb_so_dealloc ( SO* so );
  66
  67 /* Send a message via a sync object.  If strong_send is true, the
  68    resulting inter-thread dependency seen by a future receiver of this
  69    message will be a dependency on this thread only.  That is, in a
  70    strong send, the VC inside the SO is replaced by the clock of the
  71    sending thread.  For a weak send, the sender's VC is joined into
  72    that already in the SO, if any.  This subtlety is needed to model
  73    rwlocks: a strong send corresponds to releasing a rwlock that had
  74    been w-held (or releasing a standard mutex).  A weak send
  75    corresponds to releasing a rwlock that has been r-held.
  76
  77    (rationale): Since in general many threads may hold a rwlock in
  78    r-mode, a weak send facility is necessary in order that the final
  79    SO reflects the join of the VCs of all the threads releasing the
  80    rwlock, rather than merely holding the VC of the most recent thread
  81    to release it. */
  82 void libhb_so_send ( Thr* thr, SO* so, Bool strong_send );
  83
  84 /* Recv a message from a sync object.  If strong_recv is True, the
  85    resulting inter-thread dependency is considered adequate to induce
  86    a h-b ordering on both reads and writes.  If it is False, the
  87    implied h-b ordering exists only for reads, not writes.  This is
  88    subtlety is required in order to support reader-writer locks: a
  89    thread doing a write-acquire of a rwlock (or acquiring a normal
  90    mutex) models this by doing a strong receive.  A thread doing a
  91    read-acquire of a rwlock models this by doing a !strong_recv. */
  92 void libhb_so_recv ( Thr* thr, SO* so, Bool strong_recv );
  93
  94 /* Has this SO ever been sent on? */
  95 Bool libhb_so_everSent ( SO* so );
  96
  97 /* Memory accesses (1/2/4/8 byte size).  They report a race if one is
  98    found. */
  99 #define LIBHB_CWRITE_1(_thr,_a)    zsm_sapply08_f__msmcwrite((_thr),(_a))
 100 #define LIBHB_CWRITE_2(_thr,_a)    zsm_sapply16_f__msmcwrite((_thr),(_a))
 101 #define LIBHB_CWRITE_4(_thr,_a)    zsm_sapply32_f__msmcwrite((_thr),(_a))
 102 #define LIBHB_CWRITE_8(_thr,_a)    zsm_sapply64_f__msmcwrite((_thr),(_a))
 103 #define LIBHB_CWRITE_N(_thr,_a,_n) zsm_sapplyNN_f__msmcwrite((_thr),(_a),(_n))
 104
 105 #define LIBHB_CREAD_1(_thr,_a)    zsm_sapply08_f__msmcread((_thr),(_a))
 106 #define LIBHB_CREAD_2(_thr,_a)    zsm_sapply16_f__msmcread((_thr),(_a))
 107 #define LIBHB_CREAD_4(_thr,_a)    zsm_sapply32_f__msmcread((_thr),(_a))
 108 #define LIBHB_CREAD_8(_thr,_a)    zsm_sapply64_f__msmcread((_thr),(_a))
 109 #define LIBHB_CREAD_N(_thr,_a,_n) zsm_sapplyNN_f__msmcread((_thr),(_a),(_n))
 110
 111 void zsm_sapply08_f__msmcwrite ( Thr* thr, Addr a );
 112 void zsm_sapply16_f__msmcwrite ( Thr* thr, Addr a );
 113 void zsm_sapply32_f__msmcwrite ( Thr* thr, Addr a );
 114 void zsm_sapply64_f__msmcwrite ( Thr* thr, Addr a );
 115 void zsm_sapplyNN_f__msmcwrite ( Thr* thr, Addr a, SizeT len );
 116
 117 void zsm_sapply08_f__msmcread ( Thr* thr, Addr a );
 118 void zsm_sapply16_f__msmcread ( Thr* thr, Addr a );
 119 void zsm_sapply32_f__msmcread ( Thr* thr, Addr a );
 120 void zsm_sapply64_f__msmcread ( Thr* thr, Addr a );
 121 void zsm_sapplyNN_f__msmcread ( Thr* thr, Addr a, SizeT len );
 122
 123 void libhb_Thr_resumes ( Thr* thr );
 124
 125 /* Set memory address ranges to new (freshly allocated), or noaccess
 126    (no longer accessible).  NB: "AHAE" == "Actually Has An Effect" :-) */
 127 void libhb_srange_new      ( Thr*, Addr, SizeT );
 128 void libhb_srange_untrack  ( Thr*, Addr, SizeT );
 129 void libhb_srange_noaccess_NoFX ( Thr*, Addr, SizeT ); /* IS IGNORED */
 130 void libhb_srange_noaccess_AHAE ( Thr*, Addr, SizeT ); /* IS NOT IGNORED */
 131
 132 /* Counts the nr of bytes addressable in the range [a, a+len[
 133    (so a+len excluded) and returns the nr of addressable bytes found.
 134    If abits /= NULL, abits must point to a block of memory of length len.
 135    In this array, each addressable byte will be indicated with 0xff.
 136    Non-addressable bytes are indicated with 0x00. */
 137 UWord libhb_srange_get_abits (Addr a, /*OUT*/UChar *abits, SizeT len);
 138
 139 /* Get and set the hgthread (pointer to corresponding Thread
 140    structure). */
 141 Thread* libhb_get_Thr_hgthread ( Thr* );
 142 void    libhb_set_Thr_hgthread ( Thr*, Thread* );
 143
 144 /* Low level copy of shadow state from [src,src+len) to [dst,dst+len).
 145    Overlapping moves are checked for and asserted against. */
 146 void libhb_copy_shadow_state ( Thr* thr, Addr src, Addr dst, SizeT len );
 147
 148 /* Call this periodically to give libhb the opportunity to
 149    garbage-collect its internal data structures. */
 150 void libhb_maybe_GC ( void );
 151
 152 /* Extract info from the conflicting-access machinery. */
 153 Bool libhb_event_map_lookup ( /*OUT*/ExeContext** resEC,
 154                               /*OUT*/Thr**        resThr,
 155                               /*OUT*/SizeT*       resSzB,
 156                               /*OUT*/Bool*        resIsW,
 157                               /*OUT*/WordSetID*   locksHeldW,
 158                               Thr* thr, Addr a, SizeT szB, Bool isW );
 159
 160 typedef void (*Access_t) (StackTrace ips, UInt n_ips,
 161                           Thr*  Thr_a,
 162                           Addr  ga,
 163                           SizeT SzB,
 164                           Bool  isW,
 165                           WordSetID locksHeldW );
 166 /* Call fn for each recorded access history that overlaps with range [a, a+szB[.
 167    fn is first called for oldest access.*/
 168 void libhb_event_map_access_history ( Addr a, SizeT szB, Access_t fn );
 169
 170 /* ------ Exported from hg_main.c ------ */
 171 /* Yes, this is a horrible tangle.  Sigh. */
 172
 173 /* Get the univ_lset (universe for locksets) from hg_main.c.  Sigh. */
 174 WordSetU* HG_(get_univ_lsets) ( void );
 175
 176 /* Get the the header pointer for the double linked list of locks
 177    (admin_locks). */
 178 Lock* HG_(get_admin_locks) ( void );
 179
 180 #endif /* __LIBHB_H */
 181
 182 /*--------------------------------------------------------------------*/
 183 /*--- end                                                  libhb.h ---*/
 184 /*--------------------------------------------------------------------*/