|
1 | 1 | //! Implementation of C++11-consistent weak memory emulation using store buffers |
2 | 2 | //! based on Dynamic Race Detection for C++ ("the paper"): |
3 | | -//! https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf |
| 3 | +//! <https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf> |
4 | 4 | //! |
5 | 5 | //! This implementation will never generate weak memory behaviours forbidden by the C++11 model, |
6 | 6 | //! but it is incapable of producing all possible weak behaviours allowed by the model. There are |
7 | 7 | //! certain weak behaviours observable on real hardware but not while using this. |
8 | 8 | //! |
9 | 9 | //! Note that this implementation does not take into account of C++20's memory model revision to SC accesses |
10 | | -//! and fences introduced by P0668 (https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html). |
| 10 | +//! and fences introduced by P0668 (<https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html>). |
11 | 11 | //! This implementation is not fully correct under the revised C++20 model and may generate behaviours C++20 |
12 | 12 | //! disallows. |
13 | 13 | //! |
14 | 14 | //! Rust follows the C++20 memory model (except for the Consume ordering and some operations not performable through C++'s |
15 | 15 | //! std::atomic<T> API). It is therefore possible for this implementation to generate behaviours never observable when the |
16 | 16 | //! same program is compiled and run natively. Unfortunately, no literature exists at the time of writing which proposes |
17 | 17 | //! an implementable and C++20-compatible relaxed memory model that supports all atomic operation existing in Rust. The closest one is |
18 | | -//! A Promising Semantics for Relaxed-Memory Concurrency by Jeehoon Kang et al. (https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf) |
| 18 | +//! A Promising Semantics for Relaxed-Memory Concurrency by Jeehoon Kang et al. (<https://www.cs.tau.ac.il/~orilahav/papers/popl17.pdf>) |
19 | 19 | //! However, this model lacks SC accesses and is therefore unusable by Miri (SC accesses are everywhere in library code). |
20 | 20 | //! |
21 | 21 | //! If you find anything that proposes a relaxed memory model that is C++20-consistent, supports all orderings Rust's atomic accesses |
22 | 22 | //! and fences accept, and is implementable (with operational semanitcs), please open a GitHub issue! |
23 | 23 | //! |
24 | 24 | //! One characteristic of this implementation, in contrast to some other notable operational models such as ones proposed in |
25 | | -//! Taming Release-Acquire Consistency by Ori Lahav et al. (https://plv.mpi-sws.org/sra/paper.pdf) or Promising Semantics noted above, |
| 25 | +//! Taming Release-Acquire Consistency by Ori Lahav et al. (<https://plv.mpi-sws.org/sra/paper.pdf>) or Promising Semantics noted above, |
26 | 26 | //! is that this implementation does not require each thread to hold an isolated view of the entire memory. Here, store buffers are per-location |
27 | 27 | //! and shared across all threads. This is more memory efficient but does require store elements (representing writes to a location) to record |
28 | 28 | //! information about reads, whereas in the other two models it is the other way round: reads points to the write it got its value from. |
|
38 | 38 | //! on the next non-atomic or imperfectly overlapping atomic access to that region. |
39 | 39 | //! These lazy (de)allocations happen in memory_accessed() on non-atomic accesses, and |
40 | 40 | //! get_or_create_store_buffer() on atomic accesses. This mostly works well, but it does |
41 | | -//! lead to some issues (https://github.com/rust-lang/miri/issues/2164). |
| 41 | +//! lead to some issues (<https://github.com/rust-lang/miri/issues/2164>). |
42 | 42 | //! |
43 | 43 | //! One consequence of this difference is that safe/sound Rust allows for more operations on atomic locations |
44 | 44 | //! than the C++20 atomic API was intended to allow, such as non-atomically accessing |
|
0 commit comments