--- /dev/null
+****** Example1: ******
+Global Variable Declaration
+
+/* Include the header files first
+** This declaration will be written into a header file
+*/
+/* @file CDSName.h */
+/* @brief automatically generated file */
+#ifndef _CDSNAME_H
+#define _CDSNAME_H
+#include <specannotation.h>
+#include <spec_private_hashtable.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;
+
+ /* Other user-defined variables */
+ bool lock_acquired;
+ int reader_lock_cnt;
+} Sequential;
+
+Sequential __sequential;
+
+/* 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>
+
+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;
+ spec_annotation annotation_interface_begin;
+ annotation_interface_begin.type = INTERFACE_BEGIN;
+ annotation_interface_begin.annotation = &interface_boundary;
+ cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
+
+ TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
+ bool __COND__ = get(&__cond, tid);
+ uint64_t id = get(&__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 (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_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
+
+ // Interface ends
+ spec_annotation annotation_interface_end;
+ annotation_interface_end.type = INTERFACE_END;
+ annotation_interface_end.annotation = &interface_boundary;
+ cdsannotate(SPEC_ANALYSIS, &annoation_interface_end);
+}
+
+
+****** Example4: ******
+Potential Commit Point
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#include <CDSName.h>
+
+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.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);
+}
+
+****** Example5: ******
+Commit Point Define
+
+#include <threads.h>
+#include <cdstrace.h>
+#include <cdsannotate.h>
+#include <spec_private_hashtable.h>
+#include <CDSName.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:
+ // 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) */
+ FIXME: Type res0 = Expr;
+ put(__sequential.put_id, tid,
+ #define _Old_Val __sequential.put_id
+ INTERFACE0_ACTION; // Unfolded right in place
+
+ 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;
+ }
+ INTERFACE1_ACTION; // Unfolded right in place
+
+ 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.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;
+ default:
+ break;
+}
+
+
+***** Example6: ******
+Commit Point Define Check
+
projects / cdsspec-compiler.git / blobdiff