From: Brian Norris <banorris@uci.edu>
Date: Tue, 15 May 2012 17:12:04 +0000 (-0700)
Subject: libatomic: place the proper read-value in 'atomic_load' ModelActions
X-Git-Tag: pldi2013~437
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b008782b8c3eb2b845eb9514ae3cdd025fec9c8b;p=model-checker.git

libatomic: place the proper read-value in 'atomic_load' ModelActions

Even though I was doing rudimentary loading and storing of atomic values, I
didn't properly record the value in the ModelAction. That will be confusing
soon if I don't fix it. So fix it.
---

diff --git a/libatomic.cc b/libatomic.cc
index f552d93..88d7fbf 100644
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -11,9 +11,10 @@ void atomic_store_explicit(struct atomic_object *obj, int value, memory_order or
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
 {
+	int value = obj->value;
 	DBG();
-	model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
-	return obj->value;
+	model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, value));
+	return value;
 }
 
 void atomic_init(struct atomic_object *obj, int value)