spec-analysis/executiongraph.h

   1 #ifndef _EXECUTIONGRAPH_H
   2 #define _EXECUTIONGRAPH_H
   3
   4 #include <stack>
   5
   6 #include "hashtable.h"
   7 #include "specannotation.h"
   8 #include "mymemory.h"
   9 #include "modeltypes.h"
  10 #include "action.h"
  11 #include "common.h"
  12 #include "execution.h"
  13
  14 #include "methodcall.h"
  15 #include "specannotation.h"
  16
  17
  18 const int SELF_CYCLE = 0xfffe;
  19
  20 /**
  21         Record the a potential commit point information, including the potential
  22         commit point label number and the corresponding operation
  23 */
  24 typedef struct PotentialOP {
  25         ModelAction *operation;
  26         CSTR label;
  27
  28         PotentialOP(ModelAction *op, CSTR name);
  29
  30         SNAPSHOTALLOC
  31 } PotentialOP;
  32
  33 class Graph;
  34
  35
  36 typedef SnapList<PotentialOP*> PotentialOPList;
  37
  38 /**
  39         This represents the execution graph at the method call level. Each node is a
  40         MethodCall type that has the runtime info (return value & arguments) and the
  41         state info the method call. The edges in this graph are the hb/SC edges
  42         dereived from the ordering points of the method call. Those edges
  43         information are stoed in the PREV and NEXT set of MethodCall struct.
  44 */
  45 class ExecutionGraph {
  46         public:
  47         ExecutionGraph(ModelExecution *e, bool allowCyclic);
  48
  49         /********** Public class interface for the core checking engine **********/
  50         /**
  51                 Build the graph for an execution. It should returns true when the graph
  52                 is correctly built
  53         */
  54         void buildGraph(action_list_t *actions);
  55
  56         /** Check whether this is a broken execution */
  57         bool isBroken();
  58
  59         /** Check whether this is an execution that has method calls without
  60          * ordering points */
  61         bool isNoOrderingPoint();
  62
  63         /**
  64                 Check whether this is a cyclic execution graph, meaning that the graph
  65                 has an cycle derived from the ordering points' hb/SC relation
  66         */
  67         bool hasCycle();
  68
  69         /** Reset the internal graph "broken" state to okay again */
  70         void resetBroken();
  71
  72         /** Check whether the execution is admmisible */
  73         bool checkAdmissibility();
  74
  75         /** Checking cyclic graph specification */
  76         bool checkCyclicGraphSpec(bool verbose);
  77
  78         /** Check whether a number of random history is correct */
  79         bool checkRandomHistories(int num = 1, bool stopOnFail = true, bool verbose = false);
  80
  81         /** Check whether all histories are correct */
  82         bool checkAllHistories(bool stopOnFailure = true, bool verbose = false);
  83
  84         /********** A few public printing functions for DEBUGGING **********/
  85
  86         /**
  87                 Print out the ordering points and dynamic calling info (return value &
  88                 arguments) of all the methods in the methodList
  89         */
  90         void printAllMethodInfo(bool verbose);
  91
  92         /** Print a random sorting */
  93         void printOneHistory(MethodList *list, CSTR header = "A random history");
  94
  95         /** Print all the possible sortings */
  96         void printAllHistories(MethodListVector *sortings);
  97
  98         /** Print out the graph for the purpose of debugging */
  99         void print(bool allEdges = false);
 100
 101         /**
 102                 Print out the graph in reverse order (with previous edges) for the
 103                 purpose of debugging
 104         */
 105         void PrintReverse(bool allEdges);
 106
 107         SNAPSHOTALLOC
 108
 109         private:
 110         /** The corresponding execution */
 111         ModelExecution *execution;
 112
 113         /** All the threads each in a separate list of actions */
 114         SnapVector<action_list_t*> *threadLists;
 115
 116         /** A plain list of all method calls (Method) in this execution */
 117         MethodList *methodList;
 118
 119         /**
 120                 A list that represents some random history. The reason we have this here
 121                 is that before checking anything, we have to check graph acyclicity, and
 122                 that requires us to check whether we can generate a topological sorting.
 123                 Therefore, when we check it, we store that random result here.
 124         */
 125         MethodList *randomHistory;
 126
 127         /** Whether this is a broken graph */
 128         bool broken;
 129
 130         /** Whether this graph has method calls that have no ordering points */
 131         bool noOrderingPoint;
 132
 133         /** Whether there is a cycle in the graph */
 134         bool cyclic;
 135
 136         /** Whether users expect us to check cyclic graph */
 137         bool allowCyclic;
 138
 139
 140         /** The state initialization function */
 141         NamedFunction *initial;
 142
 143         /** FIXME: The final check function; we might delete this */
 144         NamedFunction *final;
 145
 146         /** The state copy function */
 147         NamedFunction *copy;
 148
 149         /** The state clear function */
 150         NamedFunction *clear;
 151
 152         /** The state print-out function */
 153         NamedFunction *printState;
 154
 155         /** The map from interface label name to the set of spec functions */
 156         StateFuncMap *funcMap;
 157
 158         /** The commutativity rule array and its size */
 159         CommutativityRule *commuteRules;
 160         int commuteRuleNum;
 161
 162         /********** Internal member functions **********/
 163
 164         /**
 165                 Simply build a vector of lists of thread actions. Such info will be very
 166                 useful for later constructing the execution graph
 167         */
 168         void buildThreadLists(action_list_t *actions);
 169
 170         /** Build the nodes from a thread list */
 171         void buildNodesFromThread(action_list_t *actions);
 172
 173         /** Build the nodes from all the thread lists */
 174         void buildNodesFromThreads();
 175
 176
 177         /**
 178                 Find the previous non-annotation model action (ordering point from the
 179                 current iterator
 180         */
 181         ModelAction* findPrevAction(action_list_t *actions, action_list_t::iterator
 182                 iter);
 183
 184         /**
 185                 Extract a MethodCall node starting from the current iterator, and the
 186                 iter iterator will be advanced to the next INTERFACE_BEGIN annotation.
 187                 When called, the iter must point to an INTERFACE_BEGIN annotation
 188         */
 189         Method extractMethod(action_list_t *actions, action_list_t::iterator &iter);
 190
 191         /**
 192                 Process the initialization annotation block to initialize the
 193                 commutativity rule info and the checking function info
 194         */
 195         void processInitAnnotation(AnnoInit *annoInit);
 196
 197         /**
 198                 A utility function to extract the actual annotation
 199                 pointer and return the actual annotation if this is an annotation action;
 200                 otherwise return NULL.
 201         */
 202         SpecAnnotation* getAnnotation(ModelAction *act);
 203
 204         /**
 205                 After building up the graph (both the nodes and egdes are correctly
 206                 built), we also call this function to initialize the most recent
 207                 justified node of each method node.
 208
 209                 A justified method node of a method m is a method that is in the allPrev
 210                 set of m, and all other nodes in the allPrev set of m are either before
 211                 or after it. The most recent justified node is the most recent one in
 212                 the hb/SC order.
 213         */
 214         void initializeJustifiedNode();
 215
 216         /**
 217                 After extracting the MethodCall info for each method call, we use this
 218                 function to build the edges (a few different sets of edges that
 219                 represent the edge of the execution graph (PREV, NEXT & CONCURRENT...)
 220         */
 221         void buildEdges();
 222
 223         /**
 224                 This method call is used to check whether the edge sets of the nodes are
 225                 built correctly --- consistently. We should only use this routine after the
 226                 builiding of edges when debugging
 227         */
 228         void AssertEdges();
 229
 230         /**
 231                 The conflicting relation between two model actions by hb/SC. If act1 and
 232                 act2 commutes, it returns 0; Otherwise, if act1->act2, it returns 1; and
 233                 if act2->act1, it returns -1
 234         */
 235         int conflict(ModelAction *act1, ModelAction *act2);
 236
 237         /**
 238                 If there is no conflict between the ordering points of m1 and m2, then
 239                 it returns 0; Otherwise, if m1->m2, it returns 1; and if m2->m1, it
 240                 returns -1.  If some ordering points have inconsistent conflicting
 241                 relation, we print out an error message (Self-cycle) and set the broken
 242                 flag and return
 243         */
 244         int conflict(Method m1, Method m2);
 245
 246         /**
 247                 Check whether m1 is before m2 in hb/SC; Reachability <=> m1 -hb/SC-> m2.
 248                 We need to call this method when checking admissibility properties
 249         */
 250         bool isReachable(Method m1, Method m2);
 251
 252         /**
 253                 Find the list of nodes that do not have any incoming edges (root nodes).
 254                 Be careful that when generating histories, this function will also
 255                 consider whether a method node logicall exists.
 256         */
 257         MethodVector* getRootNodes();
 258
 259         /**
 260                 Find the list of nodes that do not have any outgoing edges (end nodes)
 261         */
 262         MethodVector* getEndNodes();
 263
 264         /**
 265                 A helper function for generating and check all sequential histories. Before calling this function, initialize an empty
 266                 MethodList , and pass it as curList. Also pass the size of the method
 267                 list as the numLiveNodes.
 268
 269                 If you only want to stop the checking process when finding one failed
 270                 history, pass true to stopOnFailure.
 271         */
 272         bool checkAllHistoriesHelper(MethodList *curList, int &numLiveNodes, int
 273         &historyNum, bool stopOnFailure, bool verbose);
 274
 275
 276         /** Check whether a specific history is correct */
 277         bool checkHistory(MethodList *history, int historyIndex, bool verbose = false);
 278
 279         /** Generate one random topological sorting */
 280         MethodList* generateOneRandomHistory();
 281
 282         /**
 283                 The helper function to generate one random topological sorting
 284         */
 285         void generateOneRandomHistoryHelper(MethodList
 286                 *curList, int &numLiveNodes);
 287
 288         /** Return the fake nodes -- START & END */
 289         Method getStartMethod();
 290         Method getFinishMethod();
 291
 292         /** Whether method call node m is a fake node */
 293         inline bool isFakeMethod(Method m) {
 294                 return isStartMethod(m) || isFinishMethod(m);
 295         }
 296
 297         /** Whether method call node m is a starting node */
 298         inline bool isStartMethod(Method m) {
 299                 return m->name == GRAPH_START;
 300         }
 301
 302         /** Whether method call node m is a finish node */
 303         inline bool isFinishMethod(Method m) {
 304                 return m->name == GRAPH_FINISH;
 305         }
 306
 307         /**
 308                 Print out the ordering points and dynamic calling info (return value &
 309                 arguments).
 310         */
 311         void printMethodInfo(Method m, bool verbose);
 312
 313         /** Clear the states of the method call */
 314         void clearStates();
 315
 316         /**
 317                 Check the state specifications (PreCondition & PostCondition & state
 318                 transition and evaluation) based on the graph (called after
 319                 admissibility check). The verbose option controls whether we print a
 320                 detailed list of checking functions that we have called
 321         */
 322         bool checkStateSpec(MethodList *history, bool verbose, int historyNum);
 323
 324         /**
 325                 Check the justifying subhistory with respect to history of m.
 326         */
 327         bool checkJustifyingSubhistory(MethodList *subhistory, Method cur,
 328                 bool verbose, int historyIndex);
 329
 330         /** Print a problematic thread list */
 331         void printActions(action_list_t *actions, const char *header = "The problematic thread list:");
 332
 333         /** Print one jusifying subhistory of method call cur */
 334         void printOneSubhistory(MethodList *history, Method cur,
 335                 CSTR header);
 336 };
 337
 338 #endif