From: Brian Norris <banorris@uci.edu>
Date: Thu, 7 Jun 2012 00:34:47 +0000 (-0700)
Subject: libatomic: perform write before context switch
X-Git-Tag: pldi2013~391^2~38
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c9aa5d5129131b926d7589d831f4bb6f31393e0a;p=model-checker.git
libatomic: perform write before context switch
Atomic actions block a thread at the "switch_to_master" function call, so under
the current structure (which isn't quite fit for relaxed modeling yet...) we
should perform the memory write before calling "switch_to_master".
If not, we can observe sequences like the following, where x is an atomic
variable. All actions are seq_cst:
Initially, x = 0
Thread Action
------ ------
1 r1 = x; // r1 = 0
1 x = r1 + 1; // x = 1, not stored yet?
2 r2 = x; // r2 = 0
2 x = r2 // x = 1, not stored yet?
Then, depending on scheduling, Thread 1 or Thread 2 might complete first, with
its write being performed *after* it receives control again.
---
diff --git a/libatomic.cc b/libatomic.cc
index 88d7fbf..507f685 100644
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -5,8 +5,8 @@
void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
{
DBG();
- model->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
obj->value = value;
+ model->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
}
int atomic_load_explicit(struct atomic_object *obj, memory_order order)