1 ****** Example1: ******
2 Global Variable Declaration
4 /* Include all the header files that contains the interface declaration */
9 /* Other necessary header files */
11 #include <specannotation.h>
14 /* All other user-defined functions */
15 ALL_USER_DEFINED_FUNCTIONS // Make them static
17 /* Definition of interface info struct (per interface) */
18 typedef struct Put_info {
19 shared_ptr<TypeV> __RET__;
24 typedef struct Get_info {
25 shared_ptr<TypeV> __RET__;
28 /* End of info struct definition */
30 /* ID functions of interface */
31 static id_t Put_id() {
32 id_t id = PUT_ID; // Default ID == 0;
36 static id_t Get_id() {
40 /* End of ID functions */
44 /* Check_action function of interfaces */
45 bool Put_check_action(void *info, id_t __ID__) {
47 Put_info *theInfo = (Put_info) info;
48 shared_ptr<TypeV> __RET__ = theInfo->__RET__;
49 TypeK & key = theInfo->key;
50 TypeV & value = theInfo->value;
53 bool __COND_SAT__ = PUT_CONDITION;
56 check_passed = PUT_CHECK_EXPRESSION;
64 check_passed = PUT_POST_CHECK_EXPRESSION;
73 bool Get_check_action(void *info, id_t __ID__) {
76 /* End of check_action function definitions */
78 /* Initialization of interface<->function_ptr table */
79 #define INTERFACE_SIZE 2
80 void* func_ptr_table[INTERFACE_SIZE * 2];
82 /* Beginning of other user-defined variables */
85 /* End of other user-defined variables */
88 /* Define function for sequential code initialization */
89 void __sequential_init() {
90 /* Init func_ptr_table */
92 /* Init user-defined variables */
93 lock_acquired = false;
96 /* Pass the happens-before initialization here */
97 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
98 anno_hb_init hbConditionInit0;
99 hbConditionInit0.interface_num_before = 1;
100 hbConditionInit0.hb_condition_num_before = 1;
101 hbConditionInit0.interface_num_after = 2;
102 hbConditionInit0.hb_condition_num_after = 0;
103 spec_annotation hb_init0;
104 hb_init0.type = HB_INIT;
105 hb_init0.annotation = &hbConditionInit0;
106 cdsannotate(SPEC_ANALYSIS, &hb_init0);
108 /* End of Global construct generation in class */
110 /* The following static field declaration is necessary for class */
111 template <typename T>
112 bool CLASS<T>::lock_acquired;
114 template <typename T>
115 int CLASS<T>::reader_lock_cnt;
116 /* End of static field definition */
119 ****** Example2: ******
122 /* Include the header files first */
124 #include <cdsannotate.h>
125 #include <specannotation.h>
126 #include <spec_lib.h>
128 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
131 anno_interface_begin interface_begin;
132 interface_begin.interface_num = 0; // Interface number
133 spec_annotation annotation_interface_begin;
134 annotation_interface_begin.type = INTERFACE_BEGIN;
135 annotation_interface_begin.annotation = &interface_begin;
136 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
138 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
140 // HB conditions (if any)
142 anno_hb_condition hb_condition1;
143 hb_condition1.interface_num = 0; // Interface number
144 hb_condition1.hb_condition_num = 1; // HB condition number
145 spec_annotation annotation_hb_condition;
146 annotation_hb_condition.type = HB_CONDITION;
147 annotation_hb_condition.annotation = &hb_condition;
148 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
153 spec_annotation annotation_interface_end;
154 INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
155 info->__RET__ = __RET__;
158 anno_interface_end interface_end;
159 interface_end.interface_num = 0; // Interface number
160 interface_end.info = info; // Info
161 annotation_interface_end.type = INTERFACE_END;
162 annotation_interface_end.annotation = &interface_end;
163 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
167 ****** Example3: ******
168 Potential Commit Point
172 #include <cdsannotate.h>
174 /* Should add the __ATOMIC_RET__ if necessary */
175 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
177 if (POTENTIAL_CP_DEFINE_CONDITION) {
178 anno_potential_cp_define potential_cp_define;
179 potential_cp_define.label_num = 1; // Commit point label number
180 spec_annotation annotation_potential_cp_define;
181 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
182 annotation_potential_cp_define.annotation = &potential_cp_define;
183 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
186 ****** Example4: ******
190 #include <cdsannotate.h>
193 /* Should add the __ATOMIC_RET__ if necessary */
194 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
196 /* For all the interface check at this commit point (if there is multiple
198 // Commit point 3 <=> potentialCP 4
199 if (COMMIT_POINT3_CONDITION) {
200 anno_cp_define cp_define;
201 cp_define.label_num = 3;
202 cp_define.potential_cp_label_num = 1;
203 spec_annotation annotation_cp_define;
204 annotation_cp_define.type = CP_DEFINE;
205 annotation_cp_define.annotation = &cp_define;
206 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
208 // More if there are any
213 ***** Example5: ******
214 Commit Point Define Check
218 #include <cdsannotate.h>
221 /* Should add the __ATOMIC_RET__ if necessary */
222 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
225 /* For all the interface check at this commit point (if there is multiple
227 if (COMMIT_POINT3_CONDITION) {
228 anno_cp_define cp_define;
229 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
230 bool check_passed = false;
231 cp_define.check_passed = check_passed;
232 cp_define.interface_num = interface_num;
233 cp_define.label_num = 3;
234 cp_define.call_sequence_num = call_sequence_num;
235 spec_annotation annotation_cp_define;
236 annotation_cp_define.type = CP_DEFINE;
237 annotation_cp_define.annotation = &cp_define;
238 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
240 // More if there are any