Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
0 parents
commit 2b37a35
Showing
42 changed files
with
3,850 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
target | ||
Cargo.lock |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
--- | ||
language: rust | ||
rust: | ||
- stable | ||
- nightly | ||
|
||
script: | ||
# Run tests with thread based runtime | ||
- cargo test | ||
|
||
# Run tests with generator based runtime | ||
- cargo test --tests --features generator | ||
|
||
# Run tests with fringe based runtime | ||
- | | ||
if [ "${TRAVIS_RUST_VERSION}" = "nightly" ]; | ||
then cargo test --tests --features fringe; | ||
fi | ||
# Check with serde based checkpoint feature | ||
- cargo check --features checkpoint | ||
|
||
notifications: | ||
email: | ||
on_success: never |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
# 0.1.0 (unreleased) | ||
|
||
* Initial release |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,45 @@ | ||
[package] | ||
name = "loom" | ||
# When releasing to crates.io: | ||
# - Update version number | ||
# - lib.rs: html_root_url. | ||
# - README.md | ||
# - Update CHANGELOG.md | ||
# - Update doc URL. | ||
# - Cargo.toml | ||
# - README.md | ||
# - Create git tag | ||
version = "0.1.0" | ||
license = "MIT" | ||
authors = ["Carl Lerche <me@carllerche.com>"] | ||
description = "Model checker for concurrent code" | ||
documentation = "https://docs.rs/loom/0.1.0/loom" | ||
homepage = "https://github.com/carllerche/loom" | ||
repository = "https://github.com/carllerche/loom" | ||
readme = "README.md" | ||
keywords = ["atomic", "lock-free"] | ||
categories = ["concurrency", "data-structures"] | ||
|
||
[features] | ||
default = [] | ||
checkpoint = ["serde", "serde_derive", "serde_json"] | ||
|
||
[dependencies] | ||
cfg-if = "0.1.6" | ||
libc = "0.2.44" | ||
scoped-tls = "0.1.2" | ||
scoped-mut-tls = { version = "0.1.0", git = "http://github.com/carllerche/scoped-mut-tls" } | ||
|
||
# Provides a generator based runtime | ||
generator = { version = "0.6.10", optional = true } | ||
|
||
# Provides a runtime based on libfringe. Requires nightly. | ||
fringe = { git = "https://github.com/carllerche/libfringe", branch = "track-nightly", optional = true } | ||
|
||
# Optional futures support | ||
futures = { version = "", optional = true } | ||
|
||
# Requires for "checkpoint" feature | ||
serde = { version = "1.0.80", optional = true } | ||
serde_derive = { version = "1.0.80", optional = true } | ||
serde_json = { version = "1.0.33", optional = true } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
Copyright (c) 2018 Carl Lerche | ||
|
||
Permission is hereby granted, free of charge, to any | ||
person obtaining a copy of this software and associated | ||
documentation files (the "Software"), to deal in the | ||
Software without restriction, including without | ||
limitation the rights to use, copy, modify, merge, | ||
publish, distribute, sublicense, and/or sell copies of | ||
the Software, and to permit persons to whom the Software | ||
is furnished to do so, subject to the following | ||
conditions: | ||
|
||
The above copyright notice and this permission notice | ||
shall be included in all copies or substantial portions | ||
of the Software. | ||
|
||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF | ||
ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED | ||
TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A | ||
PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT | ||
SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY | ||
CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION | ||
OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR | ||
IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER | ||
DEALINGS IN THE SOFTWARE. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
# Loom | ||
|
||
Loom is a model checker for concurrent Rust code. It exhaustively explores the | ||
behaviors of code under the C11 memory model, which Rust inherits. | ||
|
||
## Getting started | ||
|
||
To use `loom`, first add this to your `Cargo.toml`: | ||
|
||
```toml | ||
[dev-dependencies] | ||
loom = "0.1.0" | ||
``` | ||
|
||
Next, create a test file. | ||
|
||
## Implementation | ||
|
||
Loom is an implementation of techniques described in [CDSChecker: Checking | ||
Concurrent Data Structures Written with C/C++ Atomics][cdschecker]. | ||
|
||
[cdschecker]: http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf | ||
|
||
## License | ||
|
||
This project is licensed under the [MIT license](LICENSE). | ||
|
||
### Contribution | ||
|
||
Unless you explicitly state otherwise, any contribution intentionally submitted | ||
for inclusion in `loom` by you, shall be licensed as MIT, without any additional | ||
terms or conditions. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,35 @@ | ||
use super::task; | ||
use std::cell::RefCell; | ||
|
||
#[derive(Debug)] | ||
pub struct AtomicTask { | ||
task: RefCell<Option<task::Task>>, | ||
} | ||
|
||
impl AtomicTask { | ||
pub fn new() -> AtomicTask { | ||
AtomicTask { | ||
task: RefCell::new(None), | ||
} | ||
} | ||
|
||
pub fn register(&self) { | ||
self.register_task(task::current()); | ||
} | ||
|
||
pub fn register_task(&self, task: task::Task) { | ||
*self.task.borrow_mut() = Some(task); | ||
} | ||
|
||
pub fn notify(&self) { | ||
if let Some(task) = self.task.borrow_mut().take() { | ||
task.notify(); | ||
} | ||
} | ||
} | ||
|
||
impl Default for AtomicTask { | ||
fn default() -> Self { | ||
AtomicTask::new() | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
mod atomic_task; | ||
|
||
pub use self::atomic_task::AtomicTask; | ||
|
||
use rt; | ||
use _futures::Future; | ||
|
||
pub fn spawn<F>(f: F) | ||
where | ||
F: Future<Item = (), Error = ()> + 'static, | ||
{ | ||
rt::spawn(move || rt::wait_future(f)); | ||
} | ||
|
||
pub mod task { | ||
use rt; | ||
|
||
#[derive(Debug)] | ||
pub struct Task { | ||
thread: rt::thread::Id, | ||
} | ||
|
||
pub fn current() -> Task { | ||
Task { | ||
thread: rt::thread::Id::current(), | ||
} | ||
} | ||
|
||
impl Task { | ||
pub fn notify(&self) { | ||
self.thread.future_notify(); | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,185 @@ | ||
use rt::{self, Execution, Scheduler}; | ||
|
||
use std::path::PathBuf; | ||
use std::sync::Arc; | ||
|
||
const DEFAULT_MAX_THREADS: usize = 4; | ||
|
||
const DEFAULT_MAX_MEMORY: usize = 4096 << 14; | ||
|
||
#[derive(Debug)] | ||
pub struct Builder { | ||
/// Max number of threads to check as part of the execution. This should be set as low as possible. | ||
pub max_threads: usize, | ||
|
||
/// Maximum amount of memory that can be consumed by the associated metadata. | ||
pub max_memory: usize, | ||
|
||
/// When doing an exhaustive fuzz, uses the file to store and load the fuzz | ||
/// progress | ||
pub checkpoint_file: Option<PathBuf>, | ||
|
||
/// How often to write the checkpoint file | ||
pub checkpoint_interval: usize, | ||
|
||
/// What runtime to use | ||
pub runtime: Runtime, | ||
|
||
/// Log execution output to stdout. | ||
pub log: bool, | ||
} | ||
|
||
#[derive(Debug)] | ||
pub enum Runtime { | ||
Thread, | ||
|
||
#[cfg(feature = "generator")] | ||
Generator, | ||
|
||
#[cfg(feature = "fringe")] | ||
Fringe, | ||
} | ||
|
||
impl Builder { | ||
pub fn new() -> Builder { | ||
Builder { | ||
max_threads: DEFAULT_MAX_THREADS, | ||
max_memory: DEFAULT_MAX_MEMORY, | ||
checkpoint_file: None, | ||
checkpoint_interval: 100_000, | ||
|
||
#[cfg(feature = "fringe")] | ||
runtime: Runtime::Fringe, | ||
|
||
#[cfg(all(feature = "generator", not(feature = "fringe")))] | ||
runtime: Runtime::Generator, | ||
|
||
#[cfg(all(not(feature = "generator"), not(feature = "fringe")))] | ||
runtime: Runtime::Thread, | ||
|
||
log: false, | ||
} | ||
} | ||
|
||
pub fn checkpoint_file(&mut self, file: &str) -> &mut Self { | ||
self.checkpoint_file = Some(file.into()); | ||
self | ||
} | ||
|
||
pub fn fuzz<F>(&self, f: F) | ||
where | ||
F: Fn() + Sync + Send + 'static, | ||
{ | ||
let mut execution = Execution::new(self.max_threads, self.max_memory); | ||
let mut scheduler = match self.runtime { | ||
Runtime::Thread => Scheduler::new_thread(self.max_threads), | ||
|
||
#[cfg(feature = "generator")] | ||
Runtime::Generator => Scheduler::new_generator(self.max_threads), | ||
|
||
#[cfg(feature = "fringe")] | ||
Runtime::Fringe => Scheduler::new_fringe(self.max_threads), | ||
}; | ||
|
||
if let Some(ref path) = self.checkpoint_file { | ||
if path.exists() { | ||
execution.path = checkpoint::load_execution_path(path); | ||
} | ||
} | ||
|
||
execution.log = self.log; | ||
|
||
let f = Arc::new(f); | ||
|
||
let mut i = 0; | ||
|
||
loop { | ||
i += 1; | ||
|
||
if i % self.checkpoint_interval == 0 { | ||
println!(" ===== iteration {} =====", i); | ||
|
||
if let Some(ref path) = self.checkpoint_file { | ||
checkpoint::store_execution_path(&execution.path, path); | ||
} | ||
} | ||
|
||
let f = f.clone(); | ||
|
||
scheduler.run(&mut execution, move || { | ||
f(); | ||
rt::thread_done(); | ||
}); | ||
|
||
if let Some(next) = execution.step() { | ||
execution = next; | ||
} else { | ||
return; | ||
} | ||
} | ||
} | ||
} | ||
|
||
pub fn fuzz<F>(f: F) | ||
where | ||
F: Fn() + Sync + Send + 'static, | ||
{ | ||
Builder::new().fuzz(f) | ||
} | ||
|
||
if_futures! { | ||
use _futures::Future; | ||
|
||
impl Builder { | ||
pub fn fuzz_future<F, R>(&self, f: F) | ||
where | ||
F: Fn() -> R + Sync + Send + 'static, | ||
R: Future<Item = (), Error = ()>, | ||
{ | ||
self.fuzz(move || rt::wait_future(f())); | ||
} | ||
} | ||
|
||
pub fn fuzz_future<F, R>(f: F) | ||
where | ||
F: Fn() -> R + Sync + Send + 'static, | ||
R: Future<Item = (), Error = ()>, | ||
{ | ||
Builder::new().fuzz_future(f); | ||
} | ||
} | ||
|
||
#[cfg(feature = "checkpoint")] | ||
mod checkpoint { | ||
use serde_json; | ||
use std::fs::File; | ||
use std::io::prelude::*; | ||
use std::path::Path; | ||
|
||
pub(crate) fn load_execution_path(fs_path: &Path) -> ::rt::Path { | ||
let mut file = File::open(fs_path).unwrap(); | ||
let mut contents = String::new(); | ||
file.read_to_string(&mut contents).unwrap(); | ||
serde_json::from_str(&contents).unwrap() | ||
} | ||
|
||
pub(crate) fn store_execution_path(path: &::rt::Path, fs_path: &Path) { | ||
let serialized = serde_json::to_string(path).unwrap(); | ||
|
||
let mut file = File::create(fs_path).unwrap(); | ||
file.write_all(serialized.as_bytes()).unwrap(); | ||
} | ||
} | ||
|
||
#[cfg(not(feature = "checkpoint"))] | ||
mod checkpoint { | ||
use std::path::Path; | ||
|
||
pub(crate) fn load_execution_path(_fs_path: &Path) -> ::rt::Path { | ||
panic!("not compiled with `checkpoint` feature") | ||
} | ||
|
||
pub(crate) fn store_execution_path(_path: &::rt::Path, _fs_path: &Path) { | ||
panic!("not compiled with `checkpoint` feature") | ||
} | ||
} |
Oops, something went wrong.