--- /dev/null
+#include <atomic>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
+#include "librace.h"
+
+
+
+typedef struct Data {
+ int data1;
+ int data2;
+} Data;
+
+atomic<Data*> data;
+
+/* All other user-defined structs */
+static IntegerList * set;
+/* All other user-defined functions */
+inline static call_id_t getID ( int64_t d1 , int64_t d2 ) {
+return d1 + d2 ;
+}
+
+inline static bool print ( int64_t p ) {
+Data * d = ( Data * ) p ;
+model_print ( "Elem-> d1 = %d, d2 = %d\n" , d -> data1 , d -> data2 ) ;
+}
+bool equal ( int64_t p1 , int64_t p2 ) {
+if ( ! p1 || ! p2 ) return false ;
+Data * d1 = ( Data * ) p1 ;
+Data * d2 = ( Data * ) p2 ;
+if ( d1 -> data1 == d2 -> data1 && d1 -> data2 == d2 -> data2 ) {
+return true ;
+}
+else {
+return false ;
+}
+}
+
+inline static void _write ( int64_t d1 , int64_t d2 ) {
+Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
+d -> data1 = d1 ;
+d -> data2 = d2 ;
+push_back ( set , ( int64_t ) d ) ;
+}
+
+inline static bool _read ( Data * res ) {
+bool hasElem = has_elem_by_value ( set , ( int64_t ) res , & equal ) ;
+return hasElem ;
+}
+
+/* Definition of interface info struct: Write */
+typedef struct Write_info {
+Data * __RET__;
+int d1;
+int d2;
+} Write_info;
+/* End of info struct definition: Write */
+
+/* ID function of interface: Write */
+inline static call_id_t Write_id(void *info, thread_id_t __TID__) {
+ Write_info* theInfo = (Write_info*)info;
+ Data * __RET__ = theInfo->__RET__;
+ int d1 = theInfo->d1;
+ int d2 = theInfo->d2;
+
+ call_id_t __ID__ = getID ( d1 , d2 ) ;;
+ return __ID__;
+}
+/* End of ID function: Write */
+
+/* Check action function of interface: Write */
+inline static bool Write_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Write_info* theInfo = (Write_info*)info;
+ Data * __RET__ = theInfo->__RET__;
+ int d1 = theInfo->d1;
+ int d2 = theInfo->d2;
+
+ _write ( d1 , d2 ) ;
+ return true;
+}
+/* End of check action function: Write */
+
+/* Definition of interface info struct: Read */
+typedef struct Read_info {
+Data * __RET__;
+} Read_info;
+/* End of info struct definition: Read */
+
+/* ID function of interface: Read */
+inline static call_id_t Read_id(void *info, thread_id_t __TID__) {
+ Read_info* theInfo = (Read_info*)info;
+ Data * __RET__ = theInfo->__RET__;
+
+ call_id_t __ID__ = getID ( __RET__ -> data1 , __RET__ -> data2 );
+ return __ID__;
+}
+/* End of ID function: Read */
+
+/* Check action function of interface: Read */
+inline static bool Read_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Read_info* theInfo = (Read_info*)info;
+ Data * __RET__ = theInfo->__RET__;
+
+ check_passed = _read ( __RET__ ) ;;
+ if (!check_passed)
+ return false;
+ return true;
+}
+/* End of check action function: Read */
+
+#define INTERFACE_SIZE 2
+static void** func_ptr_table;
+static hb_rule** hb_rule_table;
+static commutativity_rule** commutativity_rule_table;
+inline static bool CommutativityCondition0(void *info1, void *info2) {
+ Write_info *_info1 = (Write_info*) info1;
+ Read_info *_info2 = (Read_info*) info2;
+ return true;
+}
+
+/* Initialization of sequential varialbes */
+static void __SPEC_INIT__() {
+ set = createIntegerList ( ) ;
+ Data * d = ( Data * ) MODEL_MALLOC ( sizeof ( Data ) ) ;
+ d -> data1 = 0 ;
+ d -> data2 = 0 ;
+ push_back ( set , ( int64_t ) d ) ;
+}
+
+/* Cleanup routine of sequential variables */
+static bool __SPEC_CLEANUP__() {
+ if ( set ) destroyIntegerList ( set ) ;
+ return true ;
+}
+
+/* Define function for sequential code initialization */
+inline static void __sequential_init() {
+ /* Init func_ptr_table */
+ func_ptr_table = (void**) malloc(sizeof(void*) * 2 * 2);
+ func_ptr_table[2 * 1] = (void*) &Write_id;
+ func_ptr_table[2 * 1 + 1] = (void*) &Write_check_action;
+ func_ptr_table[2 * 0] = (void*) &Read_id;
+ func_ptr_table[2 * 0 + 1] = (void*) &Read_check_action;
+ /* Write(true) -> Read(true) */
+ struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
+ hbConditionInit0->interface_num_before = 1; // Write
+ hbConditionInit0->hb_condition_num_before = 0; //
+ hbConditionInit0->interface_num_after = 0; // Read
+ hbConditionInit0->hb_condition_num_after = 0; //
+ /* Write(true) -> Write(true) */
+ struct hb_rule *hbConditionInit1 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
+ hbConditionInit1->interface_num_before = 1; // Write
+ hbConditionInit1->hb_condition_num_before = 0; //
+ hbConditionInit1->interface_num_after = 1; // Write
+ hbConditionInit1->hb_condition_num_after = 0; //
+ /* Init hb_rule_table */
+ hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 2);
+ #define HB_RULE_TABLE_SIZE 2
+ hb_rule_table[0] = hbConditionInit0;
+ hb_rule_table[1] = hbConditionInit1;
+ /* Init commutativity_rule_table */
+ commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 1);
+ commutativity_rule* rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 1;
+ rule->interface_num_after = 0;
+ rule->rule = "true";
+ rule->condition = CommutativityCondition0;
+ commutativity_rule_table[0] = rule;
+ /* Pass init info, including function table info & HB rules & Commutativity Rules */
+ struct anno_init *anno_init = (struct anno_init*) malloc(sizeof(struct anno_init));
+ anno_init->init_func = (void_func_t) __SPEC_INIT__;
+ anno_init->cleanup_func = (cleanup_func_t) __SPEC_CLEANUP__;
+ anno_init->func_table = func_ptr_table;
+ anno_init->func_table_size = INTERFACE_SIZE;
+ anno_init->hb_rule_table = hb_rule_table;
+ anno_init->hb_rule_table_size = HB_RULE_TABLE_SIZE;
+ anno_init->commutativity_rule_table = commutativity_rule_table;
+ anno_init->commutativity_rule_table_size = 1;
+ struct spec_annotation *init = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ init->type = INIT;
+ init->annotation = anno_init;
+ cdsannotate(SPEC_ANALYSIS, init);
+
+}
+
+/* End of Global construct generation in class */
+
+
+Data * __wrapper__read();
+
+Data * read() {
+ /* Interface begins */
+ struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
+ interface_begin->interface_num = 0; // Read
+ interface_begin->interface_name = "Read";
+ struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_interface_begin->type = INTERFACE_BEGIN;
+ annotation_interface_begin->annotation = interface_begin;
+ cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
+ Data * __RET__ = __wrapper__read();
+ struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
+ hb_condition->interface_num = 0; // Read
+ hb_condition->hb_condition_num = 0;
+ struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_hb_condition->type = HB_CONDITION;
+ annotation_hb_condition->annotation = hb_condition;
+ cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
+
+ Read_info* info = (Read_info*) malloc(sizeof(Read_info));
+ info->__RET__ = __RET__;
+ struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
+ interface_end->interface_num = 0; // Read
+ interface_end->info = info;
+ struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annoation_interface_end->type = INTERFACE_END;
+ annoation_interface_end->annotation = interface_end;
+ cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
+ return __RET__;
+}
+
+Data * __wrapper__read() {
+
+ Data *res = data.load(memory_order_acquire);
+ /* Automatically generated code for commit point define check: Read_Success_Point */
+
+ if (true) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 0;
+ cp_define_check->label_name = "Read_Success_Point";
+ cp_define_check->interface_num = 0;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ return res;
+}
+
+Data * __wrapper__write(int d1, int d2);
+
+Data * write(int d1, int d2) {
+ /* Interface begins */
+ struct anno_interface_begin *interface_begin = (struct anno_interface_begin*) malloc(sizeof(struct anno_interface_begin));
+ interface_begin->interface_num = 1; // Write
+ interface_begin->interface_name = "Write";
+ struct spec_annotation *annotation_interface_begin = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_interface_begin->type = INTERFACE_BEGIN;
+ annotation_interface_begin->annotation = interface_begin;
+ cdsannotate(SPEC_ANALYSIS, annotation_interface_begin);
+ Data * __RET__ = __wrapper__write(d1, d2);
+ struct anno_hb_condition *hb_condition = (struct anno_hb_condition*) malloc(sizeof(struct anno_hb_condition));
+ hb_condition->interface_num = 1; // Write
+ hb_condition->hb_condition_num = 0;
+ struct spec_annotation *annotation_hb_condition = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_hb_condition->type = HB_CONDITION;
+ annotation_hb_condition->annotation = hb_condition;
+ cdsannotate(SPEC_ANALYSIS, annotation_hb_condition);
+
+ Write_info* info = (Write_info*) malloc(sizeof(Write_info));
+ info->__RET__ = __RET__;
+ info->d1 = d1;
+ info->d2 = d2;
+ struct anno_interface_end *interface_end = (struct anno_interface_end*) malloc(sizeof(struct anno_interface_end));
+ interface_end->interface_num = 1; // Write
+ interface_end->info = info;
+ struct spec_annotation *annoation_interface_end = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annoation_interface_end->type = INTERFACE_END;
+ annoation_interface_end->annotation = interface_end;
+ cdsannotate(SPEC_ANALYSIS, annoation_interface_end);
+ return __RET__;
+}
+
+Data * __wrapper__write(int d1, int d2) {
+ bool succ = false;
+ Data *tmp = (Data*) malloc(sizeof(Data));
+ do {
+
+ Data *prev = data.load(memory_order_acquire);
+ tmp->data1 = d1;
+ tmp->data2 = d2;
+
+ succ = data.compare_exchange_strong(prev, tmp,
+ memory_order_release, memory_order_relaxed);
+ /* Automatically generated code for commit point define check: Write_Success_Point */
+
+ if (succ) {
+ struct anno_cp_define_check *cp_define_check = (struct anno_cp_define_check*) malloc(sizeof(struct anno_cp_define_check));
+ cp_define_check->label_num = 1;
+ cp_define_check->label_name = "Write_Success_Point";
+ cp_define_check->interface_num = 1;
+ struct spec_annotation *annotation_cp_define_check = (struct spec_annotation*) malloc(sizeof(struct spec_annotation));
+ annotation_cp_define_check->type = CP_DEFINE_CHECK;
+ annotation_cp_define_check->annotation = cp_define_check;
+ cdsannotate(SPEC_ANALYSIS, annotation_cp_define_check);
+ }
+
+ } while (!succ);
+ return tmp;
+}
+
+
+void threadA(void *arg) {
+ write(1, 0);
+}
+
+void threadB(void *arg) {
+ write(0, 2);
+}
+
+void threadC(void *arg) {
+ write(2, 2);
+}
+
+void threadD(void *arg) {
+ Data *d = read();
+ printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
+}
+
+int user_main(int argc, char **argv) {
+ __sequential_init();
+
+
+ thrd_t t1, t2, t3, t4;
+ Data *dataInit = (Data*) malloc(sizeof(Data));
+ dataInit->data1 = 0;
+ dataInit->data2 = 0;
+ atomic_init(&data, dataInit);
+
+ thrd_create(&t1, threadA, NULL);
+ thrd_create(&t2, threadB, NULL);
+ thrd_create(&t4, threadD, NULL);
+
+ thrd_join(t1);
+ thrd_join(t2);
+ thrd_join(t4);
+
+ return 0;
+}
+
projects / cdsspec-compiler.git / blobdiff