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
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() {
36 static id_t Get_id() {
40 /* End of ID functions */
42 /* Initialization of interface<->function_ptr table */
43 #define INTERFACE_SIZE 2
44 void* func_ptr_table[INTERFACE_SIZE * 2] = {
47 /* Check_action function of interfaces */
48 bool Put_check_action(void *info, id_t __ID__) {
50 Put_info *theInfo = (Put_info) info;
51 shared_ptr<TypeV> __RET__ = theInfo->__RET__;
52 TypeK & key = theInfo->key;
53 TypeV & value = theInfo->value;
56 bool __COND_SAT__ = PUT_CONDITION;
59 check_passed = PUT_CHECK_EXPRESSION;
67 check_passed = PUT_POST_CHECK_EXPRESSION;
76 bool Get_check_action(void *info, id_t __ID__) {
79 /* End of check_action function definitions */
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 user-defined variables */
91 lock_acquired = false;
94 /* Pass the happens-before initialization here */
95 /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */
96 anno_hb_init hbConditionInit0;
97 hbConditionInit0.interface_num_before = 1;
98 hbConditionInit0.hb_condition_num_before = 1;
99 hbConditionInit0.interface_num_after = 2;
100 hbConditionInit0.hb_condition_num_after = 0;
101 spec_annotation hb_init0;
102 hb_init0.type = HB_INIT;
103 hb_init0.annotation = &hbConditionInit0;
104 cdsannotate(SPEC_ANALYSIS, &hb_init0);
106 /* End of Global construct generation in class */
108 /* The following static field declaration is necessary for class */
109 template <typename T>
110 bool CLASS<T>::lock_acquired;
112 template <typename T>
113 int CLASS<T>::reader_lock_cnt;
114 /* End of static field definition */
117 ****** Example2: ******
120 /* Include the header files first */
122 #include <cdsannotate.h>
123 #include <specannotation.h>
124 #include <spec_lib.h>
126 TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
129 anno_interface_begin interface_begin;
130 interface_begin.interface_num = 0; // Interface number
131 spec_annotation annotation_interface_begin;
132 annotation_interface_begin.type = INTERFACE_BEGIN;
133 annotation_interface_begin.annotation = &interface_begin;
134 cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
136 TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
138 // HB conditions (if any)
140 anno_hb_condition hb_condition1;
141 hb_condition1.interface_num = 0; // Interface number
142 hb_condition1.hb_condition_num = 1; // HB condition number
143 spec_annotation annotation_hb_condition;
144 annotation_hb_condition.type = HB_CONDITION;
145 annotation_hb_condition.annotation = &hb_condition;
146 cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition);
151 spec_annotation annotation_interface_end;
152 INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info));
153 info->__RET__ = __RET__;
156 anno_interface_end interface_end;
157 interface_end.interface_num = 0; // Interface number
158 interface_end.info = info; // Info
159 annotation_interface_end.type = INTERFACE_END;
160 annotation_interface_end.annotation = &interface_end;
161 cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
165 ****** Example3: ******
166 Potential Commit Point
170 #include <cdsannotate.h>
172 /* Should add the __ATOMIC_RET__ if necessary */
173 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
175 if (POTENTIAL_CP_DEFINE_CONDITION) {
176 anno_potential_cp_define potential_cp_define;
177 potential_cp_define.label_num = 1; // Commit point label number
178 spec_annotation annotation_potential_cp_define;
179 annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE;
180 annotation_potential_cp_define.annotation = &potential_cp_define;
181 cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
184 ****** Example4: ******
188 #include <cdsannotate.h>
191 /* Should add the __ATOMIC_RET__ if necessary */
192 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
194 /* For all the interface check at this commit point (if there is multiple
196 // Commit point 3 <=> potentialCP 4
197 if (COMMIT_POINT3_CONDITION) {
198 anno_cp_define cp_define;
199 cp_define.label_num = 3;
200 cp_define.potential_cp_label_num = 1;
201 spec_annotation annotation_cp_define;
202 annotation_cp_define.type = CP_DEFINE;
203 annotation_cp_define.annotation = &cp_define;
204 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
206 // More if there are any
211 ***** Example5: ******
212 Commit Point Define Check
216 #include <cdsannotate.h>
219 /* Should add the __ATOMIC_RET__ if necessary */
220 uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...);
223 /* For all the interface check at this commit point (if there is multiple
225 if (COMMIT_POINT3_CONDITION) {
226 anno_cp_define cp_define;
227 uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid);
228 bool check_passed = false;
229 cp_define.check_passed = check_passed;
230 cp_define.interface_num = interface_num;
231 cp_define.label_num = 3;
232 cp_define.call_sequence_num = call_sequence_num;
233 spec_annotation annotation_cp_define;
234 annotation_cp_define.type = CP_DEFINE;
235 annotation_cp_define.annotation = &cp_define;
236 cdsannotate(SPEC_ANALYSIS, &annotation_cp_define);
238 // More if there are any