--- /dev/null
+#ifndef DEQUE_H
+#define DEQUE_H
+
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
+typedef struct {
+ atomic_size_t size;
+ atomic_int buffer[];
+} Array;
+
+typedef struct {
+ atomic_size_t top, bottom;
+ atomic_uintptr_t array;
+} Deque;
+
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+/* All other user-defined structs */
+static IntegerList * __deque;
+/* All other user-defined functions */
+inline static bool succ ( int res ) {
+return res != EMPTY && res != ABORT ;
+}
+
+/* Definition of interface info struct: Steal */
+typedef struct Steal_info {
+int __RET__;
+Deque * q;
+} Steal_info;
+/* End of info struct definition: Steal */
+
+/* ID function of interface: Steal */
+inline static call_id_t Steal_id(void *info, thread_id_t __TID__) {
+ Steal_info* theInfo = (Steal_info*)info;
+ int __RET__ = theInfo->__RET__;
+ Deque * q = theInfo->q;
+
+ call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
+ return __ID__;
+}
+/* End of ID function: Steal */
+
+/* Check action function of interface: Steal */
+inline static bool Steal_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Steal_info* theInfo = (Steal_info*)info;
+ int __RET__ = theInfo->__RET__;
+ Deque * q = theInfo->q;
+
+ int elem = 0 ;
+ if ( succ ( __RET__ ) ) {
+ elem = front ( __deque ) ;
+ pop_front ( __deque ) ;
+ }
+ check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
+ if (!check_passed)
+ return false;
+ return true;
+}
+/* End of check action function: Steal */
+
+/* Definition of interface info struct: Take */
+typedef struct Take_info {
+int __RET__;
+Deque * q;
+} Take_info;
+/* End of info struct definition: Take */
+
+/* ID function of interface: Take */
+inline static call_id_t Take_id(void *info, thread_id_t __TID__) {
+ Take_info* theInfo = (Take_info*)info;
+ int __RET__ = theInfo->__RET__;
+ Deque * q = theInfo->q;
+
+ call_id_t __ID__ = succ ( __RET__ ) ? __RET__ : DEFAULT_CALL_ID;
+ return __ID__;
+}
+/* End of ID function: Take */
+
+/* Check action function of interface: Take */
+inline static bool Take_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Take_info* theInfo = (Take_info*)info;
+ int __RET__ = theInfo->__RET__;
+ Deque * q = theInfo->q;
+
+ int elem = 0 ;
+ if ( succ ( __RET__ ) ) {
+ elem = back ( __deque ) ;
+ pop_back ( __deque ) ;
+ }
+ check_passed = succ ( __RET__ ) ? __RET__ == elem : true;
+ if (!check_passed)
+ return false;
+ return true;
+}
+/* End of check action function: Take */
+
+/* Definition of interface info struct: Push */
+typedef struct Push_info {
+Deque * q;
+int x;
+} Push_info;
+/* End of info struct definition: Push */
+
+/* ID function of interface: Push */
+inline static call_id_t Push_id(void *info, thread_id_t __TID__) {
+ Push_info* theInfo = (Push_info*)info;
+ Deque * q = theInfo->q;
+ int x = theInfo->x;
+
+ call_id_t __ID__ = x;
+ return __ID__;
+}
+/* End of ID function: Push */
+
+/* Check action function of interface: Push */
+inline static bool Push_check_action(void *info, call_id_t __ID__, thread_id_t __TID__) {
+ bool check_passed;
+ Push_info* theInfo = (Push_info*)info;
+ Deque * q = theInfo->q;
+ int x = theInfo->x;
+
+ push_back ( __deque , x ) ;
+ return true;
+}
+/* End of check action function: Push */
+
+#define INTERFACE_SIZE 3
+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) {
+ Push_info *_info1 = (Push_info*) info1;
+ Steal_info *_info2 = (Steal_info*) info2;
+ return true;
+}
+inline static bool CommutativityCondition1(void *info1, void *info2) {
+ Take_info *_info1 = (Take_info*) info1;
+ Steal_info *_info2 = (Steal_info*) info2;
+ return true;
+}
+
+/* Initialization of sequential varialbes */
+static void __SPEC_INIT__() {
+ __deque = createIntegerList ( ) ;
+}
+
+/* Cleanup routine of sequential variables */
+static bool __SPEC_CLEANUP__() {
+ if ( __deque ) destroyIntegerList ( __deque ) ;
+ return true ;
+}
+
+/* Define function for sequential code initialization */
+inline static void __sequential_init() {
+ /* Init func_ptr_table */
+ func_ptr_table = (void**) malloc(sizeof(void*) * 3 * 2);
+ func_ptr_table[2 * 2] = (void*) &Steal_id;
+ func_ptr_table[2 * 2 + 1] = (void*) &Steal_check_action;
+ func_ptr_table[2 * 0] = (void*) &Take_id;
+ func_ptr_table[2 * 0 + 1] = (void*) &Take_check_action;
+ func_ptr_table[2 * 1] = (void*) &Push_id;
+ func_ptr_table[2 * 1 + 1] = (void*) &Push_check_action;
+ /* Push(true) -> Steal(true) */
+ struct hb_rule *hbConditionInit0 = (struct hb_rule*) malloc(sizeof(struct hb_rule));
+ hbConditionInit0->interface_num_before = 1; // Push
+ hbConditionInit0->hb_condition_num_before = 0; //
+ hbConditionInit0->interface_num_after = 2; // Steal
+ hbConditionInit0->hb_condition_num_after = 0; //
+ /* Init hb_rule_table */
+ hb_rule_table = (hb_rule**) malloc(sizeof(hb_rule*) * 1);
+ #define HB_RULE_TABLE_SIZE 1
+ hb_rule_table[0] = hbConditionInit0;
+ /* Init commutativity_rule_table */
+ commutativity_rule_table = (commutativity_rule**) malloc(sizeof(commutativity_rule*) * 2);
+ commutativity_rule* rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 1;
+ rule->interface_num_after = 2;
+ rule->rule = "true";
+ rule->condition = CommutativityCondition0;
+ commutativity_rule_table[0] = rule;
+ rule = (commutativity_rule*) malloc (sizeof(commutativity_rule));
+ rule->interface_num_before = 0;
+ rule->interface_num_after = 2;
+ rule->rule = "true";
+ rule->condition = CommutativityCondition1;
+ commutativity_rule_table[1] = 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 = 2;
+ 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 */
+
+
+
+Deque * create();
+void resize(Deque *q);
+
+int __wrapper__take(Deque * q);
+
+int __wrapper__take(Deque * q) ;
+
+void __wrapper__push(Deque * q, int x);
+
+void __wrapper__push(Deque * q, int x) ;
+
+int __wrapper__steal(Deque * q);
+
+int __wrapper__steal(Deque * q) ;
+
+#endif
+
projects / cdsspec-compiler.git / blobdiff