3 #include "traceanalysis.h"
4 #include "scanalysis.h"
6 #include "memoryorder.h"
11 #include "inference.h"
12 #include "inferlist.h"
16 #include "cyclegraph.h"
22 using std::memory_order;
25 #define DEFAULT_REPETITIVE_READ_BOUND 20
31 #define FENCE_PRINT model_print
33 #define ACT_PRINT(x) (x)->print()
35 #define CV_PRINT(x) (x)->print()
37 #define WILDCARD_ACT_PRINT(x)\
38 FENCE_PRINT("Wildcard: %d\n", get_wildcard_id_zero((x)->get_original_mo()));\
49 #define WILDCARD_ACT_PRINT(x)
53 /* Forward declaration */
61 extern SCFence *scfence;
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
69 typedef SnapList<path_t *> sync_paths_t;
70 typedef sync_paths_t paths_t;
72 typedef struct scfence_priv {
74 inferenceSet = new InferenceSet();
75 curInference = new Inference();
77 inferImplicitMO = false;
79 implicitMOReadBound = DEFAULT_REPETITIVE_READ_BOUND;
81 gettimeofday(&lastRecordedTime, NULL);
84 /** The set of the InferenceNode we maintain for exploring */
85 InferenceSet *inferenceSet;
87 /** The current inference */
88 Inference *curInference;
90 /** The file which provides a list of candidate wilcard inferences */
93 /** Whether we consider the repetitive read to infer mo (_m) */
96 /** The bound above which we think that write should be the last write (_b) */
97 int implicitMOReadBound;
99 /** Whether we have restarted the model checker */
102 /** The amount of time (in second) set to force the analysis to backtrack */
105 /** The time we recorded last time */
106 struct timeval lastRecordedTime;
111 typedef enum fix_type {
119 class SCFence : public TraceAnalysis {
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();
129 virtual void inspectModelAction(ModelAction *ac);
130 virtual void actionAtInstallation();
131 virtual void actionAtModelCheckingFinish();
136 /** The SC list generator */
139 struct sc_statistics *stats;
143 /** Should we weaken the inferences later */
146 /** Modification order graph */
147 const CycleGraph *mo_graph;
149 /** A duplica of the thread lists */
150 SnapVector<action_list_t> *dup_threadlists;
151 ModelExecution *execution;
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;
157 /** The non-snapshotting private compound data structure that has the
158 * necessary stuff for the scfence analysis */
159 static scfence_priv *priv;
161 /** For the SC analysis */
164 /** Get the custom input number for implicit bound */
165 int getImplicitMOBound(char *opt);
167 /** Get the input file for initial parameter assignments */
168 char* getInputFileName(char *opt);
170 /** The function to parse the SCFence plugin options */
171 bool parseOption(char *opt);
173 /** Helper function for option parsing */
174 char* parseOptionHelper(char *opt, int *optIdx);
176 /** Initialize the search with a file with a list of potential candidates */
177 void initializeByFile();
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();
183 /** Functions that work for infering the parameters by impsing
185 paths_t *get_rf_sb_paths(const ModelAction *act1, const ModelAction *act2);
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);
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();
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;
201 /** The two important routine when we find or cannot find a fix for the
202 * current inference */
203 void routineAfterAddFixes();
205 bool routineBacktrack(bool feasible);
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);
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);
213 /** Check if there exists data races, if so, overwrite act1 & act2 to be the
215 bool checkDataRace(action_list_t *list, ModelAction **act1,
218 /** Check if there exists data races, if so, generate the fixes */
219 bool addFixesDataRace(action_list_t *list);
221 /** The previous action in sb */
222 ModelAction* sbPrevAction(ModelAction *act);
223 /** The next action in sb */
224 ModelAction* sbNextAction(ModelAction *act);
226 /** When getting a non-SC execution, find potential fixes and add it to the
228 bool addFixesNonSC(action_list_t *list);
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);
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
237 bool addFixesImplicitMO(action_list_t *list);
239 /** General fixes wrapper */
240 bool addFixes(action_list_t *list, fix_type_t type);
242 /** Check whether a chosen reads-from path is a release sequence */
243 bool isReleaseSequence(path_t *path);
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);
251 bool imposeSync(InferenceList* inferList, path_t *path, const
252 ModelAction *begin, const ModelAction *end);
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);
260 /** Impose SC to the existing list of inferences (inferList) by action1 &
262 bool imposeSC(action_list_t * actions, InferenceList *inferList, const ModelAction *act1,
263 const ModelAction *act2);
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);
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();
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
282 bool addInference(Inference *infer) {
283 return getSet()->addInference(infer);
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
290 bool addCandidates(InferenceList *candidates) {
291 return getSet()->addCandidates(getCurInference(), candidates);
294 void addCurInference() {
295 getSet()->addCurInference(getCurInference());
298 /** Print the result of inferences */
299 void printResults() {
300 getSet()->printResults();
303 /** Print the candidates of inferences */
304 void printCandidates() {
305 getSet()->printCandidates();
308 /** The number of nodes in the set (including those parent nodes (set as
311 return getSet()->getCandidatesSize();
314 /** Set the restart flag of the model checker in order to restart the
315 * checking process */
316 void restartModelChecker();
318 /** Set the exit flag of the model checker in order to exit the whole
320 void exitModelChecker();
322 bool modelCheckerAtExitState();
324 const char* net_mo_str(memory_order order);
326 InferenceSet* getSet() {
327 return priv->inferenceSet;
330 void setHasFixes(bool val) {
331 getCurInference()->setHasFixes(val);
335 return getCurInference()->getHasFixes();
339 return getCurInference()->getBuggy();
342 void setBuggy(bool val) {
343 getCurInference()->setBuggy(val);
346 Inference* getCurInference() {
347 return priv->curInference;
350 void setCurInference(Inference* infer) {
351 priv->curInference = infer;
354 char* getCandidateFile() {
355 return priv->candidateFile;
358 void setCandidateFile(char* file) {
359 priv->candidateFile = file;
362 bool getInferImplicitMO() {
363 return priv->inferImplicitMO;
366 void setInferImplicitMO(bool val) {
367 priv->inferImplicitMO = val;
370 int getImplicitMOReadBound() {
371 return priv->implicitMOReadBound;
374 void setImplicitMOReadBound(int bound) {
375 priv->implicitMOReadBound = bound;
378 int getHasRestarted() {
379 return priv->hasRestarted;
382 void setHasRestarted(int val) {
383 priv->hasRestarted = val;
386 void setTimeout(int timeout) {
387 priv->timeout = timeout;
391 return priv->timeout;
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);
402 // Update the lastRecordedTime
403 priv->lastRecordedTime = now;
404 if (elapsedTime / 1000000.0 > priv->timeout)
410 /********************** SCFence-related stuff (end) **********************/