From: Brian Norris 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)