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 the happens-before initialization here */
102 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
103 anno_hb_init hbConditionInit0;
104 hbConditionInit0.interface_num_before = 1;
105 hbConditionInit0.hb_condition_num_before = 1;
106 hbConditionInit0.interface_num_after = 2;
107 hbConditionInit0.hb_condition_num_after = 0;
108 spec_annotation hb_init0;
109 hb_init0.type = HB_INIT;
110 hb_init0.annotation = &hbConditionInit0;
111 cdsannotate(SPEC_ANALYSIS, &hb_init0);
113 /* End of Global construct generation in class */
115 /* The following static field declaration is necessary for class */
116 template <typename T>
117 bool CLASS<T>::lock_acquired;
119 template <typename T>
120 int CLASS<T>::reader_lock_cnt;
121 /* End of static field definition */
124 ****** Example2: ******
127 /* Include the header files first */
129 #include <cdsannotate.h>
130 #include <specannotation.h>
131 #include <spec_lib.h>
133 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
136 anno_interface_begin interface_begin;
137 interface_begin.interface_num = 0; // Interface number
138 spec_annotation annotation_interface_begin;
139 annotation_interface_begin.type = INTERFACE_BEGIN;
140 annotation_interface_begin.annotation = &interface_begin;
141 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
143 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
145 // HB conditions (if any)
147 anno_hb_condition hb_condition1;
148 hb_condition1.interface_num = 0; // Interface number
149 hb_condition1.hb_condition_num = 1; // HB condition number
150 spec_annotation annotation_hb_condition;
151 annotation_hb_condition.type = HB_CONDITION;
152 annotation_hb_condition.annotation = &hb_condition;
153 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
158 INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
159 info->__RET__ = __RET__;
162 anno_interface_end interface_end;
163 interface_end.interface_num = 0; // Interface number
164 interface_end.info = info; // Info
165 spec_annotation annotation_interface_end;
166 annotation_interface_end.type = INTERFACE_END;
167 annotation_interface_end.annotation = &interface_end;
168 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
172 ****** Example3: ******
173 Potential Commit Point
177 #include <cdsannotate.h>
179 /* Should add the __ATOMIC_RET__ if necessary */
180 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
182 if (POTENTIAL_CP_DEFINE_CONDITION) {
183 anno_potential_cp_define potential_cp_define;
184 potential_cp_define.label_num = 1; // Commit point label number
185 spec_annotation annotation_potential_cp_define;
186 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
187 annotation_potential_cp_define.annotation = &potential_cp_define;
188 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
191 ****** Example4: ******
195 #include <cdsannotate.h>
198 /* Should add the __ATOMIC_RET__ if necessary */
199 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
201 /* For all the interface check at this commit point (if there is multiple
203 // Commit point 3 <=> potentialCP 4
204 if (COMMIT_POINT3_CONDITION) {
205 anno_cp_define cp_define;
206 cp_define.label_num = 3;
207 cp_define.potential_cp_label_num = 1;
208 spec_annotation annotation_cp_define;
209 annotation_cp_define.type = CP_DEFINE;
210 annotation_cp_define.annotation = &cp_define;
211 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
213 // More if there are any
218 ***** Example5: ******
219 Commit Point Define Check
223 #include <cdsannotate.h>
226 /* Should add the __ATOMIC_RET__ if necessary */
227 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
230 /* For all the interface check at this commit point (if there is multiple
232 if (COMMIT_POINT3_CONDITION) {
233 anno_cp_define cp_define;
234 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
235 bool check_passed = false;
236 cp_define.check_passed = check_passed;
237 cp_define.interface_num = interface_num;
238 cp_define.label_num = 3;
239 cp_define.call_sequence_num = call_sequence_num;
240 spec_annotation annotation_cp_define;
241 annotation_cp_define.type = CP_DEFINE;
242 annotation_cp_define.annotation = &cp_define;
243 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
245 // More if there are any