****** 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 /* Beginning of struct Sequential */ typedef struct Sequential { spec_private_hashtable cond; spec_private_hashtable id; spec_private_hashtable interface; spec_private_hashtable interface_call_sequence; /* DefineVar unfolded here */ spec_private_hashtable Put__Old_Val; /* Beginning of other user-defined variables */ bool lock_acquired; int reader_lock_cnt; /* End of other user-defined variables */ } Sequential; /* End of struct Sequential */ /* Instance of the struct */ Sequential __sequential; /* Define function for sequential code initialization */ void __sequential_init() { /* Init internal variables */ init(&__sequential.cond); init(&__sequential.id); init(&__sequential.interface); init(&__sequential.interface_call_sequence); /* Init DefineVars */ init(&__sequential.Put__Old_Val); /* Init user-defined variables */ lock_acquired = false; reader_lock_cnt = 0; } /* All other user-defined functions */ ALL_USER_DEFINED_FUNCTIONS #endif ****** Example2: ****** Interface Wrapper /* Include the header files first */ #include #include #include TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) { thrd_t tid = thrd_current(); uint64_t call_sequence_num = current(&__interface_call_sequence); put(&__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); int __COND__ = get(&__sequential.cond, tid); uint64_t __ID__ = get(&__sequential.id, tid); /* Post_check action, define macros for all DefineVars */ #define _Old_Val (get(&__sequential.put__Old_Val, tid)) // And more... bool post_check_passed = INTERFACE_POST_CHECK_CONDITION; #undef _Old_Val // And more... anno_post_check post_check; post_check.check_passed = post_check_passed; post_check.interface_num = interface_num; post_check.call_sequence_num = call_sequence_num; spec_annotation annotation_post_check; annotation_post_check.type = POST_CHECK; annotation_post_check.annotation = &post_check; cdsannotate(SPEC_ANALYSIS, &annotation_post_check); // Post Action (if any) POST_ACTION_CODE // Unfolded in place // 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> thrd_t __tid = thrd_current(); uint64_t __ATOMIC_RET__ = get_prev_value(tid); if (POTENTIAL_CP_DEFINE_CONDITION) { uint64_t call_sequence_num = get(&__sequential.interface_call_sequence, tid); int interface_num = get(&__sequential.interface, tid); anno_potential_cp_define potential_cp_define; potential_cp_define.interface_num = interface_num; 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); } ****** 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; }