notes/register-example/cdsspec-generated.h

   1 #include <cdsannotate.h>
   2 #include <modeltypes.h>
   3 #include <atomic>
   4 #include <threads.h>
   5 #include <stdatomic.h>
   6
   7 #include "mymemory.h"
   8 #include "specannotation.h"
   9 #include "cdsspec.h"
  10 #include "methodcall.h"
  11
  12 using namespace std;
  13
  14 typedef struct StateStruct {
  15         int val;
  16
  17         SNAPSHOTALLOC
  18 } StateStruct;
  19
  20 typedef struct LOAD {
  21         int RET;
  22         atomic_int *loc;
  23 } LOAD;
  24
  25 typedef struct STORE {
  26         atomic_int *loc;
  27         int val;
  28 } STORE;
  29
  30 inline void _initial(Method m) {
  31         StateStruct *state = new StateStruct;
  32         state->val = 0;
  33         m->state = state;
  34 }
  35
  36 inline void _copyState(Method dest, Method src) {
  37         StateStruct *stateSrc = (StateStruct*) src;
  38         StateStruct *stateDest = (StateStruct*) dest;
  39         stateDest->val = stateSrc->val;
  40 }
  41
  42 inline bool _checkCommutativity1(Method m1, Method m2) {
  43         if (m1->interfaceName == "LOAD" && m2->interfaceName == "LOAD") {
  44                 if (true)
  45                         return true;
  46                 else
  47                         return false;
  48         }
  49         return false;
  50 }
  51
  52 inline bool _checkCommutativity2(Method m1, Method m2) {
  53         if (m1->interfaceName == "STORE" && m2->interfaceName == "LOAD") {
  54                 if (true)
  55                         return true;
  56                 else
  57                         return false;
  58         }
  59         return false;
  60 }
  61
  62 inline bool _checkCommutativity3(Method m1, Method m2) {
  63         if (m1->interfaceName == "STORE" && m2->interfaceName == "STORE") {
  64                 if (true)
  65                         return true;
  66                 else
  67                         return false;
  68         }
  69         return false;
  70 }
  71
  72 inline void _LOAD_Transition(Method _M, Method _exec) {
  73         return;
  74 }
  75
  76 inline bool _LOAD_PreCondition(Method _M) {
  77         int RET = ((LOAD*) _M->value)->RET;
  78         atomic_int *loc = ((LOAD*) _M->value)->loc;
  79         return HasItem(PREV, Guard(STATE(val) == RET && loc));
  80 }
  81
  82 inline void _LOAD_SideEffect(Method _M) {
  83         int RET = ((LOAD*) _M->value)->RET;
  84         atomic_int *loc = ((LOAD*) _M->value)->loc;
  85         STATE(val) = RET;
  86 }
  87
  88 inline void _STORE_Transition(Method _M, Method _exec) {
  89         return;
  90 }
  91
  92 inline void _STORE_SideEffect(Method _M) {
  93         atomic_int *loc = ((STORE*) _M->value)->loc;
  94         int val = ((STORE*) _M->value)->val;
  95         STATE(val) = val;
  96 }
  97
  98 inline void _createInitAnnotation() {
  99         int CommuteRuleSize = 3;
 100         void *raw = CommutativityRule::operator new[](sizeof(CommutativityRule) * CommuteRuleSize);
 101         CommutativityRule *commuteRules = static_cast<CommutativityRule*>(raw);
 102
 103         // Initialize commutativity rule 1
 104         new( &commuteRules[0] )CommutativityRule("LOAD", "LOAD", "LOAD <-> LOAD (true)", _checkCommutativity1);
 105         // Initialize commutativity rule 2
 106         new( &commuteRules[1] )CommutativityRule("Store", "LOAD", "STORE <-> LOAD (true)", _checkCommutativity2);
 107         // Initialize commutativity rule 3
 108         new( &commuteRules[2] )CommutativityRule("STORE", "STORE", "STORE <-> STORE (true)", _checkCommutativity3);
 109
 110         // Initialize AnnoInit
 111         AnnoInit *anno = new AnnoInit(_initial, _copyState, commuteRules, CommuteRuleSize);
 112
 113         // Initialize StateFunctions map
 114         StateFunctions *stateFuncs;
 115
 116         // StateFunction for LOAD
 117         stateFuncs = new StateFunctions("LOAD", _LOAD_Transition, NULL, _LOAD_PreCondition, _LOAD_SideEffect, NULL);
 118         anno->addInterfaceFunctions("LOAD", stateFuncs);
 119         // StateFunction for STORE
 120         stateFuncs = new StateFunctions("STORE", _STORE_Transition, NULL, NULL, _STORE_SideEffect, NULL);
 121         anno->addInterfaceFunctions("STORE", stateFuncs);
 122
 123         // Create and instrument with the INIT annotation
 124         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, anno));
 125 }
 126
 127 inline Method _createInterfaceBeginAnnotation(string name) {
 128         Method cur = new MethodCall(name);
 129         // Create and instrument with the INTERFACE_BEGIN annotation
 130         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INTERFACE_BEGIN, cur));
 131         return cur;
 132 }
 133
 134 inline void _createOPDefineAnnotation() {
 135         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_DEFINE, NULL));
 136 }
 137
 138 inline void _createPotentialOPAnnotation(string label) {
 139         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(POTENTIAL_OP, new AnnoPotentialOP(label)));
 140 }
 141
 142 inline void _createOPCheckAnnotation(string label) {
 143         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CHECK, new AnnoOPCheck(label)));
 144 }
 145
 146 inline void _createOPClearAnnotation() {
 147         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR, NULL));
 148 }
 149
 150 inline void _createOPClearDefineAnnotation() {
 151         cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR_DEFINE, NULL));
 152 }