concurrency

concurrency/src/lib.rs

@@ -38,13 +38,6 @@
 //!   schedule that `parking_lot` permits. Tests that hinge on that
 //!   interleaving need `RwLock<T>` with explicit `read()` then
 //!   `write()`, or a richer state machine in the facade.
-//! * **`static FOO: Mutex<T> = Mutex::new(...)` does not compile
-//!   under loom.** `loom::sync::Mutex::new` is plain `fn`, not
-//!   `const fn`, so a static initialiser fails to typecheck. Use
-//!   `OnceLock` for the static (the facade re-exports
-//!   `std::sync::OnceLock` under all backends) or move the
-//!   construction into a runtime initialiser gated by
-//!   `#[concurrency_mode(std)]`.
 //! * **`OnceLock` under loom/shuttle** is the real `std::sync::OnceLock`,
 //!   not a model-aware shim. Loom and shuttle do not see the
 //!   atomics inside `OnceLock::get_or_init`, so tests whose

concurrency/src/sync/mod.rs

@@ -36,8 +36,6 @@
 //!   `const fn`, but the facade exposes the lowest common
 //!   denominator. So `static M: Mutex<T> = Mutex::new(...)` compiles
 //!   under the default and `parking_lot` backends and fails to
-//!   typecheck under the model-checker backends. Workaround for
-//!   tests that need a static: wrap the static in `OnceLock`.
 //!
 //! * **`OnceLock` under `loom`/`shuttle*` is re-exported from
 //!   `std::sync` unchanged.** It is sound for laziness, but it uses

config/src/external/overlay/algebra.rs

@@ -291,6 +291,16 @@ impl Footprint {
     pub fn is_empty(&self) -> bool {
         self.vpcs.is_empty() && self.peerings.is_empty()
     }
+
+    #[must_use]
+    pub fn touches_vpc_named(&self, name: &str) -> bool {
+        self.vpcs.iter().any(|vpc| vpc.name() == name)
+    }
+
+    #[must_use]
+    pub fn touches_peering_named(&self, name: &str) -> bool {
+        self.peerings.iter().any(|peering| peering.name() == name)
+    }
 }
 
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
@@ -970,6 +980,36 @@ mod tests {
     use bolero::check;
     use concurrency::sync::atomic::{AtomicUsize, Ordering::Relaxed};
 
+    #[test]
+    fn writing_a_vpc_does_not_imply_writing_its_peerings() {
+        static SEEN: AtomicUsize = AtomicUsize::new(0);
+
+        check!()
+            .with_generator(Sequence::default())
+            .for_each(|ops: &Vec<Op>| {
+                let mut draft = Draft::new();
+                for op in ops {
+                    let footprint = op.writes(&draft);
+                    for vpc in &footprint.vpcs {
+                        for (handle, spec) in draft.peerings() {
+                            if spec.touches(*vpc) && !footprint.peerings.contains(&handle) {
+                                SEEN.fetch_add(1, Relaxed);
+                            }
+                        }
+                    }
+                    op.apply(&mut draft).expect("a drawn operation applies");
+                }
+            });
+
+        assert!(
+            SEEN.load(Relaxed) > 0,
+            "no drawn operation ever wrote a vpc while leaving one of its peerings unwritten. \
+             Either the vocabulary changed and a peering-only frame filter is now sound -- in \
+             which case say so where the filter is written -- or the generator stopped drawing \
+             `AddPeering` against a vpc that already had one"
+        );
+    }
+
     static DRAWN: [AtomicUsize; 7] = [
         AtomicUsize::new(0),
         AtomicUsize::new(0),