X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=notes%2Fgenerated_code_examples.txt;h=2a7241c6156c00721d753f8592f1ab9938a779ec;hp=5dc22b7c8d495f94aa3b82f9445b555d711002f9;hb=40ad7bdbe6db661c513c66e350ebfa479cb94765;hpb=d9c5f3639af2eaa7a35b7242c846f657b875657c;ds=sidebyside diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index 5dc22b7..2a7241c 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -1,55 +1,133 @@ ****** 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 all the header files that contains the interface declaration */ +#inlcude +#include +#include + +/* Other necessary header files */ +#include #include -#include +#include + +/* All other user-defined functions */ +ALL_USER_DEFINED_FUNCTIONS // Make them static + +/* 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 */ + +/* ID functions of interface */ +static id_t Put_id() { + id_t id = PUT_ID; // Default ID == 0; + return id; +} + +static id_t Get_id() { + id_t id = GET_ID; + return id; +} +/* End of ID functions */ + + -/* 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; +/* Check_action function of interfaces */ +bool Put_check_action(void *info, id_t __ID__) { + bool check_passed; + Put_info *theInfo = (Put_info) info; + shared_ptr __RET__ = theInfo->__RET__; + TypeK & key = theInfo->key; + TypeV & value = theInfo->value; - /* DefineVar unfolded here */ - spec_private_hashtable Put__Old_Val; + // __COND_SAT__ + bool __COND_SAT__ = PUT_CONDITION; + + // Check + check_passed = PUT_CHECK_EXPRESSION; + if (!check_passed) + return false; + + // Action + PUT_ACTION + + // Post_check + check_passed = PUT_POST_CHECK_EXPRESSION; + if (!check_passed) + return false; + + // Post_action + PUT_POST_ACTION +} + + +bool Get_check_action(void *info, id_t __ID__) { + //... +} +/* End of check_action function definitions */ - /* Beginning of other user-defined variables */ - bool lock_acquired; - int reader_lock_cnt; - /* End of other user-defined variables */ +/* Initialization of interface<->function_ptr table */ +#define INTERFACE_SIZE 2 +void** func_ptr_table; -} Sequential; /* End of struct Sequential */ +/* Beginning of other user-defined variables */ +bool lock_acquired; +int reader_lock_cnt; +/* End of other user-defined variables */ -/* 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 func_ptr_table */ + func_ptr_table = (void**) malloc(sizeof(void*) * 2); + func_ptr_table[0] = (void*) &Put_id; + func_ptr_table[1] = (void*) &Put_check_action; + func_ptr_table[2] = (void*) &Get_id; + func_ptr_table[3] = (void*) &Get_check_action; + /* Init user-defined variables */ lock_acquired = false; reader_lock_cnt = 0; -} -/* All other user-defined functions */ -ALL_USER_DEFINED_FUNCTIONS + /* Pass function table info */ + anno_func_table_init func_table; + func_table.size = INTERFACE_SIZE; + func_table.table = func_ptr_table; + spec_annotation func_init; + func_init.type = FUNC_TABLE_INIT; + func_init.annotation = &anno_func_table_init; + cdsannotate(SPEC_ANALYSIS, &func_init); + + /* 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); +} +/* End of Global construct generation in class */ -#endif +/* The following static field declaration is necessary for class */ +template +bool CLASS::lock_acquired; +template +int CLASS::reader_lock_cnt; +/* End of static field definition */ ****** Example2: ****** @@ -59,63 +137,43 @@ Interface Wrapper #include #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; + anno_interface_begin interface_begin; + interface_begin.interface_num = 0; // Interface number spec_annotation annotation_interface_begin; annotation_interface_begin.type = INTERFACE_BEGIN; - annotation_interface_begin.annotation = &interface_boundary; + annotation_interface_begin.annotation = &interface_begin; 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) } + // And more (if any) // Interface ends + INTERFACE_LABEL_info info = (INTERFACE_LABEL_info*) malloc(sizeof(INTERFACE_LABEL_info)); + info->__RET__ = __RET__; + info->arg1 = arg1; + info->arg2 = arg2; + anno_interface_end interface_end; + interface_end.interface_num = 0; // Interface number + interface_end.info = info; // Info spec_annotation annotation_interface_end; annotation_interface_end.type = INTERFACE_END; - annotation_interface_end.annotation = &interface_boundary; + annotation_interface_end.annotation = &interface_end; cdsannotate(SPEC_ANALYSIS, &annoation_interface_end); } @@ -123,21 +181,16 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) ****** Example3: ****** Potential Commit Point -#include -#include + +#include #include -#include -#include <_sepc_sequential_genenrated.h> -thrd_t __tid = thrd_current(); -uint64_t __ATOMIC_RET__ = get_prev_value(tid); +/* Should add the __ATOMIC_RET__ if necessary */ +uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...); + 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; @@ -148,65 +201,26 @@ if (POTENTIAL_CP_DEFINE_CONDITION) { Commit Point Define #include -#include #include -#include -#include <_spec_sequential_generated.h> +#include + +/* Should add the __ATOMIC_RET__ if necessary */ +uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...); -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; +// Commit point 3 <=> potentialCP 4 +if (COMMIT_POINT3_CONDITION) { + anno_cp_define cp_define; + cp_define.label_num = 3; + cp_define.potential_cp_label_num = 1; + spec_annotation annotation_cp_define; + annotation_cp_define.type = CP_DEFINE; + annotation_cp_define.annotation = &cp_define; + cdsannotate(SPEC_ANALYSIS, &annotation_cp_define); +} +// More if there are any + } @@ -215,62 +229,28 @@ Commit Point Define Check #include -#include #include -#include -#include <_spec_sequential_generated.h> +#include + +/* Should add the __ATOMIC_RET__ if necessary */ +uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...); -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; +if (COMMIT_POINT3_CONDITION) { + 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); +} +// More if there are any + }