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

Auto merge of #2240 - RalfJung:readme, r=RalfJung

Browse Source 
readme

Emulation of weak memory effects is not a kind of UB, so put it into a separate paragraph. Also remove the note about incomplete threading support. :)
This commit is contained in:
bors 2022-06-19 16:19:48 +00:00
commit 2baabf796c
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
README.md
View File

@ -21,12 +21,15 @@ for example:
* **Experimental**: Violations of the [Stacked Borrows] rules governing aliasing
for reference types
* **Experimental**: Data races
* **Experimental**: Emulation of weak memory effects (i.e., reads can return outdated values)
On top of that, Miri will also tell you about memory leaks: when there is memory
still allocated at the end of the execution, and that memory is not reachable
from a global `static`, Miri will raise an error.
Miri supports almost all Rust language features; in particular, unwinding and
concurrency are properly supported (including some experimental emulation of
weak memory effects, i.e., reads can return outdated values).
You can use Miri to emulate programs on other targets, e.g. to ensure that
byte-level data manipulation works correctly both on little-endian and
big-endian systems. See
@ -62,8 +65,6 @@ in your program, and cannot run all programs:
not support networking. System API support varies between targets; if you run
on Windows it is a good idea to use `--target x86_64-unknown-linux-gnu` to get
better support.
* Threading support is not finished yet. E.g. spin loops (without syscalls) just
loop forever. There is no threading support on Windows.
* Weak memory emulation may produce weak behaivours unobservable by compiled
programs running on real hardware when `SeqCst` fences are used, and it cannot
produce all behaviors possibly observable on real hardware.