1 #include "fence_common.h"
7 /** Forward declaration */
13 bool isTheInference(Inference *infer) {
14 for (int i = 0; i < infer->getSize(); i++) {
15 memory_order mo1 = (*infer)[i], mo2;
16 if (mo1 == WILDCARD_NONEXIST)
35 const char* get_mo_str(memory_order order) {
37 case std::memory_order_relaxed: return "relaxed";
38 case std::memory_order_acquire: return "acquire";
39 case std::memory_order_release: return "release";
40 case std::memory_order_acq_rel: return "acq_rel";
41 case std::memory_order_seq_cst: return "seq_cst";
43 //model_print("Weird memory order, a bug or something!\n");
44 //model_print("memory_order: %d\n", order);
50 void Inference::resize(int newsize) {
51 ASSERT (newsize > size && newsize <= MAX_WILDCARD_NUM);
52 memory_order *newOrders = (memory_order *) model_malloc((newsize + 1) * sizeof(memory_order*));
54 for (i = 0; i <= size; i++)
55 newOrders[i] = orders[i];
56 for (; i <= newsize; i++)
57 newOrders[i] = WILDCARD_NONEXIST;
63 /** Return the state of how we update a specific mo; If we have to make an
64 * uncompatible inference or that inference cannot be imposed because it's
65 * not a wildcard, it returns -1; if it is a compatible memory order but the
66 * current memory order is no weaker than mo, it returns 0; otherwise, it
67 * does strengthen the order, and returns 1 */
68 int Inference::strengthen(const ModelAction *act, memory_order mo) {
69 memory_order wildcard = act->get_original_mo();
70 int wildcardID = get_wildcard_id_zero(wildcard);
71 if (!is_wildcard(wildcard)) {
72 FENCE_PRINT("We cannot make this update to %s!\n", get_mo_str(mo));
76 if (wildcardID > size)
78 ASSERT (is_normal_mo(mo));
79 //model_print("wildcardID -> order: %d -> %d\n", wildcardID, orders[wildcardID]);
80 ASSERT (is_normal_mo_infer(orders[wildcardID]));
81 switch (orders[wildcardID]) {
82 case memory_order_seq_cst:
84 case memory_order_relaxed:
85 if (mo == memory_order_relaxed)
87 orders[wildcardID] = mo;
89 case memory_order_acquire:
90 if (mo == memory_order_acquire || mo == memory_order_relaxed)
92 if (mo == memory_order_release)
93 orders[wildcardID] = memory_order_acq_rel;
94 else if (mo >= memory_order_acq_rel && mo <=
96 orders[wildcardID] = mo;
98 case memory_order_release:
99 if (mo == memory_order_release || mo == memory_order_relaxed)
101 if (mo == memory_order_acquire)
102 orders[wildcardID] = memory_order_acq_rel;
103 else if (mo >= memory_order_acq_rel)
104 orders[wildcardID] = mo;
106 case memory_order_acq_rel:
107 if (mo == memory_order_seq_cst)
108 orders[wildcardID] = mo;
113 orders[wildcardID] = mo;
119 Inference::Inference() {
120 orders = (memory_order *) model_malloc((4 + 1) * sizeof(memory_order*));
122 for (int i = 0; i <= size; i++)
123 orders[i] = WILDCARD_NONEXIST;
132 Inference::Inference(Inference *infer) {
133 ASSERT (infer->size > 0 && infer->size <= MAX_WILDCARD_NUM);
134 orders = (memory_order *) model_malloc((infer->size + 1) * sizeof(memory_order*));
135 this->size = infer->size;
136 for (int i = 0; i <= size; i++)
137 orders[i] = infer->orders[i];
139 initialInfer = infer->initialInfer;
149 * 1 -> mo1 stronger than mo2;
150 * -1 -> mo1 weaker than mo2;
151 * 2 -> mo1 & mo2 are uncomparable.
153 int Inference::compareMemoryOrder(memory_order mo1, memory_order mo2) {
154 if (mo1 == WILDCARD_NONEXIST)
155 mo1 = memory_order_relaxed;
156 if (mo2 == WILDCARD_NONEXIST)
157 mo2 = memory_order_relaxed;
160 if (mo1 == memory_order_relaxed)
162 if (mo1 == memory_order_acquire) {
163 if (mo2 == memory_order_relaxed)
165 if (mo2 == memory_order_release)
169 if (mo1 == memory_order_release) {
170 if (mo2 == memory_order_relaxed)
172 if (mo2 == memory_order_acquire)
176 if (mo1 == memory_order_acq_rel) {
177 if (mo2 == memory_order_seq_cst)
182 // mo1 now must be SC and mo2 can't be SC
187 /** Try to calculate the set of inferences that are weaker than this, but
188 * still stronger than infer */
189 InferenceList* Inference::getWeakerInferences(Inference *infer) {
190 // An array of strengthened wildcards
191 SnapVector<int> *strengthened = new SnapVector<int>;
192 model_print("Strengthened wildcards\n");
193 for (int i = 1; i <= size; i++) {
194 memory_order mo1 = orders[i],
196 int compVal = compareMemoryOrder(mo1, mo2);
197 if (!(compVal == 0 || compVal == 1)) {
198 model_print("assert failure\n");
199 model_print("compVal=%d\n", compVal);
202 if (compVal == 0) // Same
204 model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1),
206 strengthened->push_back(i);
209 // Got the strengthened wildcards, find out weaker inferences
210 // First get a volatile copy of this inference
211 Inference *tmpRes = new Inference(this);
212 InferenceList *res = new InferenceList;
213 if (strengthened->size() == 0)
215 getWeakerInferences(res, tmpRes, this, infer, strengthened, 0);
218 InferenceList::print(res, "Weakened");
223 // seq_cst -> acq_rel -> acquire -> release -> relaxed
224 memory_order Inference::nextWeakOrder(memory_order mo1, memory_order mo2) {
227 case memory_order_seq_cst:
228 res = memory_order_acq_rel;
230 case memory_order_acq_rel:
231 res = memory_order_acquire;
233 case memory_order_acquire:
234 res = memory_order_relaxed;
236 case memory_order_release:
237 res = memory_order_relaxed;
239 case memory_order_relaxed:
240 res = memory_order_relaxed;
243 res = memory_order_relaxed;
246 int compVal = compareMemoryOrder(res, mo2);
247 if (compVal == 2 || compVal == -1) // Incomparable
252 void Inference::getWeakerInferences(InferenceList* list, Inference *tmpRes,
253 Inference *infer1, Inference *infer2, SnapVector<int> *strengthened, unsigned idx) {
254 if (idx == strengthened->size()) { // Ready to produce one weakened result
255 Inference *res = new Inference(tmpRes);
256 //model_print("Weakened inference:\n");
258 res->setShouldFix(false);
259 list->push_back(res);
263 int w = (*strengthened)[idx]; // The wildcard
264 memory_order mo1 = (*infer1)[w];
265 memory_order mo2 = (*infer2)[w];
266 if (mo2 == WILDCARD_NONEXIST)
267 mo2 = memory_order_relaxed;
268 memory_order weakenedMO = mo1;
270 (*tmpRes)[w] = weakenedMO;
271 getWeakerInferences(list, tmpRes, infer1, infer2,
272 strengthened, idx + 1);
273 if (weakenedMO == memory_order_acq_rel) {
274 (*tmpRes)[w] = memory_order_release;
275 getWeakerInferences(list, tmpRes, infer1, infer2,
276 strengthened, idx + 1);
278 weakenedMO = nextWeakOrder(weakenedMO, mo2);
279 model_print("weakendedMO=%d\n", weakenedMO);
280 model_print("mo2=%d\n", mo2);
281 } while (weakenedMO != mo2);
282 (*tmpRes)[w] = weakenedMO;
283 getWeakerInferences(list, tmpRes, infer1, infer2,
284 strengthened, idx + 1);
287 memory_order& Inference::operator[](int idx) {
288 if (idx > 0 && idx <= size)
292 orders[idx] = WILDCARD_NONEXIST;
297 /** A simple overload, which allows caller to pass two boolean refrence, and
298 * we will set those two variables indicating whether we can update the
299 * order (copatible or not) and have updated the order */
300 int Inference::strengthen(const ModelAction *act, memory_order mo, bool &canUpdate, bool &hasUpdated) {
301 int res = strengthen(act, mo);
314 INFERENCE_INCOMPARABLE(x) -> true means incomparable
316 int Inference::compareTo(const Inference *infer) const {
317 int result = size == infer->size ? 0 : (size > infer->size) ? 1 : -1;
318 int smallerSize = size > infer->size ? infer->size : size;
321 for (int i = 0; i <= smallerSize; i++) {
322 memory_order mo1 = orders[i],
323 mo2 = infer->orders[i];
324 if ((mo1 == memory_order_acquire && mo2 == memory_order_release) ||
325 (mo1 == memory_order_release && mo2 == memory_order_acquire)) {
329 if ((mo1 == WILDCARD_NONEXIST && mo2 != WILDCARD_NONEXIST)
330 || (mo1 == WILDCARD_NONEXIST && mo2 == memory_order_relaxed)
331 || (mo1 == memory_order_relaxed && mo2 == WILDCARD_NONEXIST)
334 else if (mo1 != WILDCARD_NONEXIST && mo2 == WILDCARD_NONEXIST)
337 subResult = mo1 > mo2 ? 1 : (mo1 == mo2) ? 0 : -1;
339 if ((subResult > 0 && result < 0) || (subResult < 0 && result > 0)) {
349 unsigned long Inference::getHash() {
350 unsigned long hash = 0;
351 for (int i = 1; i <= size; i++) {
352 memory_order mo = orders[i];
353 if (mo == WILDCARD_NONEXIST) {
354 mo = memory_order_relaxed;
363 void Inference::print(bool hasHash) {
364 ASSERT(size > 0 && size <= MAX_WILDCARD_NUM);
365 for (int i = 1; i <= size; i++) {
366 memory_order mo = orders[i];
367 if (mo != WILDCARD_NONEXIST) {
368 // Print the wildcard inference result
369 FENCE_PRINT("wildcard %d -> memory_order_%s\n", i, get_mo_str(mo));
373 FENCE_PRINT("Hash: %lu\n", getHash());
376 void Inference::print() {