Added a graph based symmetry variant

crates/aterm/src/random_term.rs

@@ -1,18 +1,18 @@
 #![forbid(unsafe_code)]
 
 #[cfg(test)]
-mod inner {
-    pub use rand::Rng;
-    pub use rustc_hash::FxHashSet;
-
-    pub use crate::ATerm;
-    pub use crate::Symbol;
-    pub use crate::Term;
-    pub use crate::storage::THREAD_TERM_POOL;
-}
+use rand::Rng;
+#[cfg(test)]
+use rustc_hash::FxHashSet;
 
 #[cfg(test)]
-use inner::*;
+use crate::ATerm;
+#[cfg(test)]
+use crate::Symbol;
+#[cfg(test)]
+use crate::Term;
+#[cfg(test)]
+use crate::storage::THREAD_TERM_POOL;
 
 /// Create a random term consisting of the given symbol and constants. Performs
 /// iterations number of constructions, and uses chance_duplicates to choose the

crates/aterm/src/storage/global_aterm_pool.rs

@@ -37,6 +37,10 @@ pub(crate) static GLOBAL_TERM_POOL: LazyLock<GlobalBfSharedMutex<GlobalTermPool>
 /// Enables aggressive garbage collection, which is used for testing.
 pub(crate) const AGGRESSIVE_GC: bool = false;
 
+/// The number of terms a thread pool reserves from the shared budget at a time, see
+/// [crate::storage::ThreadTermPool].
+pub(crate) const GC_BUDGET_CHUNK: usize = 4096;
+
 /// A type alias for the global term pool guard
 pub(crate) type GlobalTermPoolGuard<'a> = RecursiveLockReadGuard<'a, GlobalTermPool>;
 
@@ -73,7 +77,7 @@ pub(crate) struct GlobalTermPool {
 
     /// The number of terms that may still be created before garbage collection should be
     /// triggered. Set to roughly `capacity - len` after each collection and consumed by the
-    /// thread pools in chunks (see [crate::storage::ThreadTermPool]) to avoid contention.
+    /// thread pools in [GC_BUDGET_CHUNK] sized chunks to avoid contention on this counter.
     gc_budget: AtomicUsize,
 
     /// Default terms
@@ -269,30 +273,25 @@ impl GlobalTermPool {
         }
     }
 
-    /// Triggers garbage collection if necessary, refreshes the global budget and returns the
-    /// per-thread chunk the calling thread pool should count down before touching the budget
-    /// again.
-    pub(crate) fn trigger_garbage_collection(&mut self) -> usize {
+    /// Triggers garbage collection if necessary and refreshes the global budget.
+    pub(crate) fn trigger_garbage_collection(&mut self) {
         if self.garbage_collection {
             // Garbage collection is enabled.
             self.collect_garbage();
         }
 
-        self.reset_gc_budget()
+        self.reset_gc_budget();
     }
 
-    /// Recomputes the global GC budget from the free storage capacity and returns the per-thread
-    /// chunk (the budget divided over the registered thread pools, to avoid every thread
-    /// contending on the shared counter).
-    pub(crate) fn reset_gc_budget(&self) -> usize {
+    /// Recomputes the global GC budget from the free storage capacity.
+    pub(crate) fn reset_gc_budget(&self) {
         let budget = if AGGRESSIVE_GC {
             1
         } else {
             self.terms.capacity().saturating_sub(self.len()).max(1)
         };
 
         self.gc_budget.store(budget, Ordering::Relaxed);
-        (budget / self.num_thread_pools()).max(1)
     }
 
     /// Subtracts `amount` from the global GC budget, saturating at zero so it never wraps, and
@@ -306,17 +305,6 @@ impl GlobalTermPool {
             .expect("the update closure always returns Some")
     }
 
-    /// Returns the current per-thread budget chunk without recomputing the global budget. Used
-    /// by a newly registered thread pool to obtain its initial counter.
-    pub(crate) fn gc_budget_chunk(&self) -> usize {
-        (self.gc_budget.load(Ordering::Relaxed) / self.num_thread_pools()).max(1)
-    }
-
-    /// Returns the number of registered (live) thread pools, at least one.
-    fn num_thread_pools(&self) -> usize {
-        self.thread_pools.iter().flatten().count().max(1)
-    }
-
     /// Enables or disables automatic garbage collection.
     pub fn automatic_garbage_collection(&mut self, enabled: bool) {
         self.garbage_collection = enabled;

crates/aterm/src/storage/thread_aterm_pool.rs

@@ -35,6 +35,7 @@ use crate::storage::GlobalTermPoolGuard;
 use crate::storage::MAX_FIXED_ARITY;
 use crate::storage::SharedTerm;
 use crate::storage::SharedTermProtection;
+use crate::storage::global_aterm_pool::GC_BUDGET_CHUNK;
 use crate::storage::global_aterm_pool::GLOBAL_TERM_POOL;
 
 thread_local! {
@@ -56,14 +57,11 @@ pub struct ThreadTermPool {
     send_term_protection_set: Arc<Mutex<ProtectionSet<ATermIndex>>>,
 
     /// Counts down the number of terms this thread may still create before it must consume the
-    /// next chunk from the global budget (see [GlobalTermPool::reset_gc_budget]).
+    /// next [GC_BUDGET_CHUNK] from the global budget (see [GlobalTermPool::reset_gc_budget]).
+    ///
+    /// Zero means this thread holds no reservation, so the next term creation has to claim one.
     garbage_collection_counter: Cell<usize>,
 
-    /// The size of a single budget chunk: the amount subtracted from the global budget, and the
-    /// value [Self::garbage_collection_counter] is refilled to, each time the counter reaches
-    /// zero.
-    garbage_collection_chunk: Cell<usize>,
-
     /// A vector of terms that are used to store the arguments of a term for lookup.
     tmp_arguments: RefCell<Vec<ATermRef<'static>>>,
 
@@ -89,15 +87,13 @@ impl ThreadTermPool {
         let empty_list_symbol = pool.get_empty_list_symbol().copy();
         let list_symbol = pool.get_list_symbol().copy();
 
-        // Claim a share of the current global budget as this thread's initial chunk.
-        let chunk = pool.gc_budget_chunk();
         drop(pool);
 
         Self {
             protection_sets,
             send_term_protection_set,
-            garbage_collection_counter: Cell::new(chunk),
-            garbage_collection_chunk: Cell::new(chunk),
+            // Start without a reservation so the first created term claims (and charges) one.
+            garbage_collection_counter: Cell::new(0),
             tmp_arguments: RefCell::new(Vec::new()),
             int_symbol,
             empty_list_symbol,
@@ -465,28 +461,26 @@ impl ThreadTermPool {
         guard.automatic_garbage_collection(enabled);
     }
 
-    /// Forces a garbage collection to occur, regardless of the current counter value or whether it is enabled.
+    /// Forces a garbage collection to occur regardless of the current GC budget.
     pub fn force_collect_garbage(&self) {
         let mut guard = self.term_pool.write().expect("Lock poisoned!");
         guard.collect_garbage();
-        self.set_budget_chunk(guard.reset_gc_budget());
+        guard.reset_gc_budget();
+        self.drop_budget_reservation();
     }
 
-    /// Perform a garbage collection.
+    /// Perform a garbage collection if the global aterm pool is not locked.
     pub fn collect_garbage(&self) {
-        if !self.term_pool.is_locked() {
-            // Trigger garbage collection and acquire a fresh budget chunk.
-            if let Some(mut guard) = self.term_pool.try_write().expect("Lock poisoned!") {
-                self.set_budget_chunk(guard.trigger_garbage_collection());
-            }
+        if let Some(mut guard) = self.term_pool.try_write().expect("Lock poisoned!") {
+            guard.trigger_garbage_collection();
+            self.drop_budget_reservation();
         }
     }
 
-    /// Records the per-thread budget chunk returned by the global pool, resetting the local
-    /// counter to count it down.
-    fn set_budget_chunk(&self, chunk: usize) {
-        self.garbage_collection_chunk.set(chunk);
-        self.garbage_collection_counter.set(chunk);
+    /// Drops this thread's outstanding reservation after the global budget was refreshed, so that
+    /// the next created term claims a chunk from (and charges it to) the new budget.
+    fn drop_budget_reservation(&self) {
+        self.garbage_collection_counter.set(0);
     }
 
     /// Triggers delayed garbage collection if the counter has reached zero.
@@ -519,27 +513,24 @@ impl ThreadTermPool {
         self.trigger_garbage_collection();
     }
 
-    /// Consumes the next budget chunk once the local counter is exhausted, triggering garbage
+    /// Reserves the next budget chunk once the local counter is exhausted, triggering garbage
     /// collection when the shared global budget has run out.
     fn trigger_garbage_collection(&self) {
         if self.garbage_collection_counter.get() == 0 && !self.term_pool.is_locked() {
-            let chunk = self.garbage_collection_chunk.get();
-
-            // Subtract this thread's chunk from the shared budget. The read guard is only needed
-            // to reach the atomic and is dropped before a potential collection acquires the write
-            // lock.
+            // Subtract a chunk from the shared budget. The read guard is only needed to reach the
+            // atomic and is dropped before a potential collection acquires the write lock.
             let previous = self
                 .term_pool
                 .read_recursive()
                 .expect("Lock poisoned!")
-                .consume_gc_budget(chunk);
+                .consume_gc_budget(GC_BUDGET_CHUNK);
 
-            if previous <= chunk {
-                // The global budget is exhausted, so collect and obtain a fresh chunk.
+            if previous <= GC_BUDGET_CHUNK {
+                // The global budget is exhausted, so collect and start over on a fresh budget.
                 self.collect_garbage();
             } else {
-                // Budget remains; refill the local counter to count down the next chunk.
-                self.garbage_collection_counter.set(chunk);
+                // The chunk is now charged to the budget, so count it down locally.
+                self.garbage_collection_counter.set(GC_BUDGET_CHUNK);
             }
         }
     }
@@ -652,7 +643,6 @@ impl DerefMut for ProtectionSetGuard<'_> {
 
 #[cfg(test)]
 mod tests {
-    use std::mem::ManuallyDrop;
     use std::sync::mpsc;
 
     use crate::ATerm;
@@ -748,7 +738,7 @@ mod tests {
 
             // Leak the term so it is still protected at thread teardown, exercising the orphan
             // adoption path. The bug we guard against is post-teardown read UB.
-            std::mem::forget(ManuallyDrop::new(term));
+            std::mem::forget(term);
         });
 
         handle.join().expect("Thread should join without panic");

crates/data/src/closed.rs

@@ -0,0 +1,66 @@
+use std::ops::ControlFlow;
+
+use ahash::AHashSet;
+use merc_aterm::Term;
+use merc_utilities::Step;
+
+use crate::DataExpressionRef;
+use crate::is_data_variable;
+use crate::visit_data_expr;
+
+/// Returns true iff `term` contains no data variables, i.e. it is a ground term.
+///
+/// A closed term normalises to the same result under every substitution, which is what makes
+/// it sound to cache its normal form across calls that pass different substitutions.
+///
+/// Panics for binders and where clauses, which have no flat argument list.
+pub fn is_closed<'a, 'b, T: Term<'a, 'b>>(term: &'b T) -> bool {
+    // Terms are maximally shared, so the same subterm is typically reachable along many paths.
+    // Remembering the ones already seen keeps this linear in the size of the term graph rather
+    // than the size of the tree it unfolds to. Keying on the term address is only valid because
+    // no terms are created here, so no garbage collection can run during the traversal.
+    let mut visited = AHashSet::new();
+
+    let variable: Option<()> = visit_data_expr(&DataExpressionRef::from(term.copy()), (), |expr, context| {
+        if !visited.insert(expr.index()) {
+            ControlFlow::Continue(Step::Prune)
+        } else if is_data_variable(expr) {
+            ControlFlow::Break(())
+        } else {
+            // A function symbol and a machine number have no children, and the head function
+            // symbol of an application is closed by definition, so neither needs to be recognised
+            // separately here.
+            ControlFlow::Continue(Step::Into(context))
+        }
+    });
+
+    variable.is_none()
+}
+
+#[cfg(test)]
+mod tests {
+    use ahash::AHashSet;
+
+    use crate::DataExpression;
+    use crate::is_closed;
+
+    #[test]
+    fn test_is_closed_ground_term() {
+        let term = DataExpression::from_string("s(s(a), b)").unwrap();
+        assert!(is_closed(&term));
+    }
+
+    #[test]
+    fn test_is_closed_with_variable() {
+        let variables = AHashSet::from_iter(["x".to_string()]);
+        let term = DataExpression::from_string_untyped("s(s(x), b)", &variables).unwrap();
+        assert!(!is_closed(&term));
+    }
+
+    #[test]
+    fn test_is_closed_bare_variable() {
+        let variables = AHashSet::from_iter(["x".to_string()]);
+        let term = DataExpression::from_string_untyped("x", &variables).unwrap();
+        assert!(!is_closed(&term));
+    }
+}

crates/data/src/data_expression.rs

@@ -38,9 +38,7 @@ use crate::is_data_variable;
 use crate::is_data_where_clause;
 use crate::is_data_whr_decl;
 
-/// The kind of a binder in a `DataAbstraction` — mirrors mCRL2's
-/// `data::binder_type` enum (the 0-arity marker term that is the first child
-/// of every `Binder(type, vars, body)` aterm).
+/// The kind of a binder in a `DataAbstraction`.
 #[derive(Clone, Copy, Debug, Eq, PartialEq)]
 pub enum BinderType {
     Lambda,
@@ -99,6 +97,24 @@ mod inner {
             }
         }
 
+        /// Same as [DataExpression::data_function_symbol], but returns `None` for a variable
+        /// instead of panicking.
+        ///
+        /// Pattern matching uses this to observe a symbol: a variable in the subject term has no
+        /// head symbol and therefore matches no pattern position. The variable is only tested
+        /// after the two cases that do have one, so the common path costs the same.
+        pub fn try_data_function_symbol(&self) -> Option<DataFunctionSymbolRef<'_>> {
+            if is_data_application(&self.term) {
+                Some(self.term.arg(0).into())
+            } else if is_data_function_symbol(&self.term) {
+                Some(self.term.copy().into())
+            } else if is_data_variable(&self.term) {
+                None
+            } else {
+                panic!("try_data_function_symbol not implemented for {self}");
+            }
+        }
+
         /// Returns the data sub-expressions of a data expression.
         ///     - function symbol                  f -> []
         ///     - variable                         x -> []
@@ -622,7 +638,20 @@ mod inner {
     }
 }
 
-pub use inner::*;
+pub use inner::DataAbstraction;
+pub use inner::DataApplication;
+pub use inner::DataApplicationRef;
+pub use inner::DataEquation;
+pub use inner::DataExpression;
+pub use inner::DataExpressionRef;
+pub use inner::DataFunctionSymbol;
+pub use inner::DataFunctionSymbolRef;
+pub use inner::DataVariable;
+pub use inner::DataVariableRef;
+pub use inner::DataWhereClause;
+pub use inner::DataWhrDecl;
+pub use inner::MachineNumber;
+pub use inner::MachineNumberRef;
 
 /// Returns the number of leading `ATerm` arguments that are *not* data sub-expressions and
 /// must therefore be skipped by `data_arguments`, or `None` for binders/where clauses which