generate more structured code

[cdsspec-compiler.git] / notes / generated_code_examples.txt

diff --git a/notes/generated_code_examples.txt b/notes/generated_code_examples.txt
index 5dc22b7c8d495f94aa3b82f9445b555d711002f9..b8d9707544afc3ab69e8541084f4f2c7d794d10d 100644 (file)
--- a/notes/generated_code_examples.txt
+++ b/notes/generated_code_examples.txt
@@ -10,13 +10,15 @@ Global Variable Declaration
 #define __SPEC_SEQUENTIAL_GENERATED_H
 #include <specannotation.h>
 #include <spec_private_hashtable.h>
+#include <spec_tag.h>
 
 /* Beginning of struct Sequential */
 typedef struct Sequential {
-       spec_private_hashtable cond;
+       spec_private_hashtable condition;
        spec_private_hashtable id;
        spec_private_hashtable interface;
        spec_private_hashtable interface_call_sequence;
+       Tag global_call_sequence;
 
        /* DefineVar unfolded here */
        spec_private_hashtable Put__Old_Val;
@@ -34,15 +36,29 @@ Sequential __sequential;
 /* Define function for sequential code initialization */
 void __sequential_init() {
        /* Init internal variables */
-       init(&__sequential.cond);
+       init(&__sequential.condition);
        init(&__sequential.id);
        init(&__sequential.interface);
        init(&__sequential.interface_call_sequence);
+       init(&global_call_sequence);
        /* Init DefineVars */
        init(&__sequential.Put__Old_Val);
        /* 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 */
@@ -59,12 +75,15 @@ Interface Wrapper
 #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;
@@ -76,15 +95,13 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
        cdsannotate(SPEC_ANALYSIS, &annoation_interface_begin);
 
        TypeReturn __RET__ = __wrapper_interfaceName(arg1, arg2);
-       int __COND__ = get(&__sequential.cond, tid);
+       int __COND__ = get(&__sequential.condition, 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;
@@ -97,13 +114,15 @@ TypeReturn interfaceName(ARGType1 arg1, ARGType2 arg2)
 
        // 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.id = __ID__;
                hb_condition1.call_sequence_num = call_sequence_num;
                spec_annotation annotation_hb_condition;
                annotation_hb_condition.type = HB_CONDITION;
@@ -129,13 +148,13 @@ Potential Commit Point
 #include <spec_private_hashtable.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;