1 ****** Example1: ******
2 Global Variable Declaration
4 /* Include the header files first
5 ** This declaration will be written into a header file
8 /* @brief automatically generated file */
11 #include <specannotation.h>
12 #include <spec_private_hashtable.h>
14 typedef struct Sequential
16 spec_private_hashtabel cond;
17 spec_private_hashtabel id;
18 spec_private_hashtabel interface;
19 spec_private_hashtabel interface_call_sequence;
21 /* DefineVar unfolded here */
22 spec_private_hashtable Put__Old_Val;
24 /* Other user-defined variables */
29 Sequential __sequential;
31 /* All other user-defined functions */
32 ALL_USER_DEFINED_FUNCTIONS
39 ****** Example2: ******
40 Global Variable Initialization (Entry Point Unfolding)
42 #include <spec_private_hashtable.h>
45 init(&__sequential.condition);
46 init(&__sequential.id);
47 init(&__sequential.interface);
48 init(&__sequential.interface_call_sequence);
49 /* DefineVar initialized here */
52 /* User-define variables */
53 lock_acquired = false;
58 ****** Example3: ******
61 /* Include the header files first */
63 #include <cdsannotate.h>
64 #include <specannotation.h>
66 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
68 thrd_t tid = thrd_current();
69 uint64_t call_sequence_num = current(&__interface_call_sequence);
70 put(&__interface_call_sequence, tid, call_sequence_num);
73 anno_interface_boundary interface_boundary;
74 interface_boundary.interface_num = 0; // Interface number
75 interface_boundary.call_sequence_num = call_sequence_num;
76 spec_annotation annotation_interface_begin;
77 annotation_interface_begin.type = INTERFACE_BEGIN;
78 annotation_interface_begin.annotation = &interface_boundary;
79 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
81 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
82 int __COND__ = get(&__sequential.cond, tid);
83 uint64_t __ID__ = get(&__sequential.id, tid);
85 /* Post_check action, define macros for all DefineVars */
86 #define _Old_Val (get(&__sequential.put__Old_Val, tid))
88 bool post_check_passed = INTERFACE_POST_CHECK_CONDITION;
92 anno_post_check post_check;
93 post_check.check_passed = post_check_passed;
94 post_check.interface_num = interface_num;
95 post_check.call_sequence_num = call_sequence_num;
96 spec_annotation annotation_post_check;
97 annotation_post_check.type = POST_CHECK;
98 annotation_post_check.annotation = &post_check;
99 cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
101 // Post Action (if any)
102 POST_ACTION_CODE // Unfolded in place
104 // HB conditions (if any)
106 anno_hb_condition hb_condition1;
107 hb_condition1.interface_num = 0; // Interface number
108 hb_condition1.hb_condition_num = 1; // HB condition number
109 hb_condition1.id = id;
110 hb_condition1.call_sequence_num = call_sequence_num;
111 spec_annotation annotation_hb_condition;
112 annotation_hb_condition.type = HB_CONDITION;
113 annotation_hb_condition.annotation = &hb_condition;
114 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
119 spec_annotation annotation_interface_end;
120 annotation_interface_end.type = INTERFACE_END;
121 annotation_interface_end.annotation = &interface_boundary;
122 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
126 ****** Example4: ******
127 Potential Commit Point
130 #include <cdstrace.h>
131 #include <cdsannotate.h>
132 #include <spec_private_hashtable.h>
135 thrd_t __tid = thrd_current();
136 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
137 if (POTENTIAL_CP_DEFINE_CONDITION) {
138 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
139 int interface_num = get(&__sequential.interface, tid);
140 anno_potential_cp_define potential_cp_define;
141 potential_cp_define.interface_num = interface_num;
142 potential_cp_define.label_num = 1; // Commit point label number
143 potential_cp_define.call_sequence_num = call_sequence_num;
144 spec_annotation annotation_potential_cp_define;
145 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
146 annotation_potential_cp_define.annotation = &potential_cp_define;
147 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
150 ****** Example5: ******
154 #include <cdstrace.h>
155 #include <cdsannotate.h>
156 #include <spec_private_hashtable.h>
159 thrd_t __tid = thrd_current();
160 int interface_num = get(&__sequential.interface, tid);
161 /* For all the interface check at this commit point (if there is multiple
163 /* Need to compute the relationship between labels before hand */
164 switch (interface_num) {
166 // Commit point 3 <=> potentialCP 4
167 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
168 if (INTERFACE0_CHECK_CONDITION) {
171 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
173 /* Unfold all if there are multiple DefineVars */
175 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
178 /* Compute id; If not defined, assign the default ID */
179 int id = INTERFACE0_ID_EXPRESSION;
180 put(__sequential.id, tid, id);
182 /* Execute actions if there's any */
183 #define _Old_Val res0;
184 INTERFACE0_ACTION; // Unfolded right in place
188 anno_cp_define cp_define;
189 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
190 bool check_passed = false;
191 cp_define.check_passed = check_passed;
192 cp_define.interface_num = interface_num;
193 cp_define.label_num = 3;
194 cp_define.call_sequence_num = call_sequence_num;
195 spec_annotation annotation_cp_define;
196 annotation_cp_define.type = CP_DEFINE;
197 annotation_cp_define.annotation = &cp_define;
198 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
202 // Commit point 5 <=> potentialCP 6
203 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
204 if (INTERFACE1_CHECK_CONDITION) {
208 // Same as the above case
216 ***** Example6: ******
217 Commit Point Define Check
221 #include <cdstrace.h>
222 #include <cdsannotate.h>
223 #include <spec_private_hashtable.h>
227 thrd_t __tid = thrd_current();
228 int interface_num = get(&__sequential.interface, tid);
229 /* For all the interface check at this commit point (if there is multiple
231 /* Need to compute the relationship between labels before hand */
232 switch (interface_num) {
234 if (COMMIT_POINT3_CONDITION) {
235 if (INTERFACE0_CHECK_CONDITION) {
238 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
240 /* Unfold all if there are multiple DefineVars */
242 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
245 /* Compute id; If not defined, assign the default ID */
246 int id = INTERFACE0_ID_EXPRESSION;
247 put(__sequential.id, tid, id);
249 /* Execute actions if there's any */
250 #define _Old_Val res0;
251 INTERFACE0_ACTION; // Unfolded right in place
255 anno_cp_define cp_define;
256 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
257 bool check_passed = false;
258 cp_define.check_passed = check_passed;
259 cp_define.interface_num = interface_num;
260 cp_define.label_num = 3;
261 cp_define.call_sequence_num = call_sequence_num;
262 spec_annotation annotation_cp_define;
263 annotation_cp_define.type = CP_DEFINE;
264 annotation_cp_define.annotation = &cp_define;
265 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
269 if (COMMIT_POINT5_CONDITION) {
270 if (INTERFACE1_CHECK_CONDITION) {
274 // Same as the above case