blob: 10768d03ce30af989bfcfd576bf672131703072e [file] [log] [blame]
sewardjf98e1c02008-10-25 16:22:41 +00001
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
sewardj9eecbbb2010-05-03 21:37:12 +000012 Copyright (C) 2008-2010 OpenWorks Ltd
sewardjf98e1c02008-10-25 16:22:41 +000013 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
sewardjf98e1c02008-10-25 16:22:41 +000042/* 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. */
45Thr* libhb_init (
46 void (*get_stacktrace)( Thr*, Addr*, UWord ),
sewardjd52392d2008-11-08 20:36:26 +000047 ExeContext* (*get_EC)( Thr* )
sewardjf98e1c02008-10-25 16:22:41 +000048 );
49
50/* Shut down the library, and print stats (in fact that's _all_
51 this is for.) */
52void libhb_shutdown ( Bool show_stats );
53
54/* Thread creation: returns Thr* for new thread */
55Thr* libhb_create ( Thr* parent );
56
57/* Thread async exit */
sewardjffce8152011-06-24 10:09:41 +000058void libhb_async_exit ( Thr* exitter );
59void libhb_joinedwith_done ( Thr* exitter );
sewardjf98e1c02008-10-25 16:22:41 +000060
61/* Synchronisation objects (abstract to caller) */
62
63/* Allocate a new one (alloc'd by library) */
64SO* libhb_so_alloc ( void );
65
66/* Dealloc one */
67void 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. */
84void 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. */
94void libhb_so_recv ( Thr* thr, SO* so, Bool strong_recv );
95
96/* Has this SO ever been sent on? */
97Bool libhb_so_everSent ( SO* so );
98
99/* Memory accesses (1/2/4/8 byte size). They report a race if one is
100 found. */
sewardj23f12002009-07-24 08:45:08 +0000101#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))
sewardjf98e1c02008-10-25 16:22:41 +0000106
sewardj23f12002009-07-24 08:45:08 +0000107#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))
sewardjf98e1c02008-10-25 16:22:41 +0000112
sewardj23f12002009-07-24 08:45:08 +0000113void zsm_sapply08_f__msmcwrite ( Thr* thr, Addr a );
114void zsm_sapply16_f__msmcwrite ( Thr* thr, Addr a );
115void zsm_sapply32_f__msmcwrite ( Thr* thr, Addr a );
116void zsm_sapply64_f__msmcwrite ( Thr* thr, Addr a );
117void zsm_sapplyNN_f__msmcwrite ( Thr* thr, Addr a, SizeT len );
sewardjf98e1c02008-10-25 16:22:41 +0000118
sewardj23f12002009-07-24 08:45:08 +0000119void zsm_sapply08_f__msmcread ( Thr* thr, Addr a );
120void zsm_sapply16_f__msmcread ( Thr* thr, Addr a );
121void zsm_sapply32_f__msmcread ( Thr* thr, Addr a );
122void zsm_sapply64_f__msmcread ( Thr* thr, Addr a );
123void zsm_sapplyNN_f__msmcread ( Thr* thr, Addr a, SizeT len );
sewardjf98e1c02008-10-25 16:22:41 +0000124
sewardj23f12002009-07-24 08:45:08 +0000125void libhb_Thr_resumes ( Thr* thr );
sewardjf98e1c02008-10-25 16:22:41 +0000126
127/* Set memory address ranges to new (freshly allocated), or noaccess
sewardjfd35d492011-03-17 19:39:55 +0000128 (no longer accessible). NB: "AHAE" == "Actually Has An Effect" :-) */
sewardj23f12002009-07-24 08:45:08 +0000129void libhb_srange_new ( Thr*, Addr, SizeT );
sewardj406bac82010-03-03 23:03:40 +0000130void libhb_srange_untrack ( Thr*, Addr, SizeT );
sewardjfd35d492011-03-17 19:39:55 +0000131void libhb_srange_noaccess_NoFX ( Thr*, Addr, SizeT ); /* IS IGNORED */
132void libhb_srange_noaccess_AHAE ( Thr*, Addr, SizeT ); /* IS NOT IGNORED */
sewardjf98e1c02008-10-25 16:22:41 +0000133
sewardj60626642011-03-10 15:14:37 +0000134/* Get and set the hgthread (pointer to corresponding Thread
135 structure). */
sewardj0b20a152011-03-10 21:34:21 +0000136Thread* libhb_get_Thr_hgthread ( Thr* );
137void libhb_set_Thr_hgthread ( Thr*, Thread* );
sewardjf98e1c02008-10-25 16:22:41 +0000138
139/* Low level copy of shadow state from [src,src+len) to [dst,dst+len).
140 Overlapping moves are checked for and asserted against. */
sewardj23f12002009-07-24 08:45:08 +0000141void libhb_copy_shadow_state ( Thr* thr, Addr src, Addr dst, SizeT len );
sewardjf98e1c02008-10-25 16:22:41 +0000142
143/* Call this periodically to give libhb the opportunity to
144 garbage-collect its internal data structures. */
145void libhb_maybe_GC ( void );
146
sewardjc5ea9962008-12-07 01:41:46 +0000147/* Extract info from the conflicting-access machinery. */
148Bool libhb_event_map_lookup ( /*OUT*/ExeContext** resEC,
sewardjffce8152011-06-24 10:09:41 +0000149 /*OUT*/Thr** resThr,
150 /*OUT*/SizeT* resSzB,
151 /*OUT*/Bool* resIsW,
152 /*OUT*/WordSetID* locksHeldW,
sewardjc5ea9962008-12-07 01:41:46 +0000153 Thr* thr, Addr a, SizeT szB, Bool isW );
154
sewardjffce8152011-06-24 10:09:41 +0000155/* ------ 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. */
159WordSetU* HG_(get_univ_lsets) ( void );
160
161/* Get the the header pointer for the double linked list of locks
162 (admin_locks). */
163Lock* HG_(get_admin_locks) ( void );
164
sewardjf98e1c02008-10-25 16:22:41 +0000165#endif /* __LIBHB_H */
166
167/*--------------------------------------------------------------------*/
168/*--- end libhb.h ---*/
169/*--------------------------------------------------------------------*/