1 #include <cdsannotate.h>
2 #include <modeltypes.h>
8 #include "specannotation.h"
10 #include "methodcall.h"
14 typedef struct StateStruct {
25 typedef struct STORE {
30 inline void _initial(Method m) {
31 StateStruct *state = new StateStruct;
36 inline void _copyState(Method dest, Method src) {
37 StateStruct *stateSrc = (StateStruct*) src;
38 StateStruct *stateDest = (StateStruct*) dest;
39 stateDest->val = stateSrc->val;
42 inline bool _checkCommutativity1(Method m1, Method m2) {
43 if (m1->interfaceName == "LOAD" && m2->interfaceName == "LOAD") {
52 inline bool _checkCommutativity2(Method m1, Method m2) {
53 if (m1->interfaceName == "STORE" && m2->interfaceName == "LOAD") {
62 inline bool _checkCommutativity3(Method m1, Method m2) {
63 if (m1->interfaceName == "STORE" && m2->interfaceName == "STORE") {
72 inline void _LOAD_Transition(Method _M, Method _exec) {
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));
82 inline void _LOAD_SideEffect(Method _M) {
83 int RET = ((LOAD*) _M->value)->RET;
84 atomic_int *loc = ((LOAD*) _M->value)->loc;
88 inline void _STORE_Transition(Method _M, Method _exec) {
92 inline void _STORE_SideEffect(Method _M) {
93 atomic_int *loc = ((STORE*) _M->value)->loc;
94 int val = ((STORE*) _M->value)->val;
98 inline void _createInitAnnotation() {
99 int CommuteRuleSize = 3;
100 void *raw = CommutativityRule::operator new[](sizeof(CommutativityRule) * CommuteRuleSize);
101 CommutativityRule *commuteRules = static_cast<CommutativityRule*>(raw);
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);
110 // Initialize AnnoInit
111 AnnoInit *anno = new AnnoInit(_initial, _copyState, commuteRules, CommuteRuleSize);
113 // Initialize StateFunctions map
114 StateFunctions *stateFuncs;
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);
123 // Create and instrument with the INIT annotation
124 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(INIT, anno));
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));
134 inline void _createOPDefineAnnotation() {
135 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_DEFINE, NULL));
138 inline void _createPotentialOPAnnotation(string label) {
139 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(POTENTIAL_OP, new AnnoPotentialOP(label)));
142 inline void _createOPCheckAnnotation(string label) {
143 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CHECK, new AnnoOPCheck(label)));
146 inline void _createOPClearAnnotation() {
147 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR, NULL));
150 inline void _createOPClearDefineAnnotation() {
151 cdsannotate(SPEC_ANALYSIS, new SpecAnnotation(OP_CLEAR_DEFINE, NULL));