****** 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 <specannotation.h>
-#include <spec_tag.h>
-
/* Include all the header files that contains the interface declaration */
-#include <iostream>
#inlcude <atomic>
#include <memory>
#include <assert.h>
+/* Other necessary header files */
+#include <stdint.h>
+#include <specannotation.h>
+#include <spec_lib.h>
+
/* All other user-defined functions */
-ALL_USER_DEFINED_FUNCTIONS
+ALL_USER_DEFINED_FUNCTIONS // Make them static
/* Definition of interface info struct (per interface) */
typedef struct Put_info {
} 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 */
+
+
-/* All function of action and check of interfaces */
-bool Put_check_action(void *info) {
+/* 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;
+ // __COND_SAT__
+ bool __COND_SAT__ = PUT_CONDITION;
+
// Check
check_passed = PUT_CHECK_EXPRESSION;
if (!check_passed)
// Action
PUT_ACTION
- /* DefineVars */
- TypeV *_Old_Val = DefineVarExpr;
-
// Post_check
check_passed = PUT_POST_CHECK_EXPRESSION;
if (!check_passed)
PUT_POST_ACTION
}
-id_t Put_id() {
- id_t id = PUT_ID;
- return id;
+
+bool Get_check_action(void *info, id_t __ID__) {
+ //...
}
+/* End of check_action function definitions */
+/* Initialization of interface<->function_ptr table */
+#define INTERFACE_SIZE 2
+void** func_ptr_table;
/* Beginning of other user-defined variables */
bool lock_acquired;
/* Define function for sequential code initialization */
void __sequential_init() {
+ /* 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;
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_tag.h>
-#include <spec_private_hashtable.h>
+#include <spec_lib.h>
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);
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>
-// 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 <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