Does Linux have a system call to create a CoW copy mapping of a given memory mapping?
Like anonymous mmap() and then an mremap with a CoW flag.
Essentially I'm building a copy-on-(some-)write graph structure which needs to be um reasonably efficient.
So the background is that we need copies for some operations where we make a choice, but other (most) operations just simplify the graph but don't change the meaning of it so we don't want copies for those.
So that's what I want to optimize storage for.
Approaches on my mind are:
- forward journaling
- backward journaling
We don't really want to backtrack at all in most circumstances. CoW seems easiest, but backward journal might be better (where we simply record changes how to get back to the previous graph).
We actually also need to propagate conflicts we learned about in later phases up through the backtracking if this has any chance of being um reasonably efficient for SAT solving
data structures, long
@juliank at uni, we’re developing something similar (in java, however), for SAT solving actually
in a previous version of the system, we were basically using journaling. that makes backtracking relatively easy, but jumping across different branches of the derivation tree (e.g., some heuristic tells you to abandon whatever you were doing, try something else, but if that doesn’t yield a solution quickly, go back to wherever you were in the search space) become inefficient, because you always have to first go back to the common ancestor, and then drill down again
currently, we’re experimenting with persistent data structures. HAMTs seem to work nicely as a big collection of labeled tuples (~graph edges). we’re following this paper: https://michael.steindorfer.name/publications/oopsla15.pdf but implemented it from scratch with our own optimizations
one particular optimization that seems useful is to have immutable and mutable tree nodes, and “check in” a new revision of a collection by copying each mutable node into a packed immutable one, which can handle batch updates more efficiently (immutable -> mutable when performing an update is just CoW)
of course, a persistent set of tuples is barely a graph, so we also have to maintain indexes for adjacency. the cool thing is that it’s very fast to determine the delta between two persistent data structures (just iterate over the two trees, skipping over immutable nodes that are referentially identical): when backtracking, you can calculate a delta (usually small), and update (mutable) indexes accordingly. we’re using https://github.com/viatra/org.eclipse.viatra to incrementally maintain indexes and graph queries, but https://github.com/vmware/differential-datalog would be another alternative
another idea would be to use another persistent data structure, like a ROMDD, radix tree, or even B-tree to store the indexes. but that might lead to pathological behavior on some inputs (that a randomly selected hash function in HAMT can avoid)
w.r.t. doing this in native code, I think you could get away with just releasing all mutable nodes when “checking in” and never releasing immutable ones (since “checking in” can control the number of stored versions, hopefully, there won’t be extremely many). otherwise, I’d try adding a refcount to mutable nodes, but I have no idea about its efficiency
@kristof do you have more similarities with https://wiki.debian.org/Teams/Apt/Spec/PrimitivesSolver ?
I found some papers that had similar approaches. Optimally I don't have any learning clauses/nodes so it's all super slow.
@kristof I'm also wondering about exploring different parts of the graph in parallel, after all we have multiple cores today.
But this needs to be done efficiently - we only want to explore likely solutions in parallel :)
@juliank we’re trying to generate large(-ish) graphs which satisfy some first-order constraints (useful as test inputs or design space exploration), so we have the benefit that our graph starts small and grows big as the solver runs – it seems you’re having to deal with the opposite
but I’ll try to keep this use-case in mind – the very least, now I know that I could make nice graph-processing benchmarks from
apt install :)
clause learning seems quite hard in this space, because the nodes of the graph ‘shift’ around as you are merging them (we’re doing the opposite by splitting), so there is no easy way to generalize the results of conflict analysis into a lemma…
@juliank the parallel exploration on different parts of the graph sounds a bit weird for me at first. in the end, you’d need to integrate the results from multiple threads, where the nodes could have shifted around in different ways.
a simpler approach could be to explore different parts of the search space in parallel: say, pick an initial branching point, and explore the possible outcomes (selected node in the or-group in your case) in separate threads. however, this may need more memory to keep track of each candidate solution on each threads (but persistent data structures with structural sharing can reduce the overhead considerably)
@juliank btw (I am not very familiar with apt, so pardon me if this is nonsense), how large/difficult are these dependency resolution problems that you need a custom decision procedure for them? naively, directly encoding everything into SAT seems possible
(OTOH p2 in Eclipse does just that, and is usually dreadfully slow)
@kristof Let's put it the other way around: They're trivial enough that you can get away writing a custom one.
And that will be more predictable in a sense than a SAT solver with heuristics, or realistically the optimizing PWMAXSat or PBO solvers that you can currently plug in.
@kristof So you have a package that depends on mysql | sqlite backends and the optimizing solver will pick the sqlite backend, but apt's greedy solver which we need to replicate picks the first choice it has a reasonable chance of satisfying.
@kristof I have basic encoding for optimization functions for those things but not tweaked them as I never finished writing them.
The graph solving thing is an experiment to play around with. And I want it to be able to make greedy decisions to, to speed up solving at the expense of optimality.
@kristof I'm not sure if either my graph solver or the Z3-based objective solver (let's call it that, it's also a pun) are practical in terms of performance.
My clasp based PBO solver sometimes ran off into too slow territories trying to calculate the optimal upgrade solution.
@kristof Even if you manually install foo, and then try to install a package that conflicts with foo, apt would remove foo.
It's solver is nuts. It's two solvers. The first one goes through the set of packages to install and then marks packages for install or removal recursively based on whether it's a Depends or a Conflicts.
If that causes conflicts, a 2nd solver later tries to resolve that with some heuristics which not always work out the way intended.