Skip to content

Commit d28063f

Browse files
committed
Fix #254
The issue was that we did not apply the RMW Atomicity constraint to the store, so it squeezed in between the read and the write part of the RMW. Now, as soon as a RMW has happened (and observed the current value), all future stores must come after that in the modification order of that variable. Fixes #254 Fixes #389
1 parent dbf32b0 commit d28063f

File tree

2 files changed

+162
-28
lines changed

2 files changed

+162
-28
lines changed

src/rt/atomic.rs

Lines changed: 21 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -118,6 +118,12 @@ pub(super) struct State {
118118
/// Last time the atomic was accessed for a store or rmw operation.
119119
last_non_load_access: Option<Access>,
120120

121+
/// Last time the atomic was accessed using an RMW access that did not fail.
122+
///
123+
/// This is used for applying the RMW atomicity constraint to other stores
124+
/// (so they don't squeeze in between the read and write part of the RMW).
125+
last_successful_rmw: VersionVec,
126+
121127
/// Currently tracked stored values. This is the `MAX_ATOMIC_HISTORY` most
122128
/// recent stores to the atomic cell in loom execution order.
123129
stores: [Store; MAX_ATOMIC_HISTORY],
@@ -413,6 +419,7 @@ impl State {
413419
is_mutating: false,
414420
last_access: None,
415421
last_non_load_access: None,
422+
last_successful_rmw: VersionVec::new(),
416423
stores: Default::default(),
417424
cnt: 0,
418425
};
@@ -482,6 +489,9 @@ impl State {
482489
}
483490
}
484491

492+
// RMW Atomicity.
493+
modification_order.join(&self.last_successful_rmw);
494+
485495
sync.sync_store(threads, ordering);
486496

487497
let mut first_seen = FirstSeen::new();
@@ -535,6 +545,10 @@ impl State {
535545
let sync = self.stores[index].sync;
536546
self.store(threads, sync, next, success);
537547

548+
// RMW Atomicity. Future stores must happen after this, because we
549+
// already observed a value.
550+
self.last_successful_rmw.join(&threads.active().causality);
551+
538552
Ok(prev)
539553
}
540554
Err(e) => {
@@ -546,7 +560,7 @@ impl State {
546560

547561
fn apply_load_coherence(&mut self, threads: &mut thread::Set, index: usize) {
548562
for i in 0..self.stores.len() {
549-
// Skip if the is current.
563+
// Skip if it is the current load.
550564
if index == i {
551565
continue;
552566
}
@@ -730,18 +744,9 @@ impl State {
730744
//
731745
// Add all stores **unless** a newer store has already been seen by the
732746
// current thread's causality.
733-
'outer: for i in 0..self.stores.len() {
734-
let store_i = &self.stores[i];
735-
736-
if i >= cnt {
737-
// Not a real store
738-
continue;
739-
}
740-
741-
for j in 0..self.stores.len() {
742-
let store_j = &self.stores[j];
743-
744-
if i == j || j >= cnt {
747+
'outer: for (i, store_i) in self.stores.iter().take(cnt).enumerate() {
748+
for (j, store_j) in self.stores.iter().take(cnt).enumerate() {
749+
if i == j {
745750
continue;
746751
}
747752

@@ -784,18 +789,9 @@ impl State {
784789

785790
// Unlike `match_load_to_stores`, rmw operations only load "newest"
786791
// stores, in terms of modification order.
787-
'outer: for i in 0..self.stores.len() {
788-
let store_i = &self.stores[i];
789-
790-
if i >= cnt {
791-
// Not a real store
792-
continue;
793-
}
794-
795-
for j in 0..self.stores.len() {
796-
let store_j = &self.stores[j];
797-
798-
if i == j || j >= cnt {
792+
'outer: for (i, store_i) in self.stores.iter().take(cnt).enumerate() {
793+
for (j, store_j) in self.stores.iter().take(cnt).enumerate() {
794+
if i == j {
799795
continue;
800796
}
801797

tests/atomic.rs

Lines changed: 141 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11
#![deny(warnings, rust_2018_idioms)]
22

3-
use loom::sync::atomic::AtomicUsize;
3+
use loom::sync::atomic::{AtomicUsize, AtomicBool};
44
use loom::thread;
55

6+
use std::collections::HashSet;
67
use std::sync::atomic::Ordering::{AcqRel, Acquire, Relaxed, Release};
78
use std::sync::Arc;
89

@@ -111,15 +112,152 @@ fn compare_and_swap_reads_old_values() {
111112

112113
#[test]
113114
fn fetch_add_atomic() {
114-
loom::model(|| {
115+
let solutions = std::sync::Arc::new(std::sync::Mutex::new(HashSet::new()));
116+
let solutions1 = std::sync::Arc::clone(&solutions);
117+
118+
loom::model(move || {
115119
let a1 = Arc::new(AtomicUsize::new(0));
116120
let a2 = a1.clone();
117121

118122
let th = thread::spawn(move || a2.fetch_add(1, Relaxed));
119123

120124
let v1 = a1.fetch_add(1, Relaxed);
121125
let v2 = th.join().unwrap();
126+
let v3 = a1.load(Relaxed);
127+
128+
solutions1.lock().unwrap().insert((v1, v2, v3));
129+
});
130+
131+
let solutions = solutions.lock().unwrap();
132+
133+
assert!(solutions.contains(&(0, 1, 2)));
134+
assert!(solutions.contains(&(1, 0, 2)));
135+
assert_eq!(solutions.len(), 2);
136+
}
137+
138+
#[test]
139+
fn store_does_not_squeeze_in_rmw() {
140+
let solutions = std::sync::Arc::new(std::sync::Mutex::new(HashSet::new()));
141+
let solutions1 = std::sync::Arc::clone(&solutions);
142+
143+
loom::model(move || {
144+
let a1 = Arc::new(AtomicUsize::new(0));
145+
let a2 = a1.clone();
146+
147+
let th = thread::spawn(move || {
148+
a1.store(1, Relaxed);
149+
});
150+
151+
let b1 = a2.swap(2, Relaxed);
152+
153+
a2.store(3, Relaxed);
154+
155+
let b2 = a2.swap(4, Relaxed);
156+
157+
th.join().unwrap();
158+
159+
let b3 = a2.load(Relaxed);
160+
161+
solutions1.lock().unwrap().insert((b1, b2, b3));
162+
});
163+
164+
let solutions = solutions.lock().unwrap();
165+
166+
// store(1) before swap(2).
167+
assert!(solutions.contains(&(1, 3, 4)));
168+
169+
// store(1) after swap(2), before store(3).
170+
assert!(solutions.contains(&(0, 3, 4)));
171+
172+
// store(1) after store(3), before swap(4).
173+
assert!(solutions.contains(&(0, 1, 4)));
174+
175+
// store(1) after swap(4) (but before join).
176+
assert!(solutions.contains(&(0, 3, 1)));
177+
178+
assert_eq!(solutions.len(), 4);
179+
}
180+
181+
#[test]
182+
fn store_oncurrent_failed_rmw() {
183+
let solutions = std::sync::Arc::new(std::sync::Mutex::new(HashSet::new()));
184+
let solutions1 = std::sync::Arc::clone(&solutions);
185+
186+
loom::model(move || {
187+
let a1 = Arc::new(AtomicUsize::new(0));
188+
let a2 = a1.clone();
189+
190+
let th = thread::spawn(move || {
191+
a1.store(1, Relaxed);
192+
});
193+
194+
let b1 = a2.compare_exchange(0, 2, Relaxed, Relaxed);
195+
196+
th.join().unwrap();
197+
198+
let b2 = a2.load(Relaxed);
199+
200+
solutions1.lock().unwrap().insert((b1, b2));
201+
});
202+
203+
let solutions = solutions.lock().unwrap();
204+
205+
// store(1) before compare_exchange(0, 2).
206+
assert!(solutions.contains(&(Err(1), 1)));
207+
208+
// store(1) after compare_exchange(0, 2).
209+
assert!(solutions.contains(&(Ok(0), 1)));
210+
211+
assert_eq!(solutions.len(), 2, "{:?}", solutions);
212+
}
213+
214+
#[test]
215+
fn unordered_stores() {
216+
let solutions = std::sync::Arc::new(std::sync::Mutex::new(HashSet::new()));
217+
let solutions1 = std::sync::Arc::clone(&solutions);
218+
219+
loom::model(move || {
220+
let a1 = Arc::new(AtomicUsize::new(0));
221+
let a2 = a1.clone();
122222

123-
assert_ne!(v1, v2);
223+
let th = thread::spawn(move || {
224+
a1.store(1, Relaxed);
225+
});
226+
227+
a2.store(2, Relaxed);
228+
229+
th.join().unwrap();
230+
231+
let b = a2.load(Relaxed);
232+
233+
solutions1.lock().unwrap().insert(b);
124234
});
235+
236+
let solutions = solutions.lock().unwrap();
237+
238+
assert!(solutions.contains(&1));
239+
assert!(solutions.contains(&2));
240+
241+
assert_eq!(solutions.len(), 2);
125242
}
243+
244+
// See issue https://github.com/tokio-rs/loom/issues/254
245+
#[test]
246+
fn concurrent_rmw_store() {
247+
loom::model(move || {
248+
let flag = Arc::new(AtomicBool::new(false));
249+
250+
let th = thread::spawn({
251+
let flag = flag.clone();
252+
move || flag.store(true, Relaxed) // a.k.a. unlock()
253+
});
254+
255+
if flag.swap(false, Relaxed) { // a.k.a. if !try_lock { return }
256+
return;
257+
}
258+
259+
th.join().unwrap();
260+
261+
assert!(flag.load(Relaxed)); // a.k.a. is_locked().
262+
});
263+
}

0 commit comments

Comments
 (0)