/* Include the header files first
** This declaration will be written into a header file
*/
-/* @file CDSName.h */
+/* @file _spec_sequential_generated.h */
/* @brief automatically generated file */
-#ifndef _CDSNAME_H
-#define _CDSNAME_H
+#ifndef __SPEC_SEQUENTIAL_GENERATED_H
+#define __SPEC_SEQUENTIAL_GENERATED_H
#include <specannotation.h>
#include <spec_private_hashtable.h>
+#include <spec_tag.h>
-typedef struct Sequential
-{
- spec_private_hashtabel cond;
- spec_private_hashtabel id;
- spec_private_hashtabel interface;
- spec_private_hashtabel interface_call_sequence;
-
- /* DefineVar unfolded here */
- spec_private_hashtable Put__Old_Val;
+/* Beginning of struct Sequential */
+typedef struct Sequential {
+ spec_private_hashtable interface;
+ Tag global_call_sequence;
- /* Other user-defined variables */
+ /* Beginning of other user-defined variables */
bool lock_acquired;
int reader_lock_cnt;
-} Sequential;
+ /* 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.interface);
+ init(&global_call_sequence);
+ /* Init user-defined variables */
+ lock_acquired = false;
+ reader_lock_cnt = 0;
+
+ /* 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);
+}
+
/* All other user-defined functions */
ALL_USER_DEFINED_FUNCTIONS
-
#endif
****** Example2: ******
-Global Variable Initialization (Entry Point Unfolding)
-
-#include <spec_private_hashtable.h>
-#include <CDSName.h>
-
-init(&__sequential.condition);
-init(&__sequential.id);
-init(&__sequential.interface);
-init(&__sequential.interface_call_sequence);
-/* DefineVar initialized here */
-init(&Put__Old_Val);
-
-/* User-define variables */
-lock_acquired = false;
-reader_lock_cnt = 0;
-
-
-
-****** Example3: ******
Interface Wrapper
/* Include the header files first */
#include <threads.h>
#include <cdsannotate.h>
#include <specannotation.h>
+#include <spec_tag.h>
+#include <spec_private_hashtable.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);
+ 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;
annotation_interface_begin.annotation = &interface_boundary;
cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
+ // FIXME:
TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
- bool __COND__ = get(&__cond, tid);
- uint64_t id = get(&__id, tid);
+ int __COND__ = get(&__sequential.condition, tid);
+ uint64_t __ID__ = get(&__sequential.id, tid);
- // 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)
- }
+ /* 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;
- // Post check (if any)
- bool post_check_passed = POST_CHECK_CONDITION;
anno_post_check post_check;
post_check.check_passed = post_check_passed;
post_check.interface_num = interface_num;
// Post Action (if any)
POST_ACTION_CODE // Unfolded in place
+ #undef _Old_Val
+ // And more...
+
+ // 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;
}
-****** Example4: ******
+****** Example3: ******
Potential Commit Point
#include <threads.h>
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_sepc_sequential_genenrated.h>
-thrd_t __tid = thrd_current();
+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.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;
cdsannotate(SPEC_ANALYSIS, &annotation_potential_cp_define);
}
-****** Example5: ******
+****** Example4: ******
Commit Point Define
#include <threads.h>
#include <cdstrace.h>
#include <cdsannotate.h>
#include <spec_private_hashtable.h>
-#include <CDSName.h>
+#include <_spec_sequential_generated.h>
thrd_t __tid = thrd_current();
int interface_num = get(&__sequential.interface, tid);
if (INTERFACE0_CHECK_CONDITION) {
check_passed = true;
}
- /* For all DefineVar of INTERFACE0 (Type id = Expr) */
- FIXME: Type res0 = Expr;
- put(__sequential.put_id, tid,
- #define _Old_Val __sequential.put_id
+ /* 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);
if (INTERFACE1_CHECK_CONDITION) {
check_passed = true;
}
- INTERFACE1_ACTION; // Unfolded right in place
+ // ...
+ // Same as the above case
+ }
+ break;
+ default:
+ break;
+}
+
+
+***** Example5: ******
+Commit Point Define Check
+
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#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 = 5;
+ cp_define.label_num = 3;
cp_define.call_sequence_num = call_sequence_num;
spec_annotation annotation_cp_define;
annotation_cp_define.type = 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;
}
-
-
-***** Example6: ******
-Commit Point Define Check
-
projects / cdsspec-compiler.git / blobdiff