Skip to content

Commit e14780a

Browse files
authored
Merge pull request rust-lang#4672 from RalfJung/sync-objs
Make pthread and other "native" synchronization objects more resilient
2 parents f796155 + d6b01ab commit e14780a

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

41 files changed

+714
-247
lines changed

src/tools/miri/src/borrow_tracker/mod.rs

Lines changed: 16 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,22 @@ use crate::*;
1111
pub mod stacked_borrows;
1212
pub mod tree_borrows;
1313

14+
/// Indicates which kind of access is being performed.
15+
#[derive(Copy, Clone, Hash, PartialEq, Eq, Debug)]
16+
pub enum AccessKind {
17+
Read,
18+
Write,
19+
}
20+
21+
impl fmt::Display for AccessKind {
22+
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
23+
match self {
24+
AccessKind::Read => write!(f, "read access"),
25+
AccessKind::Write => write!(f, "write access"),
26+
}
27+
}
28+
}
29+
1430
/// Tracking pointer provenance
1531
#[derive(Copy, Clone, Hash, PartialEq, Eq, PartialOrd, Ord)]
1632
pub struct BorTag(NonZero<u64>);
@@ -115,15 +131,6 @@ impl VisitProvenance for GlobalStateInner {
115131
/// We need interior mutable access to the global state.
116132
pub type GlobalState = RefCell<GlobalStateInner>;
117133

118-
impl fmt::Display for AccessKind {
119-
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
120-
match self {
121-
AccessKind::Read => write!(f, "read access"),
122-
AccessKind::Write => write!(f, "write access"),
123-
}
124-
}
125-
}
126-
127134
/// Policy on whether to recurse into fields to retag
128135
#[derive(Copy, Clone, Debug)]
129136
pub enum RetagFields {

src/tools/miri/src/borrow_tracker/stacked_borrows/diagnostics.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use rustc_data_structures::fx::FxHashSet;
55
use rustc_span::{Span, SpanData};
66
use smallvec::SmallVec;
77

8-
use crate::borrow_tracker::{GlobalStateInner, ProtectorKind};
8+
use crate::borrow_tracker::{AccessKind, GlobalStateInner, ProtectorKind};
99
use crate::*;
1010

1111
/// Error reporting

src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ pub use self::stack::Stack;
2121
use crate::borrow_tracker::stacked_borrows::diagnostics::{
2222
AllocHistory, DiagnosticCx, DiagnosticCxBuilder,
2323
};
24-
use crate::borrow_tracker::{GlobalStateInner, ProtectorKind};
24+
use crate::borrow_tracker::{AccessKind, GlobalStateInner, ProtectorKind};
2525
use crate::concurrency::data_race::{NaReadType, NaWriteType};
2626
use crate::*;
2727

src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,10 @@ use std::ops::Range;
44
use rustc_data_structures::fx::FxHashMap;
55
use rustc_span::{Span, SpanData};
66

7-
use crate::borrow_tracker::ProtectorKind;
87
use crate::borrow_tracker::tree_borrows::perms::{PermTransition, Permission};
98
use crate::borrow_tracker::tree_borrows::tree::LocationState;
109
use crate::borrow_tracker::tree_borrows::unimap::UniIndex;
10+
use crate::borrow_tracker::{AccessKind, ProtectorKind};
1111
use crate::*;
1212

1313
/// Cause of an access: either a real access or one

src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ use rustc_middle::ty::{self, Ty};
55

66
use self::foreign_access_skipping::IdempotentForeignAccess;
77
use self::tree::LocationState;
8-
use crate::borrow_tracker::{GlobalState, GlobalStateInner, ProtectorKind};
8+
use crate::borrow_tracker::{AccessKind, GlobalState, GlobalStateInner, ProtectorKind};
99
use crate::concurrency::data_race::NaReadType;
1010
use crate::*;
1111

src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
use std::cmp::{Ordering, PartialOrd};
22
use std::fmt;
33

4-
use crate::AccessKind;
4+
use crate::borrow_tracker::AccessKind;
55
use crate::borrow_tracker::tree_borrows::diagnostics::TransitionError;
66
use crate::borrow_tracker::tree_borrows::tree::AccessRelatedness;
77

src/tools/miri/src/borrow_tracker/tree_borrows/tree.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ use crate::borrow_tracker::tree_borrows::diagnostics::{
2525
use crate::borrow_tracker::tree_borrows::foreign_access_skipping::IdempotentForeignAccess;
2626
use crate::borrow_tracker::tree_borrows::perms::PermTransition;
2727
use crate::borrow_tracker::tree_borrows::unimap::{UniIndex, UniKeyMap, UniValMap};
28-
use crate::borrow_tracker::{GlobalState, ProtectorKind};
28+
use crate::borrow_tracker::{AccessKind, GlobalState, ProtectorKind};
2929
use crate::*;
3030

3131
mod tests;

src/tools/miri/src/concurrency/init_once.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,10 @@ impl InitOnceRef {
5757
pub fn begin(&self) {
5858
self.0.borrow_mut().begin();
5959
}
60+
61+
pub fn queue_is_empty(&self) -> bool {
62+
self.0.borrow().waiters.is_empty()
63+
}
6064
}
6165

6266
impl VisitProvenance for InitOnceRef {

0 commit comments

Comments
 (0)