# Fenic

Testing for concurrent code.

## Quickstart

Add this to your `Cargo.toml`:

```toml
[target.'cfg(fenic)'.dependencies]
fenic = "0.7"
```

Next, create a test file and add a test:

```rust
use fenic::sync::Arc;
use fenic::sync::atomic::AtomicUsize;
use fenic::sync::atomic::Ordering::{Acquire, Release, Relaxed};
use fenic::thread;

#[test]
#[should_panic]
fn buggy_concurrent_inc() {
    fenic::model(|| {
        let num = Arc::new(AtomicUsize::new(0));

        let ths: Vec<_> = (0..2)
            .map(|_| {
                let num = num.clone();
                thread::spawn(move || {
                    let curr = num.load(Acquire);
                    num.store(curr + 1, Release);
                })
            })
            .collect();

        for th in ths {
            th.join().unwrap();
        }

        assert_eq!(2, num.load(Relaxed));
    });
}
```

Then, run the test with

```console
RUSTFLAGS="--cfg fenic" cargo test --test buggy_concurrent_inc --release
```

## Unsupported features
Loom currently does not implement the full C11 memory model.
Here is the (incomplete) list of unsupported features.
* `SeqCst` accesses (e.g. `load`, `store`, ..):
  They are are regarded as `AcqRel`. That is, they impose weaker
  synchronization, causing Loom to generate false alarms (not complete). See
  [#180](https://github.com/tokio-rs/fenic/issues/180) for example. On the other
  hand, `fence(SeqCst)` is supported.
* Load buffering behavior:
  Loom does not explore some executions that are possible in the C11 memory
  model. That is, there can be a bug in the checked code even if Loom says
  there is no bug (not sound).  See the `load_buffering` test case in
  `tests/litmus.rs`.

## License

This project is licensed under the [MIT license](LICENSE).

### Contribution

Unless you explicitly state otherwise, any contribution intentionally
submitted for inclusion in `fenic` by you, shall be licensed as MIT,
without any additional terms or conditions.