Computer Laboratory

tesla_class_global.c
Go to the documentation of this file.
1 /*-
2  * Copyright (c) 2011 Robert N. M. Watson
3  * Copyright (c) 2012-2013 Jonathan Anderson
4  * All rights reserved.
5  *
6  * This software was developed by SRI International and the University of
7  * Cambridge Computer Laboratory under DARPA/AFRL contract (FA8750-10-C-0237)
8  * ("CTSRD"), as part of the DARPA CRASH research programme.
9  *
10  * Redistribution and use in source and binary forms, with or without
11  * modification, are permitted provided that the following conditions
12  * are met:
13  * 1. Redistributions of source code must retain the above copyright
14  * notice, this list of conditions and the following disclaimer.
15  * 2. Redistributions in binary form must reproduce the above copyright
16  * notice, this list of conditions and the following disclaimer in the
17  * documentation and/or other materials provided with the distribution.
18  *
19  * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND
20  * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
21  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
22  * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
23  * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
24  * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
25  * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
26  * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
27  * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
28  * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
29  * SUCH DAMAGE.
30  *
31  * $Id$
32  */
33 
34 #include "tesla_internal.h"
35 
36 static void tesla_class_global_lock_init(struct tesla_class *tsp);
37 static void tesla_class_global_lock_destroy(struct tesla_class *tsp);
38 
39 int
41 {
42 
43  assert(tsp->tc_context == TESLA_CONTEXT_GLOBAL);
44  tesla_class_global_lock_init(tsp);
45  return (TESLA_SUCCESS);
46 }
47 
48 void
50 {
51 
52  assert(tsp->tc_context == TESLA_CONTEXT_GLOBAL);
53  tesla_lock(&tsp->tc_lock);
54 }
55 
56 void
58 {
59 
60  assert(tsp->tc_context == TESLA_CONTEXT_GLOBAL);
61  tesla_unlock(&tsp->tc_lock);
62 }
63 
64 void
66 {
67 
68  tesla_class_global_lock_destroy(tsp);
69 }
70 
71 
72 /*
73  * Currently, this serialises all automata associated with a globally-scoped
74  * assertion. This is undesirable, and we should think about something more
75  * granular, such as using key values to hash to locks. This might cause
76  * atomicity problems when composing multi-clause expressions, however; more
77  * investigation required.
78  */
79 void
80 tesla_class_global_lock_init(struct tesla_class *tsp)
81 {
82 
83 #ifdef _KERNEL
84  mtx_init(&tsp->tc_lock, "tesla", NULL, MTX_DEF);
85 #else
86  __debug int error = pthread_mutex_init(&tsp->tc_lock, NULL);
87  assert(error == 0);
88 #endif
89 }
90 
91 void
92 tesla_class_global_lock_destroy(struct tesla_class *tsp)
93 {
94 
95 #ifdef _KERNEL
96  mtx_destroy(&tsp->tc_lock);
97 #else
98  __debug int error = pthread_mutex_destroy(&tsp->tc_lock);
99  assert(error == 0);
100 #endif
101 }