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 | |
| 12 | Copyright (C) 2008-2008 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, 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 | /* Abstract to the lib: execution contexts */ |
| 43 | /* struct _EC will be defined by user at some point. */ |
| 44 | typedef struct _EC EC; |
| 45 | |
| 46 | /* Initialise library; returns Thr* for root thread. 'shadow_alloc' |
| 47 | should never return NULL, instead it should simply not return if |
| 48 | they encounter an out-of-memory condition. */ |
| 49 | Thr* libhb_init ( |
| 50 | void (*get_stacktrace)( Thr*, Addr*, UWord ), |
| 51 | struct _EC* (*stacktrace_to_EC)( Addr*, UWord ), |
| 52 | struct _EC* (*get_EC)( Thr* ) |
| 53 | ); |
| 54 | |
| 55 | /* Shut down the library, and print stats (in fact that's _all_ |
| 56 | this is for.) */ |
| 57 | void libhb_shutdown ( Bool show_stats ); |
| 58 | |
| 59 | /* Thread creation: returns Thr* for new thread */ |
| 60 | Thr* libhb_create ( Thr* parent ); |
| 61 | |
| 62 | /* Thread async exit */ |
| 63 | void libhb_async_exit ( Thr* exitter ); |
| 64 | |
| 65 | /* Synchronisation objects (abstract to caller) */ |
| 66 | |
| 67 | /* Allocate a new one (alloc'd by library) */ |
| 68 | SO* libhb_so_alloc ( void ); |
| 69 | |
| 70 | /* Dealloc one */ |
| 71 | void libhb_so_dealloc ( SO* so ); |
| 72 | |
| 73 | /* Send a message via a sync object. If strong_send is true, the |
| 74 | resulting inter-thread dependency seen by a future receiver of this |
| 75 | message will be a dependency on this thread only. That is, in a |
| 76 | strong send, the VC inside the SO is replaced by the clock of the |
| 77 | sending thread. For a weak send, the sender's VC is joined into |
| 78 | that already in the SO, if any. This subtlety is needed to model |
| 79 | rwlocks: a strong send corresponds to releasing a rwlock that had |
| 80 | been w-held (or releasing a standard mutex). A weak send |
| 81 | corresponds to releasing a rwlock that has been r-held. |
| 82 | |
| 83 | (rationale): Since in general many threads may hold a rwlock in |
| 84 | r-mode, a weak send facility is necessary in order that the final |
| 85 | SO reflects the join of the VCs of all the threads releasing the |
| 86 | rwlock, rather than merely holding the VC of the most recent thread |
| 87 | to release it. */ |
| 88 | void libhb_so_send ( Thr* thr, SO* so, Bool strong_send ); |
| 89 | |
| 90 | /* Recv a message from a sync object. If strong_recv is True, the |
| 91 | resulting inter-thread dependency is considered adequate to induce |
| 92 | a h-b ordering on both reads and writes. If it is False, the |
| 93 | implied h-b ordering exists only for reads, not writes. This is |
| 94 | subtlety is required in order to support reader-writer locks: a |
| 95 | thread doing a write-acquire of a rwlock (or acquiring a normal |
| 96 | mutex) models this by doing a strong receive. A thread doing a |
| 97 | read-acquire of a rwlock models this by doing a !strong_recv. */ |
| 98 | void libhb_so_recv ( Thr* thr, SO* so, Bool strong_recv ); |
| 99 | |
| 100 | /* Has this SO ever been sent on? */ |
| 101 | Bool libhb_so_everSent ( SO* so ); |
| 102 | |
| 103 | /* Memory accesses (1/2/4/8 byte size). They report a race if one is |
| 104 | found. */ |
| 105 | #define LIBHB_WRITE_1(_thr,_a) zsm_apply8___msm_write((_thr),(_a)) |
| 106 | #define LIBHB_WRITE_2(_thr,_a) zsm_apply16___msm_write((_thr),(_a)) |
| 107 | #define LIBHB_WRITE_4(_thr,_a) zsm_apply32___msm_write((_thr),(_a)) |
| 108 | #define LIBHB_WRITE_8(_thr,_a) zsm_apply64___msm_write((_thr),(_a)) |
| 109 | #define LIBHB_WRITE_N(_thr,_a,_n) zsm_apply_range___msm_read((_thr),(_a),(_n)) |
| 110 | |
| 111 | #define LIBHB_READ_1(_thr,_a) zsm_apply8___msm_read((_thr),(_a)) |
| 112 | #define LIBHB_READ_2(_thr,_a) zsm_apply16___msm_read((_thr),(_a)) |
| 113 | #define LIBHB_READ_4(_thr,_a) zsm_apply32___msm_read((_thr),(_a)) |
| 114 | #define LIBHB_READ_8(_thr,_a) zsm_apply64___msm_read((_thr),(_a)) |
| 115 | #define LIBHB_READ_N(_thr,_a,_n) zsm_apply_range___msm_read((_thr),(_a),(_n)) |
| 116 | |
| 117 | void zsm_apply8___msm_write ( Thr* thr, Addr a ); |
| 118 | void zsm_apply16___msm_write ( Thr* thr, Addr a ); |
| 119 | void zsm_apply32___msm_write ( Thr* thr, Addr a ); |
| 120 | void zsm_apply64___msm_write ( Thr* thr, Addr a ); |
| 121 | void zsm_apply_range___msm_write ( Thr* thr, |
| 122 | Addr a, SizeT len ); |
| 123 | |
| 124 | void zsm_apply8___msm_read ( Thr* thr, Addr a ); |
| 125 | void zsm_apply16___msm_read ( Thr* thr, Addr a ); |
| 126 | void zsm_apply32___msm_read ( Thr* thr, Addr a ); |
| 127 | void zsm_apply64___msm_read ( Thr* thr, Addr a ); |
| 128 | void zsm_apply_range___msm_read ( Thr* thr, |
| 129 | Addr a, SizeT len ); |
| 130 | |
| 131 | |
| 132 | /* Set memory address ranges to new (freshly allocated), or noaccess |
| 133 | (no longer accessible). */ |
| 134 | void libhb_range_new ( Thr*, Addr, SizeT ); |
| 135 | void libhb_range_noaccess ( Thr*, Addr, SizeT ); |
| 136 | |
| 137 | /* For the convenience of callers, we offer to store one void* item in |
| 138 | a Thr, which we ignore, but the caller can get or set any time. */ |
| 139 | void* libhb_get_Thr_opaque ( Thr* ); |
| 140 | void libhb_set_Thr_opaque ( Thr*, void* ); |
| 141 | |
| 142 | /* Low level copy of shadow state from [src,src+len) to [dst,dst+len). |
| 143 | Overlapping moves are checked for and asserted against. */ |
| 144 | void libhb_copy_shadow_state ( Addr src, Addr dst, SizeT len ); |
| 145 | |
| 146 | /* Call this periodically to give libhb the opportunity to |
| 147 | garbage-collect its internal data structures. */ |
| 148 | void libhb_maybe_GC ( void ); |
| 149 | |
| 150 | #endif /* __LIBHB_H */ |
| 151 | |
| 152 | /*--------------------------------------------------------------------*/ |
| 153 | /*--- end libhb.h ---*/ |
| 154 | /*--------------------------------------------------------------------*/ |