std: Unsafe-wrap std::sync · model-checking/verify-rust-std@5ff7b40 (original) (raw)
`@@ -91,7 +91,7 @@ impl Block {
`
91
91
`` // It is not necessary to set the DESTROY bit in the last slot because that slot has
``
92
92
`// begun destruction of the block.
`
93
93
`for i in start..BLOCK_CAP - 1 {
`
94
``
`-
let slot = (*this).slots.get_unchecked(i);
`
``
94
`+
let slot = unsafe { (*this).slots.get_unchecked(i) };
`
95
95
``
96
96
`` // Mark the DESTROY bit if a thread is still using the slot.
``
97
97
`if slot.state.load(Ordering::Acquire) & READ == 0
`
`@@ -103,7 +103,7 @@ impl Block {
`
103
103
`}
`
104
104
``
105
105
`// No thread is using the block, now it is safe to destroy it.
`
106
``
`-
drop(Box::from_raw(this));
`
``
106
`+
drop(unsafe { Box::from_raw(this) });
`
107
107
`}
`
108
108
`}
`
109
109
``
`@@ -265,9 +265,11 @@ impl Channel {
`
265
265
`// Write the message into the slot.
`
266
266
`let block = token.list.block as *mut Block;
`
267
267
`let offset = token.list.offset;
`
268
``
`-
let slot = (*block).slots.get_unchecked(offset);
`
269
``
`-
slot.msg.get().write(MaybeUninit::new(msg));
`
270
``
`-
slot.state.fetch_or(WRITE, Ordering::Release);
`
``
268
`+
unsafe {
`
``
269
`+
let slot = (*block).slots.get_unchecked(offset);
`
``
270
`+
slot.msg.get().write(MaybeUninit::new(msg));
`
``
271
`+
slot.state.fetch_or(WRITE, Ordering::Release);
`
``
272
`+
}
`
271
273
``
272
274
`// Wake a sleeping receiver.
`
273
275
`self.receivers.notify();
`
`@@ -369,19 +371,21 @@ impl Channel {
`
369
371
`// Read the message.
`
370
372
`let block = token.list.block as *mut Block;
`
371
373
`let offset = token.list.offset;
`
372
``
`-
let slot = (*block).slots.get_unchecked(offset);
`
373
``
`-
slot.wait_write();
`
374
``
`-
let msg = slot.msg.get().read().assume_init();
`
375
``
-
376
``
`-
// Destroy the block if we've reached the end, or if another thread wanted to destroy but
`
377
``
`-
// couldn't because we were busy reading from the slot.
`
378
``
`-
if offset + 1 == BLOCK_CAP {
`
379
``
`-
Block::destroy(block, 0);
`
380
``
`-
} else if slot.state.fetch_or(READ, Ordering::AcqRel) & DESTROY != 0 {
`
381
``
`-
Block::destroy(block, offset + 1);
`
382
``
`-
}
`
``
374
`+
unsafe {
`
``
375
`+
let slot = (*block).slots.get_unchecked(offset);
`
``
376
`+
slot.wait_write();
`
``
377
`+
let msg = slot.msg.get().read().assume_init();
`
``
378
+
``
379
`+
// Destroy the block if we've reached the end, or if another thread wanted to destroy but
`
``
380
`+
// couldn't because we were busy reading from the slot.
`
``
381
`+
if offset + 1 == BLOCK_CAP {
`
``
382
`+
Block::destroy(block, 0);
`
``
383
`+
} else if slot.state.fetch_or(READ, Ordering::AcqRel) & DESTROY != 0 {
`
``
384
`+
Block::destroy(block, offset + 1);
`
``
385
`+
}
`
383
386
``
384
``
`-
Ok(msg)
`
``
387
`+
Ok(msg)
`
``
388
`+
}
`
385
389
`}
`
386
390
``
387
391
`/// Attempts to send a message into the channel.
`