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>
15 /* Beginning of struct Sequential */
16 typedef struct Sequential {
17 spec_private_hashtable interface;
18 Tag global_call_sequence;
20 /* Beginning of other user-defined variables */
23 /* End of other user-defined variables */
25 } Sequential; /* End of struct Sequential */
27 /* Instance of the struct */
28 Sequential __sequential;
30 /* Define function for sequential code initialization */
31 void __sequential_init() {
32 /* Init internal variables */
33 init(&__sequential.interface);
34 init(&global_call_sequence);
35 /* Init user-defined variables */
36 lock_acquired = false;
39 /* Pass the happens-before initialization here */
40 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
41 anno_hb_init hbConditionInit0;
42 hbConditionInit0.interface_num_before = 1;
43 hbConditionInit0.hb_condition_num_before = 1;
44 hbConditionInit0.interface_num_after = 2;
45 hbConditionInit0.hb_condition_num_after = 0;
46 spec_annotation hb_init0;
47 hb_init0.type = HB_INIT;
48 hb_init0.annotation = &hbConditionInit0;
49 cdsannotate(SPEC_ANALYSIS, &hb_init0);
52 /* All other user-defined functions */
53 ALL_USER_DEFINED_FUNCTIONS
59 ****** Example2: ******
62 /* Include the header files first */
64 #include <cdsannotate.h>
65 #include <specannotation.h>
67 #include <spec_private_hashtable.h>
69 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
71 thrd_t tid = thrd_current();
72 uint64_t call_sequence_num = current(&__sequential.global_call_sequence);
73 next(&__sequential.global_call_sequence);
74 put(&__sequential.interface_call_sequence, tid, call_sequence_num);
77 anno_interface_boundary interface_boundary;
78 interface_boundary.interface_num = 0; // Interface number
79 interface_boundary.call_sequence_num = call_sequence_num;
80 spec_annotation annotation_interface_begin;
81 annotation_interface_begin.type = INTERFACE_BEGIN;
82 annotation_interface_begin.annotation = &interface_boundary;
83 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
85 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
87 // HB conditions (if any)
89 anno_hb_condition hb_condition1;
90 hb_condition1.interface_num = 0; // Interface number
91 hb_condition1.hb_condition_num = 1; // HB condition number
92 hb_condition1.id = __ID__;
93 hb_condition1.call_sequence_num = call_sequence_num;
94 spec_annotation annotation_hb_condition;
95 annotation_hb_condition.type = HB_CONDITION;
96 annotation_hb_condition.annotation = &hb_condition;
97 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
102 spec_annotation annotation_interface_end;
103 annotation_interface_end.type = INTERFACE_END;
104 annotation_interface_end.annotation = &interface_boundary;
105 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
109 ****** Example3: ******
110 Potential Commit Point
113 #include <cdstrace.h>
114 #include <cdsannotate.h>
115 #include <spec_private_hashtable.h>
116 #include <_sepc_sequential_genenrated.h>
120 #define CAS (__ATOMIC_RET__ = CAS)
121 #define LOAD (__ATOMIC_RET__ = LOAD)
122 #define RMW (__ATOMIC_RET__ = RMW)
124 thrd_t tid = thrd_current();
125 if (POTENTIAL_CP_DEFINE_CONDITION) {
126 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
128 anno_potential_cp_define potential_cp_define;
129 potential_cp_define.interface_num = get(&__sequential.interface, tid);
130 potential_cp_define.label_num = 1; // Commit point label number
131 potential_cp_define.call_sequence_num = call_sequence_num;
132 spec_annotation annotation_potential_cp_define;
133 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
134 annotation_potential_cp_define.annotation = &potential_cp_define;
135 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
142 ****** Example4: ******
146 #include <cdstrace.h>
147 #include <cdsannotate.h>
148 #include <spec_private_hashtable.h>
149 #include <_spec_sequential_generated.h>
151 thrd_t __tid = thrd_current();
152 int interface_num = get(&__sequential.interface, tid);
153 /* For all the interface check at this commit point (if there is multiple
155 /* Need to compute the relationship between labels before hand */
156 switch (interface_num) {
158 // Commit point 3 <=> potentialCP 4
159 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
160 if (INTERFACE0_CHECK_CONDITION) {
163 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
165 /* Unfold all if there are multiple DefineVars */
167 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
170 /* Compute id; If not defined, assign the default ID */
171 int id = INTERFACE0_ID_EXPRESSION;
172 put(__sequential.id, tid, id);
174 /* Execute actions if there's any */
175 #define _Old_Val res0;
176 INTERFACE0_ACTION; // Unfolded right in place
180 anno_cp_define cp_define;
181 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
182 bool check_passed = false;
183 cp_define.check_passed = check_passed;
184 cp_define.interface_num = interface_num;
185 cp_define.label_num = 3;
186 cp_define.call_sequence_num = call_sequence_num;
187 spec_annotation annotation_cp_define;
188 annotation_cp_define.type = CP_DEFINE;
189 annotation_cp_define.annotation = &cp_define;
190 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
194 // Commit point 5 <=> potentialCP 6
195 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
196 if (INTERFACE1_CHECK_CONDITION) {
200 // Same as the above case
208 ***** Example5: ******
209 Commit Point Define Check
213 #include <cdstrace.h>
214 #include <cdsannotate.h>
215 #include <spec_private_hashtable.h>
216 #include <_spec_sequential_generated.h>
219 thrd_t __tid = thrd_current();
220 int interface_num = get(&__sequential.interface, tid);
221 /* For all the interface check at this commit point (if there is multiple
223 /* Need to compute the relationship between labels before hand */
224 switch (interface_num) {
226 if (COMMIT_POINT3_CONDITION) {
227 if (INTERFACE0_CHECK_CONDITION) {
230 /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a
232 /* Unfold all if there are multiple DefineVars */
234 put(&__sequential.put__Old_Val, tid, (uint64_t) res0);
237 /* Compute id; If not defined, assign the default ID */
238 int id = INTERFACE0_ID_EXPRESSION;
239 put(__sequential.id, tid, id);
241 /* Execute actions if there's any */
242 #define _Old_Val res0;
243 INTERFACE0_ACTION; // Unfolded right in place
247 anno_cp_define cp_define;
248 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
249 bool check_passed = false;
250 cp_define.check_passed = check_passed;
251 cp_define.interface_num = interface_num;
252 cp_define.label_num = 3;
253 cp_define.call_sequence_num = call_sequence_num;
254 spec_annotation annotation_cp_define;
255 annotation_cp_define.type = CP_DEFINE;
256 annotation_cp_define.annotation = &cp_define;
257 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
261 if (COMMIT_POINT5_CONDITION) {
262 if (INTERFACE1_CHECK_CONDITION) {
266 // Same as the above case