scfence/scfence.h

   1 #ifndef _SCFENCE_H
   2 #define _SCFENCE_H
   3 #include "traceanalysis.h"
   4 #include "scanalysis.h"
   5 #include "hashtable.h"
   6 #include "memoryorder.h"
   7 #include "action.h"
   8
   9 #include "wildcard.h"
  10 #include "patch.h"
  11 #include "inference.h"
  12 #include "inferlist.h"
  13 #include "inferset.h"
  14
  15 #include "model.h"
  16 #include "cyclegraph.h"
  17 #include "scgen.h"
  18
  19 #include <sys/time.h>
  20
  21 #ifdef __cplusplus
  22 using std::memory_order;
  23 #endif
  24
  25 #define DEFAULT_REPETITIVE_READ_BOUND 20
  26
  27 #define FENCE_OUTPUT
  28
  29 #ifdef FENCE_OUTPUT
  30
  31 #define FENCE_PRINT model_print
  32
  33 #define ACT_PRINT(x) (x)->print()
  34
  35 #define CV_PRINT(x) (x)->print()
  36
  37 #define WILDCARD_ACT_PRINT(x)\
  38         FENCE_PRINT("Wildcard: %d\n", get_wildcard_id_zero((x)->get_original_mo()));\
  39         ACT_PRINT(x);
  40
  41 #else
  42
  43 #define FENCE_PRINT
  44
  45 #define ACT_PRINT(x)
  46
  47 #define CV_PRINT(x)
  48
  49 #define WILDCARD_ACT_PRINT(x)
  50
  51 #endif
  52
  53 /* Forward declaration */
  54 class SCFence;
  55 class Inference;
  56 class InferenceList;
  57 class PatchUnit;
  58 class Patch;
  59 class SCGenerator;
  60
  61 extern SCFence *scfence;
  62
  63 typedef action_list_t path_t;
  64 /** A list of load operations can represent the union of reads-from &
  65  * sequence-before edges; And we have a list of lists of load operations to
  66  * represent all the possible rfUsb paths between two nodes, defined as
  67  * syns_paths_t here
  68  */
  69 typedef SnapList<path_t *> sync_paths_t;
  70 typedef sync_paths_t paths_t;
  71
  72 typedef struct scfence_priv {
  73         scfence_priv() {
  74                 inferenceSet = new InferenceSet();
  75                 curInference = new Inference();
  76                 candidateFile = NULL;
  77                 inferImplicitMO = false;
  78                 hasRestarted = false;
  79                 implicitMOReadBound = DEFAULT_REPETITIVE_READ_BOUND;
  80                 timeout = 0;
  81                 gettimeofday(&lastRecordedTime, NULL);
  82         }
  83
  84         /** The set of the InferenceNode we maintain for exploring */
  85         InferenceSet *inferenceSet;
  86
  87         /** The current inference */
  88         Inference *curInference;
  89
  90         /** The file which provides a list of candidate wilcard inferences */
  91         char *candidateFile;
  92
  93         /** Whether we consider the repetitive read to infer mo (_m) */
  94         bool inferImplicitMO;
  95
  96         /** The bound above which we think that write should be the last write (_b) */
  97         int implicitMOReadBound;
  98
  99         /** Whether we have restarted the model checker */
 100         bool hasRestarted;
 101
 102         /** The amount of time (in second) set to force the analysis to backtrack */
 103         int timeout;
 104
 105         /** The time we recorded last time */
 106         struct timeval lastRecordedTime;
 107
 108         MEMALLOC
 109 } scfence_priv;
 110
 111 typedef enum fix_type {
 112         BUGGY_EXECUTION,
 113         IMPLICIT_MO,
 114         NON_SC,
 115         DATA_RACE
 116 } fix_type_t;
 117
 118
 119 class SCFence : public TraceAnalysis {
 120  public:
 121         SCFence();
 122         ~SCFence();
 123         virtual void setExecution(ModelExecution * execution);
 124         virtual void analyze(action_list_t *);
 125         virtual const char * name();
 126         virtual bool option(char *);
 127         virtual void finish();
 128
 129         virtual void inspectModelAction(ModelAction *ac);
 130         virtual void actionAtInstallation();
 131         virtual void actionAtModelCheckingFinish();
 132
 133         SNAPSHOTALLOC
 134
 135  private:
 136         /** The SC list generator */
 137         SCGenerator *scgen;
 138
 139         struct sc_statistics *stats;
 140
 141         bool time;
 142
 143         /** Should we weaken the inferences later */
 144         bool weaken;
 145
 146         /** Modification order graph */
 147         const CycleGraph *mo_graph;
 148
 149         /** A duplica of the thread lists */
 150         SnapVector<action_list_t> *dup_threadlists;
 151         ModelExecution *execution;
 152
 153         /** A set of actions that should be ignored in the partially SC analysis */
 154         HashTable<const ModelAction*, const ModelAction*, uintptr_t, 4> ignoredActions;
 155         int ignoredActionSize;
 156
 157         /** The non-snapshotting private compound data structure that has the
 158          * necessary stuff for the scfence analysis */
 159         static scfence_priv *priv;
 160
 161         /** For the SC analysis */
 162         void update_stats();
 163
 164         /** Get the custom input number for implicit bound */
 165         int getImplicitMOBound(char *opt);
 166
 167         /** Get the input file for initial parameter assignments */
 168         char* getInputFileName(char *opt);
 169
 170         /** The function to parse the SCFence plugin options */
 171         bool parseOption(char *opt);
 172
 173         /** Helper function for option parsing */
 174         char* parseOptionHelper(char *opt, int *optIdx);
 175
 176         /** Initialize the search with a file with a list of potential candidates */
 177         void initializeByFile();
 178
 179         /** A pass through the original actions to extract the ignored actions
 180          * (partially SC); it must be called after the threadlist has been built */
 181         void extractIgnoredActions();
 182
 183         /** Functions that work for infering the parameters by impsing
 184          * synchronization */
 185         paths_t *get_rf_sb_paths(const ModelAction *act1, const ModelAction *act2);
 186
 187         /** Printing function for those paths imposed by happens-before; only for
 188          * the purpose of debugging */
 189         void print_rf_sb_paths(paths_t *paths, const ModelAction *start, const ModelAction *end);
 190
 191         /** Whether there's an edge between from and to actions */
 192         bool isSCEdge(const ModelAction *from, const ModelAction *to) {
 193                 return from->is_seqcst() && to->is_seqcst();
 194         }
 195
 196         bool isConflicting(const ModelAction *act1, const ModelAction *act2) {
 197                 return act1->get_location() == act2->get_location() ? (act1->is_write()
 198                         || act2->is_write()) : false;
 199         }
 200
 201         /** The two important routine when we find or cannot find a fix for the
 202          * current inference */
 203         void routineAfterAddFixes();
 204
 205         bool routineBacktrack(bool feasible);
 206
 207         /** A subroutine to find candidates for pattern (a) */
 208         InferenceList* getFixesFromPatternA(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter);
 209
 210         /** A subroutine to find candidates for pattern (b) */
 211         InferenceList* getFixesFromPatternB(action_list_t *list, action_list_t::iterator readIter, action_list_t::iterator writeIter);
 212
 213         /** Check if there exists data races, if so, overwrite act1 & act2 to be the
 214          *  two */
 215         bool checkDataRace(action_list_t *list, ModelAction **act1,
 216                 ModelAction **act2);
 217
 218         /** Check if there exists data races, if so, generate the fixes */
 219         bool addFixesDataRace(action_list_t *list);
 220
 221         /** The previous action in sb */
 222         ModelAction* sbPrevAction(ModelAction *act);
 223         /** The next action in sb */
 224         ModelAction* sbNextAction(ModelAction *act);
 225
 226         /** When getting a non-SC execution, find potential fixes and add it to the
 227          *  set */
 228         bool addFixesNonSC(action_list_t *list);
 229
 230         /** When getting a buggy execution (we only target the uninitialized loads
 231          * here), find potential fixes and add it to the set */
 232         bool addFixesBuggyExecution(action_list_t *list);
 233
 234         /** When getting an SC and bug-free execution, we check whether we should
 235          * fix the implicit mo problems. If so, find potential fixes and add it to
 236          * the set */
 237         bool addFixesImplicitMO(action_list_t *list);
 238
 239         /** General fixes wrapper */
 240         bool addFixes(action_list_t *list, fix_type_t type);
 241
 242         /** Check whether a chosen reads-from path is a release sequence */
 243         bool isReleaseSequence(path_t *path);
 244
 245         /** Impose synchronization to the existing list of inferences (inferList)
 246          *  according to path, begin is the beginning operation, and end is the
 247          *  ending operation. */
 248         bool imposeSync(InferenceList* inferList, paths_t *paths, const
 249                 ModelAction *begin, const ModelAction *end);
 250
 251         bool imposeSync(InferenceList* inferList, path_t *path, const
 252                 ModelAction *begin, const ModelAction *end);
 253
 254         /** For a specific pair of write and read actions, figure out the possible
 255          *  acq/rel fences that can impose hb plus the read & write sync pair */
 256         SnapVector<Patch*>* getAcqRel(const ModelAction *read,
 257                 const ModelAction *readBound, const ModelAction *write,
 258                 const ModelAction *writeBound);
 259
 260         /** Impose SC to the existing list of inferences (inferList) by action1 &
 261          *  action2. */
 262         bool imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1,
 263                 const ModelAction *act2);
 264
 265         /** When we finish model checking or cannot further strenghen with the
 266          * current inference, we commit the current inference (the node at the back
 267          * of the set) to be explored, pop it out of the set; if it is feasible,
 268          * we put it in the result list */
 269         void commitInference(Inference *infer, bool feasible) {
 270                 getSet()->commitInference(infer, feasible);
 271         }
 272
 273         /** Get the next available unexplored node; @Return NULL
 274          * if we don't have next, meaning that we are done with exploring */
 275         Inference* getNextInference() {
 276                 return getSet()->getNextInference();
 277         }
 278
 279         /** Add one possible node that represents a fix for the current inference;
 280          * @Return true if the node to add has not been explored yet
 281          */
 282         bool addInference(Inference *infer) {
 283                 return getSet()->addInference(infer);
 284         }
 285
 286         /** Add the list of fixes to the inference set. We will have to pass in the
 287          *  current inference.;
 288          * @Return true if the node to add has not been explored yet
 289          */
 290         bool addCandidates(InferenceList *candidates) {
 291                 return getSet()->addCandidates(getCurInference(), candidates);
 292         }
 293
 294         void addCurInference() {
 295                 getSet()->addCurInference(getCurInference());
 296         }
 297
 298         /** Print the result of inferences  */
 299         void printResults() {
 300                 getSet()->printResults();
 301         }
 302
 303         /** Print the candidates of inferences  */
 304         void printCandidates() {
 305                 getSet()->printCandidates();
 306         }
 307
 308         /** The number of nodes in the set (including those parent nodes (set as
 309          * explored) */
 310          int setSize() {
 311                 return getSet()->getCandidatesSize();
 312          }
 313
 314         /** Set the restart flag of the model checker in order to restart the
 315          * checking process */
 316         void restartModelChecker();
 317
 318         /** Set the exit flag of the model checker in order to exit the whole
 319          * process */
 320         void exitModelChecker();
 321
 322         bool modelCheckerAtExitState();
 323
 324         const char* net_mo_str(memory_order order);
 325
 326         InferenceSet* getSet() {
 327                 return priv->inferenceSet;
 328         }
 329
 330         void setHasFixes(bool val) {
 331                 getCurInference()->setHasFixes(val);
 332         }
 333
 334         bool hasFixes() {
 335                 return getCurInference()->getHasFixes();
 336         }
 337
 338         bool isBuggy() {
 339                 return getCurInference()->getBuggy();
 340         }
 341
 342         void setBuggy(bool val) {
 343                 getCurInference()->setBuggy(val);
 344         }
 345
 346         Inference* getCurInference() {
 347                 return priv->curInference;
 348         }
 349
 350         void setCurInference(Inference* infer) {
 351                 priv->curInference = infer;
 352         }
 353
 354         char* getCandidateFile() {
 355                 return priv->candidateFile;
 356         }
 357
 358         void setCandidateFile(char* file) {
 359                 priv->candidateFile = file;
 360         }
 361
 362         bool getInferImplicitMO() {
 363                 return priv->inferImplicitMO;
 364         }
 365
 366         void setInferImplicitMO(bool val) {
 367                 priv->inferImplicitMO = val;
 368         }
 369
 370         int getImplicitMOReadBound() {
 371                 return priv->implicitMOReadBound;
 372         }
 373
 374         void setImplicitMOReadBound(int bound) {
 375                 priv->implicitMOReadBound = bound;
 376         }
 377
 378         int getHasRestarted() {
 379                 return priv->hasRestarted;
 380         }
 381
 382         void setHasRestarted(int val) {
 383                 priv->hasRestarted = val;
 384         }
 385
 386         void setTimeout(int timeout) {
 387                 priv->timeout = timeout;
 388         }
 389
 390         int getTimeout() {
 391                 return priv->timeout;
 392         }
 393
 394         bool isTimeout() {
 395                 struct timeval now;
 396                 gettimeofday(&now, NULL);
 397                 // Check if it should be timeout
 398                 struct timeval *lastRecordedTime = &priv->lastRecordedTime;
 399                 unsigned long long elapsedTime = (now.tv_sec*1000000 + now.tv_usec) -
 400                         (lastRecordedTime->tv_sec*1000000 + lastRecordedTime->tv_usec);
 401
 402                 // Update the lastRecordedTime
 403                 priv->lastRecordedTime = now;
 404                 if (elapsedTime / 1000000.0 > priv->timeout)
 405                         return true;
 406                 else
 407                         return false;
 408         }
 409
 410         /********************** SCFence-related stuff (end) **********************/
 411 };
 412 #endif