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

diff --git a/scfence/inference.cc b/scfence/inference.cc
new file mode 100644
index 0000000..e2d2152
--- /dev/null
+++ b/scfence/inference.cc
@@ -0,0 +1,378 @@
+#include "fence_common.h"
+#include "wildcard.h"
+#include "patch.h"
+#include "inferlist.h"
+#include "inference.h"
+
+/** Forward declaration */
+class PatchUnit;
+class Patch;
+class Inference;
+class InferenceList;
+
+bool isTheInference(Inference *infer) {
+	for (int i = 0; i < infer->getSize(); i++) {
+		memory_order mo1 = (*infer)[i], mo2;
+		if (mo1 == WILDCARD_NONEXIST)
+			mo1 = relaxed;
+		switch (i) {
+			case 3:
+				mo2 = acquire;
+			break;
+			case 11:
+				mo2 = release;
+			break;
+			default:
+				mo2 = relaxed;
+			break;
+		}
+		if (mo1 != mo2)
+			return false;
+	}
+	return true;
+}
+
+const char* get_mo_str(memory_order order) {
+	switch (order) {
+		case std::memory_order_relaxed: return "relaxed";
+		case std::memory_order_acquire: return "acquire";
+		case std::memory_order_release: return "release";
+		case std::memory_order_acq_rel: return "acq_rel";
+		case std::memory_order_seq_cst: return "seq_cst";
+		default: 
+			//model_print("Weird memory order, a bug or something!\n");
+			//model_print("memory_order: %d\n", order);
+			return "unknown";
+	}
+}
+
+
+void Inference::resize(int newsize) {
+	ASSERT (newsize > size && newsize <= MAX_WILDCARD_NUM);
+	memory_order *newOrders = (memory_order *) model_malloc((newsize + 1) * sizeof(memory_order*));
+	int i;
+	for (i = 0; i <= size; i++)
+		newOrders[i] = orders[i];
+	for (; i <= newsize; i++)
+		newOrders[i] = WILDCARD_NONEXIST;
+	model_free(orders);
+	size = newsize;
+	orders = newOrders;
+}
+
+/** Return the state of how we update a specific mo; If we have to make an
+ * uncompatible inference or that inference cannot be imposed because it's
+ * not a wildcard, it returns -1; if it is a compatible memory order but the
+ * current memory order is no weaker than mo, it returns 0; otherwise, it
+ * does strengthen the order, and returns 1 */
+int Inference::strengthen(const ModelAction *act, memory_order mo) {
+	memory_order wildcard = act->get_original_mo();
+	int wildcardID = get_wildcard_id_zero(wildcard);
+	if (!is_wildcard(wildcard)) {
+		FENCE_PRINT("We cannot make this update to %s!\n", get_mo_str(mo));
+		ACT_PRINT(act);
+		return -1;
+	}
+	if (wildcardID > size)
+		resize(wildcardID);
+	ASSERT (is_normal_mo(mo));
+	//model_print("wildcardID -> order: %d -> %d\n", wildcardID, orders[wildcardID]);
+	ASSERT (is_normal_mo_infer(orders[wildcardID]));
+	switch (orders[wildcardID]) {
+		case memory_order_seq_cst:
+			return 0;
+		case memory_order_relaxed:
+			if (mo == memory_order_relaxed)
+				return 0;
+			orders[wildcardID] = mo;
+			break;
+		case memory_order_acquire:
+			if (mo == memory_order_acquire || mo == memory_order_relaxed)
+				return 0;
+			if (mo == memory_order_release)
+				orders[wildcardID] = memory_order_acq_rel;
+			else if (mo >= memory_order_acq_rel && mo <=
+				memory_order_seq_cst)
+				orders[wildcardID] = mo;
+			break;
+		case memory_order_release:
+			if (mo == memory_order_release || mo == memory_order_relaxed)
+				return 0;
+			if (mo == memory_order_acquire)
+				orders[wildcardID] = memory_order_acq_rel;
+			else if (mo >= memory_order_acq_rel)
+				orders[wildcardID] = mo;
+			break;
+		case memory_order_acq_rel:
+			if (mo == memory_order_seq_cst)
+				orders[wildcardID] = mo;
+			else
+				return 0;
+			break;
+		default:
+			orders[wildcardID] = mo;
+			break;
+	}
+	return 1;
+}
+
+Inference::Inference() {
+	orders = (memory_order *) model_malloc((4 + 1) * sizeof(memory_order*));
+	size = 4;
+	for (int i = 0; i <= size; i++)
+		orders[i] = WILDCARD_NONEXIST;
+	initialInfer = this;
+	buggy = false;
+	hasFixes = false;
+	leaf = false;
+	explored = false;
+	shouldFix = true;
+}
+
+Inference::Inference(Inference *infer) {
+	ASSERT (infer->size > 0 && infer->size <= MAX_WILDCARD_NUM);
+	orders = (memory_order *) model_malloc((infer->size + 1) * sizeof(memory_order*));
+	this->size = infer->size;
+	for (int i = 0; i <= size; i++)
+		orders[i] = infer->orders[i];
+
+	initialInfer = infer->initialInfer;
+	buggy = false;
+	hasFixes = false;
+	leaf = false;
+	explored = false;
+	shouldFix = true;
+}
+
+/** return value:
+  * 0 -> mo1 == mo2;
+  * 1 -> mo1 stronger than mo2;
+  * -1 -> mo1 weaker than mo2;
+  * 2 -> mo1 & mo2 are uncomparable.
+ */
+int Inference::compareMemoryOrder(memory_order mo1, memory_order mo2) {
+	if (mo1 == WILDCARD_NONEXIST)
+		mo1 = memory_order_relaxed;
+	if (mo2 == WILDCARD_NONEXIST)
+		mo2 = memory_order_relaxed;
+	if (mo1 == mo2)
+		return 0;
+	if (mo1 == memory_order_relaxed)
+		return -1;
+	if (mo1 == memory_order_acquire) {
+		if (mo2 == memory_order_relaxed)
+			return 1;
+		if (mo2 == memory_order_release)
+			return 2;
+		return -1;
+	}
+	if (mo1 == memory_order_release) {
+		if (mo2 == memory_order_relaxed)
+			return 1;
+		if (mo2 == memory_order_acquire)
+			return 2;
+		return -1;
+	}
+	if (mo1 == memory_order_acq_rel) {
+		if (mo2 == memory_order_seq_cst)
+			return -1;
+		else
+			return 1;
+	}
+	// mo1 now must be SC and mo2 can't be SC
+	return 1;
+}
+
+
+/** Try to calculate the set of inferences that are weaker than this, but
+ *  still stronger than infer */
+InferenceList* Inference::getWeakerInferences(Inference *infer) {
+	// An array of strengthened wildcards
+	SnapVector<int> *strengthened = new SnapVector<int>;
+	model_print("Strengthened wildcards\n");
+	for (int i = 1; i <= size; i++) {
+		memory_order mo1 = orders[i],
+			mo2 = (*infer)[i];
+		int compVal = compareMemoryOrder(mo1, mo2);
+		if (!(compVal == 0 || compVal == 1)) {
+			model_print("assert failure\n");
+			model_print("compVal=%d\n", compVal);
+			ASSERT (false);
+		}
+		if (compVal == 0) // Same
+			continue;
+		model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1),
+			get_mo_str(mo2));
+		strengthened->push_back(i);
+	}
+
+	// Got the strengthened wildcards, find out weaker inferences
+	// First get a volatile copy of this inference
+	Inference *tmpRes = new Inference(this);
+	InferenceList *res = new InferenceList;
+	if (strengthened->size() == 0)
+		return res;
+	getWeakerInferences(res, tmpRes, this, infer, strengthened, 0);
+	res->pop_front();
+	res->pop_back();
+	InferenceList::print(res, "Weakened");
+	return res;
+}
+
+
+// seq_cst -> acq_rel -> acquire -> release -> relaxed
+memory_order Inference::nextWeakOrder(memory_order mo1, memory_order mo2) {
+	memory_order res;
+	switch (mo1) {
+		case memory_order_seq_cst:
+			res = memory_order_acq_rel;
+			break;
+		case memory_order_acq_rel:
+			res = memory_order_acquire;
+			break;
+		case memory_order_acquire:
+			res = memory_order_relaxed;
+			break;
+		case memory_order_release:
+			res = memory_order_relaxed;
+			break;
+		case memory_order_relaxed:
+			res = memory_order_relaxed;
+			break;
+		default: 
+			res = memory_order_relaxed;
+			break;
+	}
+	int compVal = compareMemoryOrder(res, mo2);
+	if (compVal == 2 || compVal == -1) // Incomparable
+		res = mo2;
+	return res;
+}
+
+void Inference::getWeakerInferences(InferenceList* list, Inference *tmpRes,
+	Inference *infer1, Inference *infer2, SnapVector<int> *strengthened, unsigned idx) {
+	if (idx == strengthened->size()) { // Ready to produce one weakened result
+		Inference *res = new Inference(tmpRes);
+		//model_print("Weakened inference:\n");
+		//res->print();
+		res->setShouldFix(false);
+		list->push_back(res);
+		return;
+	}
+
+	int w = (*strengthened)[idx]; // The wildcard
+	memory_order mo1 = (*infer1)[w];
+	memory_order mo2 = (*infer2)[w];
+	if (mo2 == WILDCARD_NONEXIST)
+		mo2 = memory_order_relaxed;
+	memory_order weakenedMO = mo1;
+	do {
+		(*tmpRes)[w] = weakenedMO;
+		getWeakerInferences(list, tmpRes, infer1, infer2,
+			strengthened, idx + 1);
+		if (weakenedMO == memory_order_acq_rel) {
+			(*tmpRes)[w] = memory_order_release;
+			getWeakerInferences(list, tmpRes, infer1, infer2,
+				strengthened, idx + 1);
+		}
+		weakenedMO = nextWeakOrder(weakenedMO, mo2);
+		model_print("weakendedMO=%d\n", weakenedMO);
+		model_print("mo2=%d\n", mo2);
+	} while (weakenedMO != mo2);
+	(*tmpRes)[w] = weakenedMO;
+	getWeakerInferences(list, tmpRes, infer1, infer2,
+		strengthened, idx + 1);
+}
+
+memory_order& Inference::operator[](int idx) {
+	if (idx > 0 && idx <= size)
+		return orders[idx];
+	else {
+		resize(idx);
+		orders[idx] = WILDCARD_NONEXIST;
+		return orders[idx];
+	}
+}
+
+/** A simple overload, which allows caller to pass two boolean refrence, and
+ * we will set those two variables indicating whether we can update the
+ * order (copatible or not) and have updated the order */
+int Inference::strengthen(const ModelAction *act, memory_order mo, bool &canUpdate, bool &hasUpdated) {
+	int res = strengthen(act, mo);
+	if (res == -1)
+		canUpdate = false;
+	if (res == 1)
+		hasUpdated = true;
+
+	return res;
+}
+
+/** @Return:
+	1 -> 'this> infer';
+	-1 -> 'this < infer'
+	0 -> 'this == infer'
+	INFERENCE_INCOMPARABLE(x) -> true means incomparable
+ */
+int Inference::compareTo(const Inference *infer) const {
+	int result = size == infer->size ? 0 : (size > infer->size) ? 1 : -1;
+	int smallerSize = size > infer->size ? infer->size : size;
+	int subResult;
+
+	for (int i = 0; i <= smallerSize; i++) {
+		memory_order mo1 = orders[i],
+			mo2 = infer->orders[i];
+		if ((mo1 == memory_order_acquire && mo2 == memory_order_release) ||
+			(mo1 == memory_order_release && mo2 == memory_order_acquire)) {
+			// Incomparable
+			return -2;
+		} else {
+			if ((mo1 == WILDCARD_NONEXIST && mo2 != WILDCARD_NONEXIST)
+				|| (mo1 == WILDCARD_NONEXIST && mo2 == memory_order_relaxed)
+				|| (mo1 == memory_order_relaxed && mo2 == WILDCARD_NONEXIST)
+				)
+				subResult = 1;
+			else if (mo1 != WILDCARD_NONEXIST && mo2 == WILDCARD_NONEXIST)
+				subResult = -1;
+			else
+				subResult = mo1 > mo2 ? 1 : (mo1 == mo2) ? 0 : -1;
+
+			if ((subResult > 0 && result < 0) || (subResult < 0 && result > 0)) {
+				return -2;
+			}
+			if (subResult != 0)
+				result = subResult;
+		}
+	}
+	return result;
+}
+
+unsigned long Inference::getHash() {
+	unsigned long hash = 0;
+	for (int i = 1; i <= size; i++) {
+		memory_order mo = orders[i];
+		if (mo == WILDCARD_NONEXIST) {
+			mo = memory_order_relaxed;
+		}
+		hash *= 37;
+		hash += (mo + 4096);
+	}
+	return hash;
+}
+
+
+void Inference::print(bool hasHash) {
+	ASSERT(size > 0 && size <= MAX_WILDCARD_NUM);
+	for (int i = 1; i <= size; i++) {
+		memory_order mo = orders[i];
+		if (mo != WILDCARD_NONEXIST) {
+			// Print the wildcard inference result
+			FENCE_PRINT("wildcard %d -> memory_order_%s\n", i, get_mo_str(mo));
+		}
+	}
+	if (hasHash)
+		FENCE_PRINT("Hash: %lu\n", getHash());
+}
+
+void Inference::print() {
+	print(false);
+}