1 ****** Example1: ******
2 Global Variable Declaration
4 /* Include the header files first
5 ** This declaration will be written into a header file
7 /* @file _spec_sequential_generated.h */
8 /* @brief automatically generated file */
9 #ifndef __SPEC_SEQUENTIAL_GENERATED_H
10 #define __SPEC_SEQUENTIAL_GENERATED_H
11 #include <specannotation.h>
12 #include <spec_private_hashtable.h>
14 /* Beginning of struct Sequential */
15 typedef struct Sequential {
16 spec_private_hashtable cond;
17 spec_private_hashtable id;
18 spec_private_hashtable interface;
19 spec_private_hashtable interface_call_sequence;
21 /* DefineVar unfolded here */
22 spec_private_hashtable Put__Old_Val;
24 /* Beginning of other user-defined variables */
27 /* End of other user-defined variables */
29 } Sequential; /* End of struct Sequential */
31 /* Instance of the struct */
32 Sequential __sequential;
34 /* Define function for sequential code initialization */
35 void __sequential_init() {
36 /* Init internal variables */
37 init(&__sequential.cond);
38 init(&__sequential.id);
39 init(&__sequential.interface);
40 init(&__sequential.interface_call_sequence);
42 init(&__sequential.Put__Old_Val);
43 /* Init user-defined variables */
44 lock_acquired = false;
48 /* All other user-defined functions */
49 ALL_USER_DEFINED_FUNCTIONS
55 ****** Example2: ******
58 /* Include the header files first */
60 #include <cdsannotate.h>
61 #include <specannotation.h>
63 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
65 thrd_t tid = thrd_current();
66 uint64_t call_sequence_num = current(&__interface_call_sequence);
67 put(&__interface_call_sequence, tid, call_sequence_num);
70 anno_interface_boundary interface_boundary;
71 interface_boundary.interface_num = 0; // Interface number
72 interface_boundary.call_sequence_num = call_sequence_num;
73 spec_annotation annotation_interface_begin;
74 annotation_interface_begin.type = INTERFACE_BEGIN;
75 annotation_interface_begin.annotation = &interface_boundary;
76 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
78 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
79 int __COND__ = get(&__sequential.cond, tid);
80 uint64_t __ID__ = get(&__sequential.id, tid);
82 /* Post_check action, define macros for all DefineVars */
83 #define _Old_Val (get(&__sequential.put__Old_Val, tid))
85 bool post_check_passed = INTERFACE_POST_CHECK_CONDITION;
89 anno_post_check post_check;
90 post_check.check_passed = post_check_passed;
91 post_check.interface_num = interface_num;
92 post_check.call_sequence_num = call_sequence_num;
93 spec_annotation annotation_post_check;
94 annotation_post_check.type = POST_CHECK;
95 annotation_post_check.annotation = &post_check;
96 cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
98 // Post Action (if any)
99 POST_ACTION_CODE // Unfolded in place
101 // HB conditions (if any)
103 anno_hb_condition hb_condition1;
104 hb_condition1.interface_num = 0; // Interface number
105 hb_condition1.hb_condition_num = 1; // HB condition number
106 hb_condition1.id = id;
107 hb_condition1.call_sequence_num = call_sequence_num;
108 spec_annotation annotation_hb_condition;
109 annotation_hb_condition.type = HB_CONDITION;
110 annotation_hb_condition.annotation = &hb_condition;
111 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
116 spec_annotation annotation_interface_end;
117 annotation_interface_end.type = INTERFACE_END;
118 annotation_interface_end.annotation = &interface_boundary;
119 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
123 ****** Example3: ******
124 Potential Commit Point
127 #include <cdstrace.h>
128 #include <cdsannotate.h>
129 #include <spec_private_hashtable.h>
130 #include <_sepc_sequential_genenrated.h>
132 thrd_t __tid = thrd_current();
133 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
134 if (POTENTIAL_CP_DEFINE_CONDITION) {
135 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
136 int interface_num = get(&__sequential.interface, tid);
137 anno_potential_cp_define potential_cp_define;
138 potential_cp_define.interface_num = interface_num;
139 potential_cp_define.label_num = 1; // Commit point label number
140 potential_cp_define.call_sequence_num = call_sequence_num;
141 spec_annotation annotation_potential_cp_define;
142 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
143 annotation_potential_cp_define.annotation = &potential_cp_define;
144 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
147 ****** Example4: ******
151 #include <cdstrace.h>
152 #include <cdsannotate.h>
153 #include <spec_private_hashtable.h>
154 #include <_spec_sequential_generated.h>
156 thrd_t __tid = thrd_current();
157 int interface_num = get(&__sequential.interface, tid);
158 /* For all the interface check at this commit point (if there is multiple
160 /* Need to compute the relationship between labels before hand */
161 switch (interface_num) {
163 // Commit point 3 <=> potentialCP 4
164 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
165 if (INTERFACE0_CHECK_CONDITION) {
168 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
170 /* Unfold all if there are multiple DefineVars */
172 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
175 /* Compute id; If not defined, assign the default ID */
176 int id = INTERFACE0_ID_EXPRESSION;
177 put(__sequential.id, tid, id);
179 /* Execute actions if there's any */
180 #define _Old_Val res0;
181 INTERFACE0_ACTION; // Unfolded right in place
185 anno_cp_define cp_define;
186 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
187 bool check_passed = false;
188 cp_define.check_passed = check_passed;
189 cp_define.interface_num = interface_num;
190 cp_define.label_num = 3;
191 cp_define.call_sequence_num = call_sequence_num;
192 spec_annotation annotation_cp_define;
193 annotation_cp_define.type = CP_DEFINE;
194 annotation_cp_define.annotation = &cp_define;
195 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
199 // Commit point 5 <=> potentialCP 6
200 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
201 if (INTERFACE1_CHECK_CONDITION) {
205 // Same as the above case
213 ***** Example5: ******
214 Commit Point Define Check
218 #include <cdstrace.h>
219 #include <cdsannotate.h>
220 #include <spec_private_hashtable.h>
221 #include <_spec_sequential_generated.h>
224 thrd_t __tid = thrd_current();
225 int interface_num = get(&__sequential.interface, tid);
226 /* For all the interface check at this commit point (if there is multiple
228 /* Need to compute the relationship between labels before hand */
229 switch (interface_num) {
231 if (COMMIT_POINT3_CONDITION) {
232 if (INTERFACE0_CHECK_CONDITION) {
235 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
237 /* Unfold all if there are multiple DefineVars */
239 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
242 /* Compute id; If not defined, assign the default ID */
243 int id = INTERFACE0_ID_EXPRESSION;
244 put(__sequential.id, tid, id);
246 /* Execute actions if there's any */
247 #define _Old_Val res0;
248 INTERFACE0_ACTION; // Unfolded right in place
252 anno_cp_define cp_define;
253 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
254 bool check_passed = false;
255 cp_define.check_passed = check_passed;
256 cp_define.interface_num = interface_num;
257 cp_define.label_num = 3;
258 cp_define.call_sequence_num = call_sequence_num;
259 spec_annotation annotation_cp_define;
260 annotation_cp_define.type = CP_DEFINE;
261 annotation_cp_define.annotation = &cp_define;
262 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
266 if (COMMIT_POINT5_CONDITION) {
267 if (INTERFACE1_CHECK_CONDITION) {
271 // Same as the above case