Model-checks x86-TSO litmus test, in TLC style.
For x86-TSO, see x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors for details.
See sb.rs, corresponding to sb example in above paper, which states two concurrent processors performing these two snippets,
mov [x], $1
mov eax, [y]
---
mov [y], $1
mov ebx, [x]should allow eax and ebx on each processor both equal to 0 due to the store buffer on x86 architecture.
Executing cargo test --test sb -- --nocapture produces the following result.
running 1 test
[sb] 34 states explored, 4 terminal states.
test sb ... ok
test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out
Known to compile with Rust stable 1.22.1.