Add breaking changes to the specification traits

CHANGELOG.md

@@ -7,6 +7,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Changed
+- `ConcurrentSpec` trait now has the sequential specification as an associated type and reuses the `Op` and `Ret` types from it.
+- `new()` method in the `SequentialSpec` and `ConcurrentSpec` traits was deleted in favor of the `Default` trait.
+- Bumped `loom` version to 0.6.
+
 ## [0.1.1] - 2023-07-14
 
 ### Added

Cargo.toml

@@ -8,11 +8,17 @@ license = "MIT"
 readme = "README.md"
 repository = "https://github.com/SmnTin/lincheck"
 documentation = "https://docs.rs/lincheck"
-keywords = ["concurrency", "linearizability", "testing", "verification", "lock-free"]
+keywords = [
+    "concurrency",
+    "linearizability",
+    "testing",
+    "verification",
+    "lock-free",
+]
 categories = ["development-tools::testing"]
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-loom = "0.5"
+loom = "0.6"
 proptest = "1.1"

src/checker.rs

@@ -61,7 +61,7 @@ where
             in_degree,
             minimal_invocations,
             linearized: Vec::new(),
-            seq_spec: Seq::new(),
+            seq_spec: Seq::default(),
         };
 
         checker.check_init_part()
@@ -113,7 +113,7 @@ where
     }
 
     fn rebuild_seq_spec(&mut self) {
-        self.seq_spec = Seq::new();
+        self.seq_spec = Seq::default();
 
         for inv in self.execution.init_part.iter() {
             self.seq_spec.exec(inv.op.clone());
@@ -158,14 +158,16 @@ mod tests {
         stack: Vec<T>,
     }
 
+    impl<T> Default for SequentialStack<T> {
+        fn default() -> Self {
+            Self { stack: Vec::new() }
+        }
+    }
+
     impl<T> SequentialSpec for SequentialStack<T> {
         type Op = Op<T>;
         type Ret = Ret<T>;
 
-        fn new() -> Self {
-            Self { stack: Vec::new() }
-        }
-
         fn exec(&mut self, op: Self::Op) -> Self::Ret {
             match op {
                 Op::Push(value) => {

src/lib.rs

@@ -54,69 +54,63 @@
 //!     }
 //! }
 //!
-//! // We then define the concurrent implementation that we want to test:
-//! struct TwoSlotsParallel {
-//!     x: AtomicBool,
-//!     y: AtomicBool,
+//! // We then define the sequential implementation which we test against.
+//! // This type must be default-constructible:
+//! #[derive(Default)]
+//! struct TwoSlotsSequential {
+//!     x: bool,
+//!     y: bool,
 //! }
 //!
-//! // We implement the `ConcurrentSpec` trait for our implementation:
-//! impl ConcurrentSpec for TwoSlotsParallel {
+//! // We implement the `SequentialSpec` trait for our implementation:
+//! impl SequentialSpec for TwoSlotsSequential {
 //!     type Op = Op;
 //!     type Ret = Ret;
 //!
-//!     // We must be able to create a new instance of our implementation:
-//!     fn new() -> Self {
-//!         Self {
-//!             x: AtomicBool::new(false),
-//!             y: AtomicBool::new(false),
-//!         }
-//!     }
-//!
-//!     // We must be able to execute an operation on our implementation:
-//!     fn exec(&self, op: Op) -> Ret {
+//!     fn exec(&mut self, op: Op) -> Ret {
 //!         match op {
 //!             Op::WriteX => {
-//!                 self.x.store(true, Ordering::Relaxed);
+//!                 self.x = true;
 //!                 Ret::Write
 //!             }
 //!             Op::WriteY => {
-//!                 self.y.store(true, Ordering::Relaxed);
+//!                 self.y = true;
 //!                 Ret::Write
 //!             }
-//!             Op::ReadX => Ret::Read(self.x.load(Ordering::Relaxed)),
-//!             Op::ReadY => Ret::Read(self.y.load(Ordering::Relaxed)),
+//!             Op::ReadX => Ret::Read(self.x),
+//!             Op::ReadY => Ret::Read(self.y),
 //!         }
 //!     }
 //! }
 //!
-//! // We then define the sequential implementation which we test against:
-//! struct TwoSlotsSequential {
-//!     x: bool,
-//!     y: bool,
+//! // We then define the concurrent implementation that we want to test.
+//! // This type must be default-constructible too:
+//! #[derive(Default)]
+//! struct TwoSlotsParallel {
+//!     x: AtomicBool,
+//!     y: AtomicBool,
 //! }
 //!
-//! // We implement the `SequentialSpec` trait for our implementation:
-//! impl SequentialSpec for TwoSlotsSequential {
-//!     type Op = Op;
-//!     type Ret = Ret;
-//!
-//!     fn new() -> Self {
-//!         Self { x: false, y: false }
-//!     }
+//! // We implement the `ConcurrentSpec` trait for our implementation:
+//! impl ConcurrentSpec for TwoSlotsParallel {
+//!     // We declare which sequential specification
+//!     // this data structure implements
+//!     type Seq = TwoSlotsSequential;
 //!
-//!     fn exec(&mut self, op: Op) -> Ret {
+//!     // We must be able to execute an operation on our implementation.
+//!     // Note that we reuse `Op` and `Ret` types from the sequential spec.
+//!     fn exec(&self, op: Op) -> Ret {
 //!         match op {
 //!             Op::WriteX => {
-//!                 self.x = true;
+//!                 self.x.store(true, Ordering::Relaxed);
 //!                 Ret::Write
 //!             }
 //!             Op::WriteY => {
-//!                 self.y = true;
+//!                 self.y.store(true, Ordering::Relaxed);
 //!                 Ret::Write
 //!             }
-//!             Op::ReadX => Ret::Read(self.x),
-//!             Op::ReadY => Ret::Read(self.y),
+//!             Op::ReadX => Ret::Read(self.x.load(Ordering::Relaxed)),
+//!             Op::ReadY => Ret::Read(self.y.load(Ordering::Relaxed)),
 //!         }
 //!     }
 //! }
@@ -133,7 +127,7 @@
 //!     Lincheck {
 //!         num_threads: 2,
 //!         num_ops: 5,
-//!     }.verify::<TwoSlotsParallel, TwoSlotsSequential>();
+//!     }.verify::<TwoSlotsParallel>();
 //! }
 //! ```
 //!
@@ -258,37 +252,38 @@ impl Lincheck {
     /// the parallel execution is linearizable to some sequential execution.
     ///
     /// It returns a non-linearizable execution if the test fails.
-    pub fn verify<Conc, Seq>(&self) -> Result<(), Execution<Conc::Op, Conc::Ret>>
+    pub fn verify<Conc>(&self) -> Result<(), Execution<ConcOp<Conc>, ConcRet<Conc>>>
     where
         Conc: ConcurrentSpec + Send + Sync + 'static,
-        Seq: SequentialSpec<Op = Conc::Op, Ret = Conc::Ret> + Send + Sync + 'static,
-        Conc::Op: Send + Sync + Clone + Arbitrary + Debug + UnwindSafe + 'static,
-        Conc::Ret: PartialEq + Debug + Send + Clone,
+        Conc::Seq: Send + Sync + 'static,
+        ConcOp<Conc>: Send + Sync + Clone + Arbitrary + Debug + UnwindSafe + 'static,
+        ConcRet<Conc>: PartialEq + Debug + Send + Clone,
     {
-        let result = TestRunner::default().run(&any::<Scenario<Conc::Op>>(), |scenario| {
-            check_scenario_with_loom::<Conc, Seq>(scenario)
+        let result = TestRunner::default().run(&any::<Scenario<ConcOp<Conc>>>(), |scenario| {
+            check_scenario_with_loom::<Conc>(scenario)
                 .map_err(|_| TestCaseError::Fail("Non-linearizable execution".into()))
         });
 
         match result {
             Ok(_) => Ok(()),
             Err(TestError::Fail(_, scenario)) => {
                 // rerun the scenario to get the failing execution
-                Err(check_scenario_with_loom::<Conc, Seq>(scenario).unwrap_err())
+                Err(check_scenario_with_loom::<Conc>(scenario).unwrap_err())
             }
             Err(failure) => panic!("Unexpected failure: {:?}", failure),
         }
     }
 
     /// The same as [verify](Lincheck::verify) but automatically panics and pretty-prints the execution if the test fails.
-    pub fn verify_or_panic<Conc, Seq>(&self)
+    pub fn verify_or_panic<Conc>(&self)
     where
         Conc: ConcurrentSpec + Send + Sync + 'static,
-        Seq: SequentialSpec<Op = Conc::Op, Ret = Conc::Ret> + Send + Sync + 'static,
-        Conc::Op: Send + Sync + UnwindSafe + Clone + Arbitrary + Debug + 'static,
-        Conc::Ret: PartialEq + Debug + Send + Clone,
+        Conc::Seq: Send + Sync + 'static,
+        <Conc::Seq as SequentialSpec>::Op:
+            Send + Sync + UnwindSafe + Clone + Arbitrary + Debug + 'static,
+        <Conc::Seq as SequentialSpec>::Ret: PartialEq + Debug + Send + Clone,
     {
-        let result = self.verify::<Conc, Seq>();
+        let result = self.verify::<Conc>();
         if let Err(execution) = result {
             panic!("Non-linearizable execution: \n\n {}", execution);
         }

src/scenario.rs

@@ -29,14 +29,14 @@ pub struct Scenario<Op> {
 ///
 /// It works by panicking inside using the failing execution as the message and catching the panic outside.
 /// This is the only way to return a value from loom model-checker.
-pub fn check_scenario_with_loom<Conc, Seq>(
-    scenario: Scenario<Conc::Op>,
-) -> Result<(), Execution<Conc::Op, Conc::Ret>>
+pub fn check_scenario_with_loom<Conc>(
+    scenario: Scenario<ConcOp<Conc>>,
+) -> Result<(), Execution<ConcOp<Conc>, ConcRet<Conc>>>
 where
     Conc: ConcurrentSpec + Send + Sync + 'static,
-    Seq: SequentialSpec<Op = Conc::Op, Ret = Conc::Ret> + Send + Sync + 'static,
-    Conc::Op: Send + Sync + Clone + Debug + UnwindSafe + 'static,
-    Conc::Ret: PartialEq + Clone + Debug + Send,
+    Conc::Seq: Send + Sync + 'static,
+    ConcOp<Conc>: Send + Sync + Clone + Debug + UnwindSafe + 'static,
+    ConcRet<Conc>: PartialEq + Clone + Debug + Send,
 {
     // temporarily disable the panic hook to avoid printing the panic message
     let old_hook = panic::take_hook();
@@ -46,7 +46,7 @@ where
     let result = panic::catch_unwind(|| {
         loom::model(move || {
             let execution = execute_scenario_with_loom::<Conc>(scenario.clone());
-            if !LinearizabilityChecker::<Seq>::check(&execution) {
+            if !LinearizabilityChecker::<Conc::Seq>::check(&execution) {
                 // panic with the failing execution as the payload
                 panic::panic_any(execution);
             }
@@ -59,21 +59,21 @@ where
     result.map_err(|payload| {
         // recover the failing execution from the panic payload
         *payload
-            .downcast::<Execution<Conc::Op, Conc::Ret>>()
+            .downcast::<Execution<ConcOp<Conc>, ConcRet<Conc>>>()
             .unwrap_or_else(|_| panic!("loom::model panicked with unknown payload"))
     })
 }
 
 /// Executes the given scenario with [loom] mock threads and returns the resulting execution.
 pub fn execute_scenario_with_loom<Conc>(
-    scenario: Scenario<Conc::Op>,
-) -> Execution<Conc::Op, Conc::Ret>
+    scenario: Scenario<ConcOp<Conc>>,
+) -> Execution<ConcOp<Conc>, ConcRet<Conc>>
 where
     Conc: ConcurrentSpec + Send + Sync + 'static,
-    Conc::Op: Send + Sync + Clone + 'static,
-    Conc::Ret: PartialEq,
+    ConcOp<Conc>: Send + Sync + Clone + 'static,
+    ConcRet<Conc>: PartialEq,
 {
-    let conc = Rc::new(Conc::new());
+    let conc = Rc::new(Conc::default());
 
     let mut recorder = recorder::record_init_part_with_capacity(scenario.init_part.len());
 

src/spec.rs

@@ -1,29 +1,26 @@
 /// The sequential implementation of a data structure.
-pub trait SequentialSpec {
+pub trait SequentialSpec: Default {
     /// The type of operations.
     type Op;
 
     /// The type of return values.
     type Ret;
 
-    /// Creates a new instance of the data structure.
-    fn new() -> Self;
-
     /// Executes an operation on the data structure.
     fn exec(&mut self, op: Self::Op) -> Self::Ret;
 }
 
 /// The concurrent implementation of a data structure.
-pub trait ConcurrentSpec {
-    /// The type of operations.
-    type Op;
-
-    /// The type of return values.
-    type Ret;
-
-    /// Creates a new instance of the data structure.
-    fn new() -> Self;
+pub trait ConcurrentSpec: Default {
+    /// The sequential specification for the data structure.
+    type Seq: SequentialSpec;
 
     /// Executes an operation on the data structure.
-    fn exec(&self, op: Self::Op) -> Self::Ret;
+    fn exec(&self, op: ConcOp<Self>) -> ConcRet<Self>;
 }
+
+/// Type alias not to have always write down FQP.
+pub type ConcOp<T> = <<T as ConcurrentSpec>::Seq as SequentialSpec>::Op;
+
+/// Type alias not to have always write down FQP.
+pub type ConcRet<T> = <<T as ConcurrentSpec>::Seq as SequentialSpec>::Ret;