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>
14 /* Include all the header files that contains the interface declaration */
20 /* All other user-defined functions */
21 ALL_USER_DEFINED_FUNCTIONS
23 /* Definition of interface info struct (per interface) */
24 typedef struct Put_info {
25 shared_ptr<TypeV> __RET__;
30 typedef struct Get_info {
31 shared_ptr<TypeV> __RET__;
34 /* End of info struct definition */
37 /* All function of action and check of interfaces */
38 bool Put_check_action(void *info) {
40 Put_info *theInfo = (Put_info) info;
41 shared_ptr<TypeV> __RET__ = theInfo->__RET__;
42 TypeK & key = theInfo->key;
43 TypeV & value = theInfo->value;
46 check_passed = PUT_CHECK_EXPRESSION;
54 TypeV *_Old_Val = DefineVarExpr;
57 check_passed = PUT_POST_CHECK_EXPRESSION;
71 /* Beginning of other user-defined variables */
74 /* End of other user-defined variables */
77 /* Define function for sequential code initialization */
78 void __sequential_init() {
79 /* Init user-defined variables */
80 lock_acquired = false;
83 /* Pass the happens-before initialization here */
84 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
85 anno_hb_init hbConditionInit0;
86 hbConditionInit0.interface_num_before = 1;
87 hbConditionInit0.hb_condition_num_before = 1;
88 hbConditionInit0.interface_num_after = 2;
89 hbConditionInit0.hb_condition_num_after = 0;
90 spec_annotation hb_init0;
91 hb_init0.type = HB_INIT;
92 hb_init0.annotation = &hbConditionInit0;
93 cdsannotate(SPEC_ANALYSIS, &hb_init0);
100 ****** Example2: ******
103 /* Include the header files first */
105 #include <cdsannotate.h>
106 #include <specannotation.h>
107 #include <spec_tag.h>
108 #include <spec_private_hashtable.h>
110 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
112 thrd_t tid = thrd_current();
113 uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
114 next(&__sequential.global_call_sequence);
115 put(&__sequential.interface_call_sequence, tid, call_sequence_num);
118 anno_interface_boundary interface_boundary;
119 interface_boundary.interface_num = 0; // Interface number
120 interface_boundary.call_sequence_num = call_sequence_num;
121 spec_annotation annotation_interface_begin;
122 annotation_interface_begin.type = INTERFACE_BEGIN;
123 annotation_interface_begin.annotation = &interface_boundary;
124 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
126 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
128 // HB conditions (if any)
130 anno_hb_condition hb_condition1;
131 hb_condition1.interface_num = 0; // Interface number
132 hb_condition1.hb_condition_num = 1; // HB condition number
133 hb_condition1.id = __ID__;
134 hb_condition1.call_sequence_num = call_sequence_num;
135 spec_annotation annotation_hb_condition;
136 annotation_hb_condition.type = HB_CONDITION;
137 annotation_hb_condition.annotation = &hb_condition;
138 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
143 spec_annotation annotation_interface_end;
144 annotation_interface_end.type = INTERFACE_END;
145 annotation_interface_end.annotation = &interface_boundary;
146 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
150 ****** Example3: ******
151 Potential Commit Point
154 #include <cdstrace.h>
155 #include <cdsannotate.h>
156 #include <spec_private_hashtable.h>
157 #include <_sepc_sequential_genenrated.h>
161 #define CAS (__ATOMIC_RET__ = CAS)
162 #define LOAD (__ATOMIC_RET__ = LOAD)
163 #define RMW (__ATOMIC_RET__ = RMW)
165 thrd_t tid = thrd_current();
166 if (POTENTIAL_CP_DEFINE_CONDITION) {
167 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
169 anno_potential_cp_define potential_cp_define;
170 potential_cp_define.interface_num = get(&__sequential.interface, tid);
171 potential_cp_define.label_num = 1; // Commit point label number
172 potential_cp_define.call_sequence_num = call_sequence_num;
173 spec_annotation annotation_potential_cp_define;
174 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
175 annotation_potential_cp_define.annotation = &potential_cp_define;
176 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
183 ****** Example4: ******
187 #include <cdstrace.h>
188 #include <cdsannotate.h>
189 #include <spec_private_hashtable.h>
190 #include <_spec_sequential_generated.h>
192 thrd_t __tid = thrd_current();
193 int interface_num = get(&__sequential.interface, tid);
194 /* For all the interface check at this commit point (if there is multiple
196 /* Need to compute the relationship between labels before hand */
197 switch (interface_num) {
199 // Commit point 3 <=> potentialCP 4
200 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
201 if (INTERFACE0_CHECK_CONDITION) {
204 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
206 /* Unfold all if there are multiple DefineVars */
208 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
211 /* Compute id; If not defined, assign the default ID */
212 int id = INTERFACE0_ID_EXPRESSION;
213 put(__sequential.id, tid, id);
215 /* Execute actions if there's any */
216 #define _Old_Val res0;
217 INTERFACE0_ACTION; // Unfolded right in place
221 anno_cp_define cp_define;
222 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
223 bool check_passed = false;
224 cp_define.check_passed = check_passed;
225 cp_define.interface_num = interface_num;
226 cp_define.label_num = 3;
227 cp_define.call_sequence_num = call_sequence_num;
228 spec_annotation annotation_cp_define;
229 annotation_cp_define.type = CP_DEFINE;
230 annotation_cp_define.annotation = &cp_define;
231 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
235 // Commit point 5 <=> potentialCP 6
236 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
237 if (INTERFACE1_CHECK_CONDITION) {
241 // Same as the above case
249 ***** Example5: ******
250 Commit Point Define Check
254 #include <cdstrace.h>
255 #include <cdsannotate.h>
256 #include <spec_private_hashtable.h>
257 #include <_spec_sequential_generated.h>
260 thrd_t __tid = thrd_current();
261 int interface_num = get(&__sequential.interface, tid);
262 /* For all the interface check at this commit point (if there is multiple
264 /* Need to compute the relationship between labels before hand */
265 switch (interface_num) {
267 if (COMMIT_POINT3_CONDITION) {
268 if (INTERFACE0_CHECK_CONDITION) {
271 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
273 /* Unfold all if there are multiple DefineVars */
275 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
278 /* Compute id; If not defined, assign the default ID */
279 int id = INTERFACE0_ID_EXPRESSION;
280 put(__sequential.id, tid, id);
282 /* Execute actions if there's any */
283 #define _Old_Val res0;
284 INTERFACE0_ACTION; // Unfolded right in place
288 anno_cp_define cp_define;
289 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
290 bool check_passed = false;
291 cp_define.check_passed = check_passed;
292 cp_define.interface_num = interface_num;
293 cp_define.label_num = 3;
294 cp_define.call_sequence_num = call_sequence_num;
295 spec_annotation annotation_cp_define;
296 annotation_cp_define.type = CP_DEFINE;
297 annotation_cp_define.annotation = &cp_define;
298 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
302 if (COMMIT_POINT5_CONDITION) {
303 if (INTERFACE1_CHECK_CONDITION) {
307 // Same as the above case