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 | 03f8d3f | 2012-08-05 15:46:46 +0000 | [diff] [blame] | 12 | Copyright (C) 2008-2012 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 | |
sewardj | 6062664 | 2011-03-10 15:14:37 +0000 | [diff] [blame] | 134 | /* Get and set the hgthread (pointer to corresponding Thread |
| 135 | structure). */ |
sewardj | 0b20a15 | 2011-03-10 21:34:21 +0000 | [diff] [blame] | 136 | Thread* libhb_get_Thr_hgthread ( Thr* ); |
| 137 | void libhb_set_Thr_hgthread ( Thr*, Thread* ); |
sewardj | f98e1c0 | 2008-10-25 16:22:41 +0000 | [diff] [blame] | 138 | |
| 139 | /* Low level copy of shadow state from [src,src+len) to [dst,dst+len). |
| 140 | Overlapping moves are checked for and asserted against. */ |
sewardj | 23f1200 | 2009-07-24 08:45:08 +0000 | [diff] [blame] | 141 | void libhb_copy_shadow_state ( Thr* thr, Addr src, Addr dst, SizeT len ); |
sewardj | f98e1c0 | 2008-10-25 16:22:41 +0000 | [diff] [blame] | 142 | |
| 143 | /* Call this periodically to give libhb the opportunity to |
| 144 | garbage-collect its internal data structures. */ |
| 145 | void libhb_maybe_GC ( void ); |
| 146 | |
sewardj | c5ea996 | 2008-12-07 01:41:46 +0000 | [diff] [blame] | 147 | /* Extract info from the conflicting-access machinery. */ |
| 148 | Bool libhb_event_map_lookup ( /*OUT*/ExeContext** resEC, |
sewardj | ffce815 | 2011-06-24 10:09:41 +0000 | [diff] [blame] | 149 | /*OUT*/Thr** resThr, |
| 150 | /*OUT*/SizeT* resSzB, |
| 151 | /*OUT*/Bool* resIsW, |
| 152 | /*OUT*/WordSetID* locksHeldW, |
sewardj | c5ea996 | 2008-12-07 01:41:46 +0000 | [diff] [blame] | 153 | Thr* thr, Addr a, SizeT szB, Bool isW ); |
| 154 | |
sewardj | ffce815 | 2011-06-24 10:09:41 +0000 | [diff] [blame] | 155 | /* ------ Exported from hg_main.c ------ */ |
| 156 | /* Yes, this is a horrible tangle. Sigh. */ |
| 157 | |
| 158 | /* Get the univ_lset (universe for locksets) from hg_main.c. Sigh. */ |
| 159 | WordSetU* HG_(get_univ_lsets) ( void ); |
| 160 | |
| 161 | /* Get the the header pointer for the double linked list of locks |
| 162 | (admin_locks). */ |
| 163 | Lock* HG_(get_admin_locks) ( void ); |
| 164 | |
sewardj | f98e1c0 | 2008-10-25 16:22:41 +0000 | [diff] [blame] | 165 | #endif /* __LIBHB_H */ |
| 166 | |
| 167 | /*--------------------------------------------------------------------*/ |
| 168 | /*--- end libhb.h ---*/ |
| 169 | /*--------------------------------------------------------------------*/ |