****** 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 <atomic>
+#include <memory>
+#include <assert.h>
+
+/* Other necessary header files */
+#include <stdint.h>
#include <specannotation.h>
-#include <spec_private_hashtable.h>
+#include <spec_lib.h>
+
+/* 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<TypeV> __RET__;
+ TypeK & key;
+ TypeV & value;
+} Put_info;
+
+typedef struct Get_info {
+ shared_ptr<TypeV> __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<TypeV> __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 <typename T>
+bool CLASS<T>::lock_acquired;
+template <typename T>
+int CLASS<T>::reader_lock_cnt;
+/* End of static field definition */
****** Example2: ******
#include <threads.h>
#include <cdsannotate.h>
#include <specannotation.h>
+#include <spec_lib.h>
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);
}
****** Example3: ******
Potential Commit Point
-#include <threads.h>
-#include <cdstrace.h>
+
+#include <stdint.h>
#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#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;
Commit Point Define
#include <threads.h>
-#include <cdstrace.h>
#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
+#include <stdint.h>
+
+/* 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
+
}
#include <threads.h>
-#include <cdstrace.h>
#include <cdsannotate.h>
-#include <spec_private_hashtable.h>
-#include <_spec_sequential_generated.h>
+#include <stdint.h>
+
+/* 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
+
}
projects / cdsspec-compiler.git / blobdiff