1 ****** Example1: ******
2 Global Variable Declaration
5 /* Include all the header files that contains the interface declaration */
11 /* Other necessary header files */
12 #include <specannotation.h>
15 /* All other user-defined functions */
16 ALL_USER_DEFINED_FUNCTIONS
18 /* Definition of interface info struct (per interface) */
19 typedef struct Put_info {
20 shared_ptr<TypeV> __RET__;
25 typedef struct Get_info {
26 shared_ptr<TypeV> __RET__;
29 /* End of info struct definition */
31 /* ID functions of interface */
32 static id_t Put_id() {
37 static id_t Get_id() {
41 /* End of ID functions */
43 /* Initialization of interface<->function_ptr table */
44 #define INTERFACE_SIZE 2
45 void* func_ptr_table[INTERFACE_SIZE * 2] = {
48 /* Check_action function of interfaces */
49 bool Put_check_action(void *info, id_t __ID__) {
51 Put_info *theInfo = (Put_info) info;
52 shared_ptr<TypeV> __RET__ = theInfo->__RET__;
53 TypeK & key = theInfo->key;
54 TypeV & value = theInfo->value;
57 bool __COND_SAT__ = PUT_CONDITION;
60 check_passed = PUT_CHECK_EXPRESSION;
68 TypeV *_Old_Val = DefineVarExpr;
71 check_passed = PUT_POST_CHECK_EXPRESSION;
80 bool Get_check_action(void *info, id_t __ID__) {
83 /* End of check_action function definitions */
86 /* Beginning of other user-defined variables */
89 /* End of other user-defined variables */
92 /* Define function for sequential code initialization */
93 void __sequential_init() {
94 /* Init user-defined variables */
95 lock_acquired = false;
98 /* Pass the happens-before initialization here */
99 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
100 anno_hb_init hbConditionInit0;
101 hbConditionInit0.interface_num_before = 1;
102 hbConditionInit0.hb_condition_num_before = 1;
103 hbConditionInit0.interface_num_after = 2;
104 hbConditionInit0.hb_condition_num_after = 0;
105 spec_annotation hb_init0;
106 hb_init0.type = HB_INIT;
107 hb_init0.annotation = &hbConditionInit0;
108 cdsannotate(SPEC_ANALYSIS, &hb_init0);
114 ****** Example2: ******
117 /* Include the header files first */
119 #include <cdsannotate.h>
120 #include <specannotation.h>
121 #include <spec_tag.h>
122 #include <spec_private_hashtable.h>
124 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
126 thrd_t tid = thrd_current();
127 uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
128 next(&__sequential.global_call_sequence);
129 put(&__sequential.interface_call_sequence, tid, call_sequence_num);
132 anno_interface_boundary interface_boundary;
133 interface_boundary.interface_num = 0; // Interface number
134 interface_boundary.call_sequence_num = call_sequence_num;
135 spec_annotation annotation_interface_begin;
136 annotation_interface_begin.type = INTERFACE_BEGIN;
137 annotation_interface_begin.annotation = &interface_boundary;
138 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
140 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
142 // HB conditions (if any)
144 anno_hb_condition hb_condition1;
145 hb_condition1.interface_num = 0; // Interface number
146 hb_condition1.hb_condition_num = 1; // HB condition number
147 hb_condition1.id = __ID__;
148 hb_condition1.call_sequence_num = call_sequence_num;
149 spec_annotation annotation_hb_condition;
150 annotation_hb_condition.type = HB_CONDITION;
151 annotation_hb_condition.annotation = &hb_condition;
152 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
157 spec_annotation annotation_interface_end;
158 annotation_interface_end.type = INTERFACE_END;
159 annotation_interface_end.annotation = &interface_boundary;
160 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
164 ****** Example3: ******
165 Potential Commit Point
168 #include <cdstrace.h>
169 #include <cdsannotate.h>
170 #include <spec_private_hashtable.h>
171 #include <_sepc_sequential_genenrated.h>
175 #define CAS (__ATOMIC_RET__ = CAS)
176 #define LOAD (__ATOMIC_RET__ = LOAD)
177 #define RMW (__ATOMIC_RET__ = RMW)
179 thrd_t tid = thrd_current();
180 if (POTENTIAL_CP_DEFINE_CONDITION) {
181 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
183 anno_potential_cp_define potential_cp_define;
184 potential_cp_define.interface_num = get(&__sequential.interface, tid);
185 potential_cp_define.label_num = 1; // Commit point label number
186 potential_cp_define.call_sequence_num = call_sequence_num;
187 spec_annotation annotation_potential_cp_define;
188 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
189 annotation_potential_cp_define.annotation = &potential_cp_define;
190 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
197 ****** Example4: ******
201 #include <cdstrace.h>
202 #include <cdsannotate.h>
203 #include <spec_private_hashtable.h>
204 #include <_spec_sequential_generated.h>
206 thrd_t __tid = thrd_current();
207 int interface_num = get(&__sequential.interface, tid);
208 /* For all the interface check at this commit point (if there is multiple
210 /* Need to compute the relationship between labels before hand */
211 switch (interface_num) {
213 // Commit point 3 <=> potentialCP 4
214 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
215 if (INTERFACE0_CHECK_CONDITION) {
218 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
220 /* Unfold all if there are multiple DefineVars */
222 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
225 /* Compute id; If not defined, assign the default ID */
226 int id = INTERFACE0_ID_EXPRESSION;
227 put(__sequential.id, tid, id);
229 /* Execute actions if there's any */
230 #define _Old_Val res0;
231 INTERFACE0_ACTION; // Unfolded right in place
235 anno_cp_define cp_define;
236 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
237 bool check_passed = false;
238 cp_define.check_passed = check_passed;
239 cp_define.interface_num = interface_num;
240 cp_define.label_num = 3;
241 cp_define.call_sequence_num = call_sequence_num;
242 spec_annotation annotation_cp_define;
243 annotation_cp_define.type = CP_DEFINE;
244 annotation_cp_define.annotation = &cp_define;
245 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
249 // Commit point 5 <=> potentialCP 6
250 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
251 if (INTERFACE1_CHECK_CONDITION) {
255 // Same as the above case
263 ***** Example5: ******
264 Commit Point Define Check
268 #include <cdstrace.h>
269 #include <cdsannotate.h>
270 #include <spec_private_hashtable.h>
271 #include <_spec_sequential_generated.h>
274 thrd_t __tid = thrd_current();
275 int interface_num = get(&__sequential.interface, tid);
276 /* For all the interface check at this commit point (if there is multiple
278 /* Need to compute the relationship between labels before hand */
279 switch (interface_num) {
281 if (COMMIT_POINT3_CONDITION) {
282 if (INTERFACE0_CHECK_CONDITION) {
285 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
287 /* Unfold all if there are multiple DefineVars */
289 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
292 /* Compute id; If not defined, assign the default ID */
293 int id = INTERFACE0_ID_EXPRESSION;
294 put(__sequential.id, tid, id);
296 /* Execute actions if there's any */
297 #define _Old_Val res0;
298 INTERFACE0_ACTION; // Unfolded right in place
302 anno_cp_define cp_define;
303 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
304 bool check_passed = false;
305 cp_define.check_passed = check_passed;
306 cp_define.interface_num = interface_num;
307 cp_define.label_num = 3;
308 cp_define.call_sequence_num = call_sequence_num;
309 spec_annotation annotation_cp_define;
310 annotation_cp_define.type = CP_DEFINE;
311 annotation_cp_define.annotation = &cp_define;
312 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
316 if (COMMIT_POINT5_CONDITION) {
317 if (INTERFACE1_CHECK_CONDITION) {
321 // Same as the above case