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;
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 */
91 func_ptr_table = (void**) malloc(sizeof(void*) * 2);
92 func_ptr_table[0] = (void*) &Put_id;
93 func_ptr_table[1] = (void*) &Put_check_action;
94 func_ptr_table[2] = (void*) &Get_id;
95 func_ptr_table[3] = (void*) &Get_check_action;
97 /* Init user-defined variables */
98 lock_acquired = false;
101 /* Pass function table info */
102 anno_func_table_init func_table;
103 func_table.size = INTERFACE_SIZE;
104 func_table.table = func_ptr_table;
105 spec_annotation func_init;
106 func_init.type = FUNC_TABLE_INIT;
107 func_init.annotation = &anno_func_table_init;
108 cdsannotate(SPEC_ANALYSIS, &func_init);
110 /* Pass the happens-before initialization here */
111 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
112 anno_hb_init hbConditionInit0;
113 hbConditionInit0.interface_num_before = 1;
114 hbConditionInit0.hb_condition_num_before = 1;
115 hbConditionInit0.interface_num_after = 2;
116 hbConditionInit0.hb_condition_num_after = 0;
117 spec_annotation hb_init0;
118 hb_init0.type = HB_INIT;
119 hb_init0.annotation = &hbConditionInit0;
120 cdsannotate(SPEC_ANALYSIS, &hb_init0);
122 /* End of Global construct generation in class */
124 /* The following static field declaration is necessary for class */
125 template <typename T>
126 bool CLASS<T>::lock_acquired;
128 template <typename T>
129 int CLASS<T>::reader_lock_cnt;
130 /* End of static field definition */
133 ****** Example2: ******
136 /* Include the header files first */
138 #include <cdsannotate.h>
139 #include <specannotation.h>
140 #include <spec_lib.h>
142 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
145 anno_interface_begin interface_begin;
146 interface_begin.interface_num = 0; // Interface number
147 spec_annotation annotation_interface_begin;
148 annotation_interface_begin.type = INTERFACE_BEGIN;
149 annotation_interface_begin.annotation = &interface_begin;
150 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
152 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
154 // HB conditions (if any)
156 anno_hb_condition hb_condition1;
157 hb_condition1.interface_num = 0; // Interface number
158 hb_condition1.hb_condition_num = 1; // HB condition number
159 spec_annotation annotation_hb_condition;
160 annotation_hb_condition.type = HB_CONDITION;
161 annotation_hb_condition.annotation = &hb_condition;
162 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
167 INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
168 info->__RET__ = __RET__;
171 anno_interface_end interface_end;
172 interface_end.interface_num = 0; // Interface number
173 interface_end.info = info; // Info
174 spec_annotation annotation_interface_end;
175 annotation_interface_end.type = INTERFACE_END;
176 annotation_interface_end.annotation = &interface_end;
177 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
181 ****** Example3: ******
182 Potential Commit Point
186 #include <cdsannotate.h>
188 /* Should add the __ATOMIC_RET__ if necessary */
189 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
191 if (POTENTIAL_CP_DEFINE_CONDITION) {
192 anno_potential_cp_define potential_cp_define;
193 potential_cp_define.label_num = 1; // Commit point label number
194 spec_annotation annotation_potential_cp_define;
195 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
196 annotation_potential_cp_define.annotation = &potential_cp_define;
197 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
200 ****** Example4: ******
204 #include <cdsannotate.h>
207 /* Should add the __ATOMIC_RET__ if necessary */
208 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
210 /* For all the interface check at this commit point (if there is multiple
212 // Commit point 3 <=> potentialCP 4
213 if (COMMIT_POINT3_CONDITION) {
214 anno_cp_define cp_define;
215 cp_define.label_num = 3;
216 cp_define.potential_cp_label_num = 1;
217 spec_annotation annotation_cp_define;
218 annotation_cp_define.type = CP_DEFINE;
219 annotation_cp_define.annotation = &cp_define;
220 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
222 // More if there are any
227 ***** Example5: ******
228 Commit Point Define Check
232 #include <cdsannotate.h>
235 /* Should add the __ATOMIC_RET__ if necessary */
236 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
239 /* For all the interface check at this commit point (if there is multiple
241 if (COMMIT_POINT3_CONDITION) {
242 anno_cp_define cp_define;
243 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
244 bool check_passed = false;
245 cp_define.check_passed = check_passed;
246 cp_define.interface_num = interface_num;
247 cp_define.label_num = 3;
248 cp_define.call_sequence_num = call_sequence_num;
249 spec_annotation annotation_cp_define;
250 annotation_cp_define.type = CP_DEFINE;
251 annotation_cp_define.annotation = &cp_define;
252 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
254 // More if there are any