Add SCFence analysis

[model-checker.git] / scfence / patch.h

diff --git a/scfence/patch.h b/scfence/patch.h
new file mode 100644 (file)
index 0000000..d25bed1
--- /dev/null
+++ b/scfence/patch.h
@@ -0,0 +1,59 @@
+#ifndef _PATCH_H
+#define _PATCH_H
+
+#include "fence_common.h"
+#include "inference.h"
+
+class PatchUnit;
+class Patch;
+
+class PatchUnit {
+       private:
+       const ModelAction *act;
+       memory_order mo;
+
+       public:
+       PatchUnit(const ModelAction *act, memory_order mo) {
+               this->act= act;
+               this->mo = mo;
+       }
+
+       const ModelAction* getAct() {
+               return act;
+       }
+
+       memory_order getMO() {
+               return mo;
+       }
+
+       SNAPSHOTALLOC
+};
+
+class Patch {
+       private:
+       SnapVector<PatchUnit*> *units;
+
+       public:
+       Patch(const ModelAction *act, memory_order mo);
+
+       Patch(const ModelAction *act1, memory_order mo1, const ModelAction *act2,
+               memory_order mo2);
+
+       Patch();
+
+       bool canStrengthen(Inference *curInfer);
+
+       bool isApplicable();
+
+       void addPatchUnit(const ModelAction *act, memory_order mo);
+
+       int getSize();
+
+       PatchUnit* get(int i);
+
+       void print();
+
+       SNAPSHOTALLOC
+};
+
+#endif