X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scfence%2Fpatch.h;fp=scfence%2Fpatch.h;h=d25bed19dc5b550b1359faaa73a1e2664f053f2b;hp=0000000000000000000000000000000000000000;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=7c510878f9679da10de79c289df402356b092396

diff --git a/scfence/patch.h b/scfence/patch.h
new file mode 100644
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