mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Fix span management

Browse Source
This commit is contained in:
Ben Kimock 2022-12-20 22:48:23 -05:00
parent d1184ae58d
commit d2e1c3738e
15 changed files with 42 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/tools/miri/src/concurrency/data_race.rs
View File

@ -51,7 +51,6 @@
use rustc_index::vec::{Idx, IndexVec};
use rustc_middle::mir;
use rustc_span::Span;
use rustc_span::DUMMY_SP;
use rustc_target::abi::{Align, Size};
use crate::diagnostics::RacingOp;
@ -398,7 +397,10 @@ fn read_race_detect(
current_span: Span,
) -> Result<(), DataRace> {
log::trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, clocks);
let res = if self.write <= clocks.clock[self.write_index] {
if !current_span.is_dummy() {
clocks.clock[index].span = current_span;
}
if self.write <= clocks.clock[self.write_index] {
let race_free = if let Some(atomic) = self.atomic() {
atomic.write_vector <= clocks.clock
} else {
@ -408,11 +410,7 @@ fn read_race_detect(
if race_free { Ok(()) } else { Err(DataRace) }
} else {
Err(DataRace)
};
if res.is_ok() && current_span != DUMMY_SP {
clocks.clock[index].span = current_span;
}
res
}
/// Detect races for non-atomic write operations at the current memory cell
@ -425,7 +423,7 @@ fn write_race_detect(
current_span: Span,
) -> Result<(), DataRace> {
log::trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, clocks);
if current_span != DUMMY_SP {
if !current_span.is_dummy() {
clocks.clock[index].span = current_span;
}
if self.write <= clocks.clock[self.write_index] && self.read <= clocks.clock {
@ -712,9 +710,7 @@ pub fn new_allocation(
| MemoryKind::Stack => {
let (alloc_index, clocks) = global.current_thread_state(thread_mgr);
let mut alloc_timestamp = clocks.clock[alloc_index];
if current_span != DUMMY_SP {
alloc_timestamp.span = current_span;
}
alloc_timestamp.span = current_span;
(alloc_timestamp, alloc_index)
}
// Other global memory should trace races but be allocated at the 0 timestamp.

21
src/tools/miri/src/concurrency/vector_clock.rs
View File

@ -45,8 +45,9 @@ fn from(id: u32) -> Self {
/// clock vectors larger than this will be stored on the heap
const SMALL_VECTOR: usize = 4;
/// The type of the time-stamps recorded in the data-race detector
/// set to a type of unsigned integer
/// The time-stamps recorded in the data-race detector consist of both
/// a 32-bit unsigned integer which is the actual timestamp, and a `Span`
/// so that diagnostics can report what code was responsible for an operation.
#[derive(Clone, Copy, Debug, Eq)]
pub struct VTimestamp {
time: u32,
@ -128,7 +129,7 @@ pub fn increment_index(&mut self, idx: VectorIdx, current_span: Span) {
let mut_slice = self.get_mut_with_min_len(idx + 1);
let idx_ref = &mut mut_slice[idx];
idx_ref.time = idx_ref.time.checked_add(1).expect("Vector clock overflow");
if current_span != DUMMY_SP {
if !current_span.is_dummy() {
idx_ref.span = current_span;
}
}
@ -143,14 +144,7 @@ pub fn join(&mut self, other: &Self) {
let l_span = l.span;
let r_span = r.span;
*l = r.max(*l);
if l.span == DUMMY_SP {
if r_span != DUMMY_SP {
l.span = r_span;
}
if l_span != DUMMY_SP {
l.span = l_span;
}
}
l.span = l.span.substitute_dummy(r_span).substitute_dummy(l_span);
}
}
@ -162,9 +156,8 @@ pub fn set_at_index(&mut self, other: &Self, idx: VectorIdx) {
mut_slice[idx.index()] = other[idx];
if other[idx].span == DUMMY_SP {
mut_slice[idx.index()].span = prev_span;
}
let span = &mut mut_slice[idx.index()].span;
*span = span.substitute_dummy(prev_span);
}
/// Set the vector to the all-zero vector

2
src/tools/miri/tests/fail/data_race/alloc_read_race.stderr
View File

@ -8,7 +8,7 @@ help: The Read on thread `<unnamed>` is here
--> $DIR/alloc_read_race.rs:LL:CC
|
LL | ... *pointer.load(Ordering::Relaxed)
| ^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: The Allocate on thread `<unnamed>` is here
--> $DIR/alloc_read_race.rs:LL:CC
|

6
src/tools/miri/tests/fail/data_race/atomic_write_na_read_race1.stderr
View File

@ -5,10 +5,10 @@ LL | *atomic_ref.get_mut()
| ^^^^^^^^^^^^^^^^^^^^^ Data race detected between Read on thread `<unnamed>` and Atomic Store on thread `<unnamed>` at ALLOC
|
help: The Read on thread `<unnamed>` is here
--> RUSTLIB/core/src/ptr/mod.rs:LL:CC
--> $DIR/atomic_write_na_read_race1.rs:LL:CC
|
LL | }
| ^
LL | *atomic_ref.get_mut()
| ^^^^^^^^^^^^^^^^^^^^^
help: The Atomic Store on thread `<unnamed>` is here
--> $DIR/atomic_write_na_read_race1.rs:LL:CC
|

6
src/tools/miri/tests/fail/data_race/atomic_write_na_read_race2.stderr
View File

@ -10,10 +10,10 @@ help: The Atomic Store on thread `<unnamed>` is here
LL | ... (&*c.0).store(32, Ordering::SeqCst);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: The Read on thread `<unnamed>` is here
--> RUSTLIB/core/src/ptr/mod.rs:LL:CC
--> $DIR/atomic_write_na_read_race2.rs:LL:CC
|
LL | }
| ^
LL | let _val = *(c.0 as *mut usize);
| ^^^^^^^^^^^^^^^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:

6
src/tools/miri/tests/fail/data_race/dealloc_read_race1.stderr
View File

@ -20,10 +20,10 @@ LL | | std::mem::align_of::<usize>(),
LL | | );
| |_____________^
help: The Read on thread `<unnamed>` is here
--> RUSTLIB/core/src/ptr/mod.rs:LL:CC
--> $DIR/dealloc_read_race1.rs:LL:CC
|
LL | }
| ^
LL | let _val = *ptr.0;
| ^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:

2
src/tools/miri/tests/fail/data_race/dealloc_read_race_stack.stderr
View File

@ -13,7 +13,7 @@ help: The Read on thread `<unnamed>` is here
--> $DIR/dealloc_read_race_stack.rs:LL:CC
|
LL | *pointer.load(Ordering::Acquire)
| ^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:

6
src/tools/miri/tests/fail/data_race/read_write_race.stderr
View File

@ -10,10 +10,10 @@ help: The Write on thread `<unnamed>` is here
LL | *c.0 = 64;
| ^^^^^^^^^
help: The Read on thread `<unnamed>` is here
--> RUSTLIB/core/src/ptr/mod.rs:LL:CC
--> $DIR/read_write_race.rs:LL:CC
|
LL | }
| ^
LL | let _val = *c.0;
| ^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:

4
src/tools/miri/tests/fail/data_race/read_write_race_stack.stderr
View File

@ -7,8 +7,8 @@ LL | stack_var
help: The Read on thread `<unnamed>` is here
--> $DIR/read_write_race_stack.rs:LL:CC
|
LL | sleep(Duration::from_millis(200));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
LL | stack_var
| ^^^^^^^^^
help: The Write on thread `<unnamed>` is here
--> $DIR/read_write_race_stack.rs:LL:CC
|

4
src/tools/miri/tests/fail/data_race/relax_acquire_race.stderr
View File

@ -7,8 +7,8 @@ LL | *c.0
help: The Read on thread `<unnamed>` is here
--> $DIR/relax_acquire_race.rs:LL:CC
|
LL | if SYNC.load(Ordering::Acquire) == 2 {
| ^
LL | *c.0
| ^^^^
help: The Write on thread `<unnamed>` is here
--> $DIR/relax_acquire_race.rs:LL:CC
|

4
src/tools/miri/tests/fail/data_race/release_seq_race.stderr
View File

@ -7,8 +7,8 @@ LL | *c.0
help: The Read on thread `<unnamed>` is here
--> $DIR/release_seq_race.rs:LL:CC
|
LL | if SYNC.load(Ordering::Acquire) == 3 {
| ^
LL | *c.0
| ^^^^
help: The Write on thread `<unnamed>` is here
--> $DIR/release_seq_race.rs:LL:CC
|

4
src/tools/miri/tests/fail/data_race/release_seq_race_same_thread.stderr
View File

@ -7,8 +7,8 @@ LL | *c.0
help: The Read on thread `<unnamed>` is here
--> $DIR/release_seq_race_same_thread.rs:LL:CC
|
LL | if SYNC.load(Ordering::Acquire) == 2 {
| ^
LL | *c.0
| ^^^^
help: The Write on thread `<unnamed>` is here
--> $DIR/release_seq_race_same_thread.rs:LL:CC
|

4
src/tools/miri/tests/fail/data_race/rmw_race.stderr
View File

@ -7,8 +7,8 @@ LL | *c.0
help: The Read on thread `<unnamed>` is here
--> $DIR/rmw_race.rs:LL:CC
|
LL | if SYNC.load(Ordering::Acquire) == 3 {
| ^
LL | *c.0
| ^^^^
help: The Write on thread `<unnamed>` is here
--> $DIR/rmw_race.rs:LL:CC
|

6
src/tools/miri/tests/fail/data_race/stack_pop_race.stderr
View File

@ -10,10 +10,10 @@ help: The Deallocate on thread `main` is here
LL | }
| ^
help: The Read on thread `<unnamed>` is here
--> RUSTLIB/core/src/ptr/mod.rs:LL:CC
--> $DIR/stack_pop_race.rs:LL:CC
|
LL | }
| ^
LL | let _val = unsafe { *ptr.0 };
| ^^^^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:

4
src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.stderr
View File

@ -12,8 +12,8 @@ LL | *p = 5;
help: The Read on thread `<unnamed>` is here
--> $DIR/retag_data_race_read.rs:LL:CC
|
LL | let t1 = std::thread::spawn(move || thread_1(p));
| ^
LL | let _r = &*p;
| ^^^
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE: