Skip to content

Commit fbc4bba

Browse files
committed
extract cache into its own, shared structure
1 parent 8f73cc6 commit fbc4bba

File tree

5 files changed

+90
-29
lines changed

5 files changed

+90
-29
lines changed

chalk-integration/src/lib.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ pub mod tls;
1414
use chalk_engine::solve::SLGSolver;
1515
use chalk_ir::interner::HasInterner;
1616
use chalk_ir::Binders;
17-
use chalk_recursive::RecursiveSolver;
17+
use chalk_recursive::{Cache, RecursiveSolver};
1818
use chalk_solve::Solver;
1919
use interner::ChalkIr;
2020

@@ -104,7 +104,11 @@ impl SolverChoice {
104104
} => Box::new(RecursiveSolver::new(
105105
overflow_depth,
106106
max_size,
107-
caching_enabled,
107+
if caching_enabled {
108+
Some(Cache::default())
109+
} else {
110+
None
111+
},
108112
)),
109113
}
110114
}

chalk-recursive/src/cache.rs

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
use crate::UCanonicalGoal;
2+
use chalk_ir::interner::Interner;
3+
use chalk_ir::Fallible;
4+
use chalk_solve::Solution;
5+
use rustc_hash::FxHashMap;
6+
use std::sync::{Arc, Mutex};
7+
use tracing::debug;
8+
use tracing::instrument;
9+
/// The "cache" stores results for goals that we have completely solved.
10+
/// Things are added to the cache when we have completely processed their
11+
/// result, and it can be shared amongst many solvers.
12+
pub struct Cache<I: Interner> {
13+
data: Arc<Mutex<CacheData<I>>>,
14+
}
15+
struct CacheData<I: Interner> {
16+
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
17+
}
18+
19+
impl<I: Interner> Cache<I> {
20+
pub fn new() -> Self {
21+
Self::default()
22+
}
23+
24+
/// Record a cache result.
25+
#[instrument(skip(self))]
26+
pub fn insert(&self, goal: UCanonicalGoal<I>, result: Fallible<Solution<I>>) {
27+
let mut data = self.data.lock().unwrap();
28+
data.cache.insert(goal, result);
29+
}
30+
31+
/// Record a cache result.
32+
pub fn get(&self, goal: &UCanonicalGoal<I>) -> Option<Fallible<Solution<I>>> {
33+
let data = self.data.lock().unwrap();
34+
if let Some(result) = data.cache.get(&goal) {
35+
debug!(?goal, ?result, "Cache hit");
36+
Some(result.clone())
37+
} else {
38+
debug!(?goal, "Cache miss");
39+
None
40+
}
41+
}
42+
}
43+
44+
impl<I: Interner> Clone for Cache<I> {
45+
fn clone(&self) -> Self {
46+
Self {
47+
data: self.data.clone(),
48+
}
49+
}
50+
}
51+
52+
impl<I: Interner> Default for Cache<I> {
53+
fn default() -> Self {
54+
Self {
55+
data: Default::default(),
56+
}
57+
}
58+
}
59+
60+
impl<I: Interner> Default for CacheData<I> {
61+
fn default() -> Self {
62+
Self {
63+
cache: Default::default(),
64+
}
65+
}
66+
}

chalk-recursive/src/lib.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,15 @@ use chalk_ir::{Goal, InEnvironment, UCanonical};
33

44
pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
55

6+
mod cache;
67
mod combine;
78
mod fulfill;
89
mod recursive;
910
mod search_graph;
1011
pub mod solve;
1112
mod stack;
1213

14+
pub use cache::Cache;
1315
pub use recursive::RecursiveSolver;
1416

1517
/// The `minimums` struct is used while solving to track whether we encountered

chalk-recursive/src/recursive.rs

Lines changed: 13 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
use crate::cache::Cache;
12
use crate::search_graph::DepthFirstNumber;
23
use crate::search_graph::SearchGraph;
34
use crate::solve::{SolveDatabase, SolveIteration};
@@ -7,7 +8,6 @@ use chalk_ir::Fallible;
78
use chalk_ir::{interner::Interner, NoSolution};
89
use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
910
use chalk_solve::{coinductive_goal::IsCoinductive, RustIrDatabase, Solution};
10-
use rustc_hash::FxHashMap;
1111
use std::fmt;
1212
use tracing::debug;
1313
use tracing::{info, instrument};
@@ -22,12 +22,10 @@ struct RecursiveContext<I: Interner> {
2222
/// The "cache" stores results for goals that we have completely solved.
2323
/// Things are added to the cache when we have completely processed their
2424
/// result.
25-
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
25+
cache: Option<Cache<I>>,
2626

2727
/// The maximum size for goals.
2828
max_size: usize,
29-
30-
caching_enabled: bool,
3129
}
3230

3331
/// A Solver is the basic context in which you can propose goals for a given
@@ -45,13 +43,9 @@ pub struct RecursiveSolver<I: Interner> {
4543
}
4644

4745
impl<I: Interner> RecursiveSolver<I> {
48-
pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
46+
pub fn new(overflow_depth: usize, max_size: usize, cache: Option<Cache<I>>) -> Self {
4947
Self {
50-
ctx: Box::new(RecursiveContext::new(
51-
overflow_depth,
52-
max_size,
53-
caching_enabled,
54-
)),
48+
ctx: Box::new(RecursiveContext::new(overflow_depth, max_size, cache)),
5549
}
5650
}
5751
}
@@ -83,13 +77,12 @@ impl<T> MergeWith<T> for Fallible<T> {
8377
}
8478

8579
impl<I: Interner> RecursiveContext<I> {
86-
pub fn new(overflow_depth: usize, max_size: usize, caching_enabled: bool) -> Self {
80+
pub fn new(overflow_depth: usize, max_size: usize, cache: Option<Cache<I>>) -> Self {
8781
RecursiveContext {
8882
stack: Stack::new(overflow_depth),
8983
search_graph: SearchGraph::new(),
90-
cache: FxHashMap::default(),
84+
cache,
9185
max_size,
92-
caching_enabled,
9386
}
9487
}
9588

@@ -202,9 +195,11 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
202195
minimums: &mut Minimums,
203196
) -> Fallible<Solution<I>> {
204197
// First check the cache.
205-
if let Some(value) = self.context.cache.get(&goal) {
206-
debug!("solve_reduced_goal: cache hit, value={:?}", value);
207-
return value.clone();
198+
if let Some(cache) = &self.context.cache {
199+
if let Some(value) = cache.get(&goal) {
200+
debug!("solve_reduced_goal: cache hit, value={:?}", value);
201+
return value.clone();
202+
}
208203
}
209204

210205
// Next, check if the goal is in the search tree already.
@@ -260,10 +255,8 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
260255
// cache now. This is a sort of hack to alleviate the
261256
// worst of the repeated work that we do during tabling.
262257
if subgoal_minimums.positive >= dfn {
263-
if self.context.caching_enabled {
264-
self.context
265-
.search_graph
266-
.move_to_cache(dfn, &mut self.context.cache);
258+
if let Some(cache) = &mut self.context.cache {
259+
self.context.search_graph.move_to_cache(dfn, cache);
267260
debug!("solve_reduced_goal: SCC head encountered, moving to cache");
268261
} else {
269262
debug!(

chalk-recursive/src/search_graph.rs

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use std::ops::IndexMut;
44
use std::usize;
55

66
use super::stack::StackDepth;
7-
use crate::{Minimums, UCanonicalGoal};
7+
use crate::{Cache, Minimums, UCanonicalGoal};
88
use chalk_ir::{
99
interner::Interner, Canonical, ClausePriority, ConstrainedSubst, Constraints, Fallible,
1010
NoSolution,
@@ -104,12 +104,8 @@ impl<I: Interner> SearchGraph<I> {
104104

105105
/// Removes all nodes with a depth-first-number greater than or
106106
/// equal to `dfn`, adding their final solutions into the cache.
107-
#[instrument(level = "debug", skip(self))]
108-
pub(crate) fn move_to_cache(
109-
&mut self,
110-
dfn: DepthFirstNumber,
111-
cache: &mut FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
112-
) {
107+
#[instrument(level = "debug", skip(self, cache))]
108+
pub(crate) fn move_to_cache(&mut self, dfn: DepthFirstNumber, cache: &Cache<I>) {
113109
self.indices.retain(|_key, value| *value < dfn);
114110
for node in self.nodes.drain(dfn.index..) {
115111
assert!(node.stack_depth.is_none());

0 commit comments

Comments
 (0)