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