****** Example1: ****** Global Variable Declaration /* Include the header files first ** This declaration will be written into a header file */ /* @file _spec_sequential_generated.h */ /* @brief automatically generated file */ #ifndef __SPEC_SEQUENTIAL_GENERATED_H #define __SPEC_SEQUENTIAL_GENERATED_H #include #include /* Include all the header files that contains the interface declaration */ #include #inlcude #include #include /* All other user-defined functions */ ALL_USER_DEFINED_FUNCTIONS /* Definition of interface info struct (per interface) */ typedef struct Put_info { shared_ptr __RET__; TypeK & key; TypeV & value; } Put_info; typedef struct Get_info { shared_ptr __RET__; TypeK & key; } Get_info; /* End of info struct definition */ /* All function of action and check of interfaces */ bool Put_check_action(void *info) { bool check_passed; Put_info *theInfo = (Put_info) info; shared_ptr __RET__ = theInfo->__RET__; TypeK & key = theInfo->key; TypeV & value = theInfo->value; // Check check_passed = PUT_CHECK_EXPRESSION; if (!check_passed) return false; // Action PUT_ACTION /* DefineVars */ TypeV *_Old_Val = DefineVarExpr; // Post_check check_passed = PUT_POST_CHECK_EXPRESSION; if (!check_passed) return false; // Post_action PUT_POST_ACTION } id_t Put_id() { id_t id = PUT_ID; return id; } /* Beginning of other user-defined variables */ bool lock_acquired; int reader_lock_cnt; /* End of other user-defined variables */ /* Define function for sequential code initialization */ void __sequential_init() { /* Init user-defined variables */ lock_acquired = false; reader_lock_cnt = 0; /* Pass the happens-before initialization here */ /* PutIfAbsent (putIfAbsent_Succ) -> Get (true) */ anno_hb_init hbConditionInit0; hbConditionInit0.interface_num_before = 1; hbConditionInit0.hb_condition_num_before = 1; hbConditionInit0.interface_num_after = 2; hbConditionInit0.hb_condition_num_after = 0; spec_annotation hb_init0; hb_init0.type = HB_INIT; hb_init0.annotation = &hbConditionInit0; cdsannotate(SPEC_ANALYSIS, &hb_init0); } #endif ****** Example2: ****** Interface Wrapper /* Include the header files first */ #include #include #include #include #include TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) { thrd_t tid = thrd_current(); uint64_t call_sequence_num = current(&__sequential.global_call_sequence); next(&__sequential.global_call_sequence); put(&__sequential.interface_call_sequence, tid, call_sequence_num); // Interface begins anno_interface_boundary interface_boundary; interface_boundary.interface_num = 0; // Interface number interface_boundary.call_sequence_num = call_sequence_num; spec_annotation annotation_interface_begin; annotation_interface_begin.type = INTERFACE_BEGIN; annotation_interface_begin.annotation = &interface_boundary; cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin); TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2); // HB conditions (if any) if (HB_CONDITION1) { anno_hb_condition hb_condition1; hb_condition1.interface_num = 0; // Interface number hb_condition1.hb_condition_num = 1; // HB condition number hb_condition1.id = __ID__; hb_condition1.call_sequence_num = call_sequence_num; spec_annotation annotation_hb_condition; annotation_hb_condition.type = HB_CONDITION; annotation_hb_condition.annotation = &hb_condition; cdsannotate(SPEC_ANALYSIS, &annotation_hb_condition); // And more (if any) } // Interface ends spec_annotation annotation_interface_end; annotation_interface_end.type = INTERFACE_END; annotation_interface_end.annotation = &interface_boundary; cdsannotate(SPEC_ANALYSIS, &annoation_interface_end); } ****** Example3: ****** Potential Commit Point #include #include #include #include #include <_sepc_sequential_genenrated.h> // FIXME /* Define MACRO */ #define CAS (__ATOMIC_RET__ = CAS) #define LOAD (__ATOMIC_RET__ = LOAD) #define RMW (__ATOMIC_RET__ = RMW) thrd_t tid = thrd_current(); if (POTENTIAL_CP_DEFINE_CONDITION) { uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid); anno_potential_cp_define potential_cp_define; potential_cp_define.interface_num = get(&__sequential.interface, tid); potential_cp_define.label_num = 1; // Commit point label number potential_cp_define.call_sequence_num = call_sequence_num; spec_annotation annotation_potential_cp_define; annotation_potential_cp_define.type = POTENTIAL_CP_DEFINE; annotation_potential_cp_define.annotation = &potential_cp_define; cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define); } /* Undefine MACRO */ #undef CAS #undef LOAD #undef RMW ****** Example4: ****** Commit Point Define #include #include #include #include #include <_spec_sequential_generated.h> thrd_t __tid = thrd_current(); int interface_num = get(&__sequential.interface, tid); /* For all the interface check at this commit point (if there is multiple * checks here) */ /* Need to compute the relationship between labels before hand */ switch (interface_num) { case 0: // Commit point 3 <=> potentialCP 4 if (COMMIT_POINT3_CONDITION && potential_cp_satisfied(3, 4)) { if (INTERFACE0_CHECK_CONDITION) { check_passed = true; } /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a * pointer) */ /* Unfold all if there are multiple DefineVars */ Type res0 = Expr; put(&__sequential.put__Old_Val, tid, (uint64_t) res0); // And more... /* Compute id; If not defined, assign the default ID */ int id = INTERFACE0_ID_EXPRESSION; put(__sequential.id, tid, id); /* Execute actions if there's any */ #define _Old_Val res0; INTERFACE0_ACTION; // Unfolded right in place #undef _Old_Val // And more... anno_cp_define cp_define; uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid); bool check_passed = false; cp_define.check_passed = check_passed; cp_define.interface_num = interface_num; cp_define.label_num = 3; cp_define.call_sequence_num = call_sequence_num; spec_annotation annotation_cp_define; annotation_cp_define.type = CP_DEFINE; annotation_cp_define.annotation = &cp_define; cdsannotate(SPEC_ANALYSIS, &annotation_cp_define); } break; case 1: // Commit point 5 <=> potentialCP 6 if (COMMIT_POINT5_CONDITION && potential_cp_satisfied(5, 6)) { if (INTERFACE1_CHECK_CONDITION) { check_passed = true; } // ... // Same as the above case } break; default: break; } ***** Example5: ****** Commit Point Define Check #include #include #include #include #include <_spec_sequential_generated.h> thrd_t __tid = thrd_current(); int interface_num = get(&__sequential.interface, tid); /* For all the interface check at this commit point (if there is multiple * checks here) */ /* Need to compute the relationship between labels before hand */ switch (interface_num) { case 0: if (COMMIT_POINT3_CONDITION) { if (INTERFACE0_CHECK_CONDITION) { check_passed = true; } /* For all DefineVar of INTERFACE0 (Type id = Expr) (Type must be a * pointer) */ /* Unfold all if there are multiple DefineVars */ Type res0 = Expr; put(&__sequential.put__Old_Val, tid, (uint64_t) res0); // And more... /* Compute id; If not defined, assign the default ID */ int id = INTERFACE0_ID_EXPRESSION; put(__sequential.id, tid, id); /* Execute actions if there's any */ #define _Old_Val res0; INTERFACE0_ACTION; // Unfolded right in place #undef _Old_Val // And more... anno_cp_define cp_define; uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid); bool check_passed = false; cp_define.check_passed = check_passed; cp_define.interface_num = interface_num; cp_define.label_num = 3; cp_define.call_sequence_num = call_sequence_num; spec_annotation annotation_cp_define; annotation_cp_define.type = CP_DEFINE; annotation_cp_define.annotation = &cp_define; cdsannotate(SPEC_ANALYSIS, &annotation_cp_define); } break; case 1: if (COMMIT_POINT5_CONDITION) { if (INTERFACE1_CHECK_CONDITION) { check_passed = true; } // ... // Same as the above case } break; default: break; }