File tree Expand file tree Collapse file tree 2 files changed +7
-3
lines changed Expand file tree Collapse file tree 2 files changed +7
-3
lines changed Original file line number Diff line number Diff line change @@ -26,7 +26,7 @@ struct Event {
26
26
/// kernel. This counter is initialized with the value specified in the argument initval.
27
27
counter : u64 ,
28
28
is_nonblock : bool ,
29
- _clock : VClock ,
29
+ clock : VClock ,
30
30
}
31
31
32
32
impl FileDescription for Event {
@@ -60,6 +60,8 @@ impl FileDescription for Event {
60
60
throw_unsup_format ! ( "eventfd: blocking is unsupported" ) ;
61
61
}
62
62
} else {
63
+ // Prevent false alarm in data race detection when doing synchronisation via eventfd.
64
+ ecx. acquire_clock ( & self . clock ) ;
63
65
// Return the counter in the host endianness using the buffer provided by caller.
64
66
let counter_byte: [ u8 ; 8 ] = match ecx. tcx . sess . target . endian {
65
67
Endian :: Little => self . counter . to_le_bytes ( ) ,
@@ -117,6 +119,8 @@ impl FileDescription for Event {
117
119
throw_unsup_format ! ( "eventfd: blocking is unsupported" ) ;
118
120
}
119
121
} else {
122
+ // Prevent false alarm in data race detection when doing synchronisation via eventfd.
123
+ self . clock . join ( & ecx. release_clock ( ) . unwrap ( ) ) ;
120
124
self . counter = self . counter . checked_add ( num) . unwrap ( ) ;
121
125
}
122
126
Ok ( Ok ( 8 ) )
@@ -174,7 +178,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
174
178
let fd = this. machine . fds . insert_fd ( FileDescriptor :: new ( Event {
175
179
counter : val. into ( ) ,
176
180
is_nonblock,
177
- _clock : VClock :: default ( ) ,
181
+ clock : VClock :: default ( ) ,
178
182
} ) ) ;
179
183
Ok ( Scalar :: from_i32 ( fd) )
180
184
}
Original file line number Diff line number Diff line change 3
3
use std:: thread;
4
4
5
5
fn main ( ) {
6
- // test_read_write();
6
+ test_read_write ( ) ;
7
7
test_race ( ) ;
8
8
}
9
9
You can’t perform that action at this time.
0 commit comments