X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=notes%2Fgenerated_code_examples.txt;h=2a7241c6156c00721d753f8592f1ab9938a779ec;hb=d1da7bb66eab25dfab97f46d9e2c34cdbf380a31;hp=e1eed1936eace4c99bd83304791d5f8ba7321336;hpb=589dca6c19ba28251d70ef9ac3f757b6532d9c82;p=cdsspec-compiler.git diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt index e1eed19..2a7241c 100644 --- a/notes/generated_code_examples.txt +++ b/notes/generated_code_examples.txt @@ -1,41 +1,112 @@ ****** 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 +#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 */ + + + +/* 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; + + // __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 +} + -/* Beginning of struct Sequential */ -typedef struct Sequential { - spec_private_hashtable interface; - Tag global_call_sequence; +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.interface); - init(&global_call_sequence); + /* 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; + /* 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; @@ -48,12 +119,15 @@ void __sequential_init() { hb_init0.annotation = &hbConditionInit0; cdsannotate(SPEC_ANALYSIS, &hb_init0); } +/* End of Global construct generation in class */ -/* All other user-defined functions */ -ALL_USER_DEFINED_FUNCTIONS - -#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: ****** @@ -63,23 +137,16 @@ Interface Wrapper #include #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; + 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); @@ -89,19 +156,24 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) 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); } @@ -109,99 +181,46 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2) ****** Example3: ****** Potential Commit Point -#include -#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) +/* Should add the __ATOMIC_RET__ if necessary */ +uint64_t __ATOMIC_RET = somevar.compare_exchange_explicit(...); -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> +#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 + } @@ -210,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 + }