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-2010 OpenWorks Ltd 13 info (at) 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 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 ), 47 ExeContext* (*get_EC)( Thr* ) 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 */ 58 void libhb_async_exit ( Thr* exitter ); 59 60 /* Synchronisation objects (abstract to caller) */ 61 62 /* Allocate a new one (alloc'd by library) */ 63 SO* libhb_so_alloc ( void ); 64 65 /* Dealloc one */ 66 void libhb_so_dealloc ( SO* so ); 67 68 /* Send a message via a sync object. If strong_send is true, the 69 resulting inter-thread dependency seen by a future receiver of this 70 message will be a dependency on this thread only. That is, in a 71 strong send, the VC inside the SO is replaced by the clock of the 72 sending thread. For a weak send, the sender's VC is joined into 73 that already in the SO, if any. This subtlety is needed to model 74 rwlocks: a strong send corresponds to releasing a rwlock that had 75 been w-held (or releasing a standard mutex). A weak send 76 corresponds to releasing a rwlock that has been r-held. 77 78 (rationale): Since in general many threads may hold a rwlock in 79 r-mode, a weak send facility is necessary in order that the final 80 SO reflects the join of the VCs of all the threads releasing the 81 rwlock, rather than merely holding the VC of the most recent thread 82 to release it. */ 83 void libhb_so_send ( Thr* thr, SO* so, Bool strong_send ); 84 85 /* Recv a message from a sync object. If strong_recv is True, the 86 resulting inter-thread dependency is considered adequate to induce 87 a h-b ordering on both reads and writes. If it is False, the 88 implied h-b ordering exists only for reads, not writes. This is 89 subtlety is required in order to support reader-writer locks: a 90 thread doing a write-acquire of a rwlock (or acquiring a normal 91 mutex) models this by doing a strong receive. A thread doing a 92 read-acquire of a rwlock models this by doing a !strong_recv. */ 93 void libhb_so_recv ( Thr* thr, SO* so, Bool strong_recv ); 94 95 /* Has this SO ever been sent on? */ 96 Bool libhb_so_everSent ( SO* so ); 97 98 /* Memory accesses (1/2/4/8 byte size). They report a race if one is 99 found. */ 100 #define LIBHB_CWRITE_1(_thr,_a) zsm_sapply08_f__msmcwrite((_thr),(_a)) 101 #define LIBHB_CWRITE_2(_thr,_a) zsm_sapply16_f__msmcwrite((_thr),(_a)) 102 #define LIBHB_CWRITE_4(_thr,_a) zsm_sapply32_f__msmcwrite((_thr),(_a)) 103 #define LIBHB_CWRITE_8(_thr,_a) zsm_sapply64_f__msmcwrite((_thr),(_a)) 104 #define LIBHB_CWRITE_N(_thr,_a,_n) zsm_sapplyNN_f__msmcwrite((_thr),(_a),(_n)) 105 106 #define LIBHB_CREAD_1(_thr,_a) zsm_sapply08_f__msmcread((_thr),(_a)) 107 #define LIBHB_CREAD_2(_thr,_a) zsm_sapply16_f__msmcread((_thr),(_a)) 108 #define LIBHB_CREAD_4(_thr,_a) zsm_sapply32_f__msmcread((_thr),(_a)) 109 #define LIBHB_CREAD_8(_thr,_a) zsm_sapply64_f__msmcread((_thr),(_a)) 110 #define LIBHB_CREAD_N(_thr,_a,_n) zsm_sapplyNN_f__msmcread((_thr),(_a),(_n)) 111 112 void zsm_sapply08_f__msmcwrite ( Thr* thr, Addr a ); 113 void zsm_sapply16_f__msmcwrite ( Thr* thr, Addr a ); 114 void zsm_sapply32_f__msmcwrite ( Thr* thr, Addr a ); 115 void zsm_sapply64_f__msmcwrite ( Thr* thr, Addr a ); 116 void zsm_sapplyNN_f__msmcwrite ( Thr* thr, Addr a, SizeT len ); 117 118 void zsm_sapply08_f__msmcread ( Thr* thr, Addr a ); 119 void zsm_sapply16_f__msmcread ( Thr* thr, Addr a ); 120 void zsm_sapply32_f__msmcread ( Thr* thr, Addr a ); 121 void zsm_sapply64_f__msmcread ( Thr* thr, Addr a ); 122 void zsm_sapplyNN_f__msmcread ( Thr* thr, Addr a, SizeT len ); 123 124 void libhb_Thr_resumes ( Thr* thr ); 125 126 /* Set memory address ranges to new (freshly allocated), or noaccess 127 (no longer accessible). */ 128 void libhb_srange_new ( Thr*, Addr, SizeT ); 129 void libhb_srange_noaccess ( Thr*, Addr, SizeT ); /* IS IGNORED */ 130 void libhb_srange_untrack ( Thr*, Addr, SizeT ); 131 132 /* For the convenience of callers, we offer to store one void* item in 133 a Thr, which we ignore, but the caller can get or set any time. */ 134 void* libhb_get_Thr_opaque ( Thr* ); 135 void libhb_set_Thr_opaque ( Thr*, void* ); 136 137 /* Low level copy of shadow state from [src,src+len) to [dst,dst+len). 138 Overlapping moves are checked for and asserted against. */ 139 void libhb_copy_shadow_state ( Thr* thr, Addr src, Addr dst, SizeT len ); 140 141 /* Call this periodically to give libhb the opportunity to 142 garbage-collect its internal data structures. */ 143 void libhb_maybe_GC ( void ); 144 145 /* Extract info from the conflicting-access machinery. */ 146 Bool libhb_event_map_lookup ( /*OUT*/ExeContext** resEC, 147 /*OUT*/Thr** resThr, 148 /*OUT*/SizeT* resSzB, 149 /*OUT*/Bool* resIsW, 150 Thr* thr, Addr a, SizeT szB, Bool isW ); 151 152 #endif /* __LIBHB_H */ 153 154 /*--------------------------------------------------------------------*/ 155 /*--- end libhb.h ---*/ 156 /*--------------------------------------------------------------------*/ 157
