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 bool __COND__ = get(&__cond, tid);
83 uint64_t id = get(&__id, tid);
85 // HB conditions (if any)
87 anno_hb_condition hb_condition1;
88 hb_condition1.interface_num = 0; // Interface number
89 hb_condition1.hb_condition_num = 1; // HB condition number
90 hb_condition1.id = id;
91 hb_condition1.call_sequence_num = call_sequence_num;
92 spec_annotation annotation_hb_condition;
93 annotation_hb_condition.type = HB_CONDITION;
94 annotation_hb_condition.annotation = &hb_condition;
95 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
99 // Post check (if any)
100 bool post_check_passed = POST_CHECK_CONDITION;
101 anno_post_check post_check;
102 post_check.check_passed = post_check_passed;
103 post_check.interface_num = interface_num;
104 post_check.call_sequence_num = call_sequence_num;
105 spec_annotation annotation_post_check;
106 annotation_post_check.type = POST_CHECK;
107 annotation_post_check.annotation = &post_check;
108 cdsannotate(SPEC_ANALYSIS, &annotation_post_check);
110 // Post Action (if any)
111 POST_ACTION_CODE // Unfolded in place
114 spec_annotation annotation_interface_end;
115 annotation_interface_end.type = INTERFACE_END;
116 annotation_interface_end.annotation = &interface_boundary;
117 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
121 ****** Example4: ******
122 Potential Commit Point
125 #include <cdstrace.h>
126 #include <cdsannotate.h>
127 #include <spec_private_hashtable.h>
130 thrd_t __tid = thrd_current();
131 uint64_t __ATOMIC_RET__ = get_prev_value(tid);
132 if (POTENTIAL_CP_DEFINE_CONDITION) {
133 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
134 int interface_num = get(&__sequential.interface, tid);
135 anno_potential_cp_define potential_cp_define;
136 potential_cp_define.interface_num = interface_num;
137 potential_cp_define.label_num = 1; // Commit point label number
138 potential_cp_define.call_sequence_num = call_sequence_num;
139 spec_annotation annotation_potential_cp_define;
140 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
141 annotation_potential_cp_define.annotation = &potential_cp_define;
142 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
145 ****** Example5: ******
149 #include <cdstrace.h>
150 #include <cdsannotate.h>
151 #include <spec_private_hashtable.h>
154 thrd_t __tid = thrd_current();
155 int interface_num = get(&__sequential.interface, tid);
156 /* For all the interface check at this commit point (if there is multiple
158 /* Need to compute the relationship between labels before hand */
159 switch (interface_num) {
161 // Commit point 3 <=> potentialCP 4
162 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) {
163 if (INTERFACE0_CHECK_CONDITION) {
166 /* For all DefineVar of INTERFACE0 (Type id = Expr) */
167 FIXME: Type res0 = Expr;
168 put(__sequential.put_id, tid,
169 #define _Old_Val __sequential.put_id
170 INTERFACE0_ACTION; // Unfolded right in place
172 anno_cp_define cp_define;
173 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
174 bool check_passed = false;
175 cp_define.check_passed = check_passed;
176 cp_define.interface_num = interface_num;
177 cp_define.label_num = 3;
178 cp_define.call_sequence_num = call_sequence_num;
179 spec_annotation annotation_cp_define;
180 annotation_cp_define.type = CP_DEFINE;
181 annotation_cp_define.annotation = &cp_define;
182 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
186 // Commit point 5 <=> potentialCP 6
187 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) {
188 if (INTERFACE1_CHECK_CONDITION) {
191 INTERFACE1_ACTION; // Unfolded right in place
193 anno_cp_define cp_define;
194 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
195 bool check_passed = false;
196 cp_define.check_passed = check_passed;
197 cp_define.interface_num = interface_num;
198 cp_define.label_num = 5;
199 cp_define.call_sequence_num = call_sequence_num;
200 spec_annotation annotation_cp_define;
201 annotation_cp_define.type = CP_DEFINE;
202 annotation_cp_define.annotation = &cp_define;
203 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
211 ***** Example6: ******
212 Commit Point Define Check