--- /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
+
+ ";");
// __ID__
newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_ID + ";");
-
// DefineVars
for (String interfaceName : _semantics.interfaceName2Construct.keySet()) {
InterfaceConstruct iConstruct = (InterfaceConstruct) _semantics.interfaceName2Construct
+ ";");
}
}
-
// __interface
newCode.add(CodeVariables.SPEC_HASHTABLE + CodeVariables.SPEC_INTERFACE
+ ";");
-
+ // __interface_call_sequence
+ newCode.add(CodeVariables.SPEC_HASHTABLE
+ + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ";");
+ // Interface call sequence varaiable
+ newCode.add(CodeVariables.SPEC_TAG + " "
+ + CodeVariables.INTERFACE_CALL_SEQUENCE + ";");
// End of the struct
newCode.add("}");
}
// __interface
newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE + ");");
+ // __interface_call_sequence
+ newCode.add("init_table(&" + CodeVariables.SPEC_INTERFACE_CALL_SEQUENCE + ");");
// Pass the happens-before relationship check here
newCode.addAll(CodeVariables.generateHBInitAnnotation(_semantics));
newCode.add("\n");
-
+
// Generate the sequential functions
breakCodeLines(newCode, globalCode.defineFunc);
}
// Generate new wrapper
- breakCodeLines(newCode, funcDecl);
+ /**
+ *
+ *
+ */
+ breakCodeLines(newCode, funcDecl);
newCode.add("{");
-
- // Generate
-
+ // Generate interface sequence call
+ newCode.add(CodeVariables.UINT64 + " call_sequence_num = current(&"
+ + CodeVariables.INTERFACE_CALL_SEQUENCE + ");");
// FIXME: Add Happens-before check here
-
newCode.add("}");
+
CodeAddition addition = new CodeAddition(lineNum, newCode);
if (!codeAdditions.containsKey(inst.file)) {
codeAdditions.put(inst.file, new ArrayList<CodeAddition>());
public class CodeVariables {
// C++ code or library
- public static final String ThreadIDType = "thread_id_t";
+ public static final String HEADER_threads = "threads.h";
+ public static final String ThreadIDType = "thrd_t";
+ public static final String GET_THREAD_ID = "thrd_current";
public static final String BOOLEAN = "bool";
+ public static final String UINT64 = "uint64_t";
// Model checker code
public static final String HEADER_CDSAnnotate = "cdsannotate.h";
+ public static final String HEADER_SPECANNOTATION = "specannotation.h";
public static final String CDSAnnotate = "cdsannotate";
public static final String CDSAnnotateType = "SPEC_ANALYSIS";
+ // It's a SPEC_TAG type, it has current() and next() function
+ public static final String INTERFACE_CALL_SEQUENCE = "__interface_call_sequence";
public static final String SPEC_ANNOTATION_TYPE = "spec_anno_type";
public static final String SPEC_ANNOTATION = "spec_annotation";
public static final String ANNO_HB_INIT = "anno_hb_init";
- public static final String ANNO_INTERFACE_BEGIN = "anno_interface_begin";
- public static final String ANNO_INTERFACE_END = "anno_interface_end";
+ public static final String ANNO_INTERFACE_BOUNDARY = "anno_interface_boundary";
public static final String ANNO_ID = "anno_id";
public static final String ANNO_POTENTIAL_CP_DEFINE = "anno_potentail_cp_define";
public static final String ANNO_CP_DEFINE = "anno_cp_define";
public static final String SPEC_STRUCT = "Sequential";
public static final String SPEC_INSTANCE = "__sequential";
- public static final String SPEC_CONDITION = "__cond";
- public static final String SPEC_ID = "__id";
- public static final String SPEC_INTERFACE = "__interface";
+ public static final String SPEC_CONDITION = "condition";
+ public static final String SPEC_ID = "id";
+ public static final String SPEC_INTERFACE = "interface";
+ public static final String SPEC_INTERFACE_CALL_SEQUENCE = "interface_call_sequence";
public static final String SPEC_INTERFACE_WRAPPER = "__wrapper_";
public static final String SPEC_QUEUE = "spec_queue";
public static final String SPEC_STACK = "spec_stack";
public static final String SPEC_HASHTABLE = "spec_hashtable";
+ public static final String SPEC_PRIVATE_HASHTABLE = "spec_private_hashtable";
public static final String SPEC_TAG = "spec_tag";
// Macro