We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Spack's new Concretizer

00:00

Formal Metadata

Title
Spack's new Concretizer
Subtitle
Dependency solving is more than just SAT!
Title of Series
Number of Parts
490
Author
License
CC Attribution 2.0 Belgium:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
Abstract
Dependency resolution is deceptively complex; simply selecting a set of compatible versions for an arbitrary network of dependencies is NP-hard. Much effort has been spent on this problem for modern single-language ecosystems, but many of these ecosystems rely on natively compiled libraries, and dependency mangers often fail at managing the additional complexities that native libraries entail. Further, dependency resolution has traditionally been modeled as a SAT problem, where the package manager should find any workable solution to satisfy package constraints. However, any solution may not be good enough. Users want the most tested, most optimized, or most secure configuration, and this is a SAT problem coupled with complex optimization. Spack is a package/dependency manager rapidly gaining popularity in High Performance Computing (HPC) that aims to address many of the complexities of native, multi-language, cross-platform dependency management. Spack has recently been reworked to use Answer Set Programming (ASP), a declarative logic programming paradigm that also provides sophisticated facilities for optimization. This talk will cover how we’ve been able to model the compiler toolchain, ISA, build options, ABI, and other constraints on native libraries. We’ll also talk about how ASP has been a useful tool for finding optimized dependency configurations. This work can be used to improve dependency resolvers in general — so that they can prefer more secure or tested configurations instead of simply selecting the most recent workable versions. Expected prior knowledge / intended audience: Audience should have basic knowledge of build systems and compiled languages, but we'll explain this up front with some brief background. The talk is aimed broadly -- for users, developers, packagers, researchers, package manager implementors, and HPC administrators.
SatelliteComputer animationLecture/Conference
Simultaneous localization and mappingComputing platformSource codePortable communications deviceDesign of experimentsSource codeData managementRevision controlMathematical optimizationBuildingCompilerBinary codeVirtual machineWebsiteComputer simulationData compressionProjective planeConfiguration spaceOcean currentIntegrated development environmentCodeEndliche ModelltheorieNuclear spaceSoftwareFormal languageData managementMultiplication signSupercomputerDifferent (Kate Ryan album)Graphics processing unitImage resolutionNP-hardCodeCoprocessorInformation securityQuicksortBitMikroarchitekturUser interfaceLecture/Conference
Computer configurationDifferent (Kate Ryan album)Parameter (computer programming)BuildingConfiguration spaceImplementationRevision controlCompilerSoftwareLibrary (computing)Formal languageResolvent formalismLecture/Conference
SupercomputerPointer (computer programming)Execution unitMenu (computing)Intrusion detection systemEmpennageTemplate (C++)Configuration spaceComplex (psychology)SoftwareCombinatoricsConstraint (mathematics)AbstractionData managementInvertible matrixSatelliteFigurate numberEndliche ModelltheorieRevision controlLogic programmingError messageProof theoryProjective planeConfiguration spaceDefault (computer science)AlgorithmComputer architectureCondition numberComplex (psychology)Computer configurationDifferent (Kate Ryan album)Virtual machineProper mapResultantBacktrackingStatisticsData managementQuicksortNumberLevel (video gaming)Thread (computing)FlagBoolean algebraoutputDistribution (mathematics)1 (number)Computer fileImage resolutionPoint (geometry)Self-organizationCore dumpUsabilityImplementationVector potentialElectronic mailing listLibrary (computing)Resolvent formalismRight angleBuildingSystem programmingConstraint (mathematics)SatelliteVirtualizationCompilerInformationMathematical optimizationIntegrated development environmentSoftwareSpacetimeCombinatoricsSoftware developerFile systemLecture/Conference
Data modelRevision controlConstraint (mathematics)Error messageTraffic reportingSatelliteData structureTrailMessage passingMathematical optimizationComplex (psychology)Bit2 (number)Video gameMathematical optimizationRevision controlLimit (category theory)
Interface (computing)Modulo (jargon)TheoryApplication service providerComputer programmingComputer configurationStandard deviationIntegerMathematicsLogicOperations researchMathematical optimizationMultiplicationFormal grammarFormal verificationStress (mechanics)Personal digital assistantComplex (psychology)Error messageSatelliteProof theoryManufacturing execution systemAlgorithmImplementationQuicksortTheoryHigh-level programming languageConstraint (mathematics)Mathematical optimizationNichtlineares GleichungssystemApplication service providerComputer programmingInformation securityComputerAdditionMathematicsRight angleBoolean algebraProof theoryProjective planeBoolean satisfiability problemFormal verificationJackson-MethodeComputer animation
MereologyApplication service providerAlgorithmPrototypeLogicLine (geometry)Repository (publishing)BuildingParsingFraction (mathematics)Computer configurationManufacturing execution systemFraction (mathematics)ResultantElectric generatorMultiplication signRight angleString (computer science)Computer programmingElectronic mailing listDifferent (Kate Ryan album)Computer fileDeclarative programmingRevision controlLogic programmingStatement (computer science)Source codeComputer animation
SpacetimeRevision controlWeightApplication service providerLogicRevision controlCognitionStructural loadLogic programmingAsynchronous Transfer ModeSpacetimeQuicksortWeightMereologyLine (geometry)Application service providerStatement (computer science)CodeBitComputer animation
CompilerPersonal digital assistantWeightLogicArchitectureCodeCompilerCodeCompilerCompilerMathematical optimizationComputer architectureRevision controlQuicksortComputer animation
Virtual realityLogicConstraint (mathematics)Internet service providerSource codeLogic programmingInterface (computing)Internet service providerDifferent (Kate Ryan album)ImplementationConstraint (mathematics)Symbol tableComputer animation
Application service providerMathematical optimizationPersonal digital assistantWritingSqueeze theoremMathematical optimizationMaxima and minimaConstraint (mathematics)NumberDefault (computer science)BuildingLine (geometry)CodeComputer configurationCurveQuicksortComputer animation
Installation artRevision controlInstallation artImplementationLibrary (computing)Computer animation
Installation artComputer configurationEndliche ModelltheorieConstraint (mathematics)BuildingRight angleArithmetic meanSource codeComputer animation
InformationError messagePersonal digital assistantMessage passingProof theoryPoint (geometry)Constraint (mathematics)QuicksortMaxima and minimaPrototypeCASE <Informatik>Goodness of fitFunction (mathematics)Error messageSet (mathematics)Constraint (mathematics)Proof theoryElectric generatorMechanism designCore dumpComputer animation
System programmingMathematical optimizationPoint (geometry)CompilerDeterminismError messageApplication service providerControl flowMathematical analysisGodFerry CorstenLibrary (computing)Constraint (mathematics)Revision controlIntegrated development environmentStandard deviationSystem programmingDivergenceLink (knot theory)Run time (program lifecycle phase)Configuration spaceQuicksortProcess (computing)InformationExistencePoint (geometry)System callGraph (mathematics)Computer animation
PlastikkarteInstallation artConstraint (mathematics)Gaussian eliminationMaxima and minimaRight angleGraph (mathematics)ImplementationImage resolutionComputer configurationConfiguration spaceTotal S.A.NumberNP-completeWeightSatelliteMultiplication signSource codeComputer animation
SpacetimeRevision controlWeightApplication service providerLogicWeightPlastikkarteComputer fileDifferent (Kate Ryan album)SpacetimeOrder (biology)Configuration spaceImage resolutionMultiplication signSimplex algorithmMathematical optimizationConstraint (mathematics)Optimization problemGreedy algorithmRevision controlComputer animation
Installation art1 (number)QuicksortCore dumpSource codeConfiguration spaceProof theoryBinary codeSystem programmingLine (geometry)Computer programmingSource codeComputer animation
Application service providerMereologyAlgorithmPrototypeRepository (publishing)LogicComputer configurationBuildingFraction (mathematics)ParsingLine (geometry)Electric currentImplementationSource codeIntegrated development environmentGraph (mathematics)NP-hardTraverse (surveying)Scale (map)Condition numberDefault (computer science)Constraint (mathematics)Conditional probabilityKolmogorov complexityInclusion mapData managementComputer fileAbstractionSet (mathematics)Regular graphEndliche ModelltheorieSimilarity (geometry)Software developerRootCross-platformoutputConfiguration spaceQuicksortVirtual machineComputer animation
Point cloudOpen sourceFacebook
Transcript: English(auto-generated)
All right, I'm Todd. I'm from Lawrence Livermore National Laboratory.
For people who aren't familiar with that. It's a national security laboratory. It's about an hour from San Francisco. And we run a lot of supercomputers, which is sort of the motivation for SPAC. I'm going to talk a little bit about dependency management in general first. So, so far we've heard from a lot of different dependency managers, what's managed by dependency managers, typically.
It's usually, what packages does this project depend on? And what version of each of the installed package, or what version of each of the dependencies should I actually install? And so if you think about, what does that look like as a package model? For most package managers, it's like this. It's a little, this is a node, it has a name,
it's got a version, it depends on some other things and some other versions. And so it's fairly simple. It gets to be complex when you start to do dependency resolution on this. It's NP-hard even to select the versions for a DAG. But this is pretty much what most package managers are resolving. The concerns that people typically have with what versions are selected are,
do I have correct or compatible versions? Do I have the latest version? Do I have the most tested version? Do I have a secure version? Those are the kinds of things we've heard about so far. This is gonna be a slightly different kind of talk. We're gonna talk about building, basically resolving dependencies for optimization and not necessarily for these concerns,
although we care about those too. So, some fairly common but maybe questionable assumptions that your package manager makes, and we've talked about these today too, are, hey, there's a one-to-one relationship between the source code and the binary. This is an assumption that Debian makes for their reproducible builds project. It sort of assumes that you're only gonna build source code one way. And we don't really do that in HPC.
Binaries should be as portable as possible in most distros. It's bad for performance. If you build dash O2 dash G binaries, they're not gonna run fast. And so if you have something performance-critical in your stack, you need to be able to build it a fast way, which is harder than building the portable binaries.
The other assumption that typically is made is the tool chain's the same across the ecosystem. I'm gonna build this thing with the standard compiler, or maybe I don't even have a compiler. I'm using an interpretive language. And so we'd like to be able to actually resolve the compiler in the stack. And then the assumption that users build and deploy configurations that were tested before.
Most package managers are taking an artifact that someone generated, that they tested, they're deploying it. What we'd really like on the stack project at least is that it would be really nice if building something for the first time were just as easy as building something that someone built before. So that's what we're working towards. And why are we doing that? We build for machines like this.
So these are some of the Department of Energy's current and upcoming supercomputers. And so if you look at these, there's four plus different CPU architectures and four plus different GPUs across these machines. None of these looks the same. And so typically when we're building something, we're building in a pretty new, probably bleeding edge environment if we want to tune for the machine.
And so code is typically distributed as source, which is pretty horrible. It's a pain. We have to build it all the time. We build many variants of the same package. The code's optimized for the processor model. And so it's not an O2-G binary. It might even be optimized for like Skylake, Cannon Lake, a particular model of the processor,
not just X86-64. There's no standard ecosystem. Most things are Linux, but the user environment and where the software on the machine is is very different from site to site. And then it's multi-language. So we're not dealing with one package ecosystem. We're dealing with C, C++, Fortran, Python, lots of other things. It's pretty complicated.
So these are the kind of things that we're building. These are large simulations for things like compressible flow, nuclear reactors, urban disasters, radiological problems, things like that. And so the model becomes a lot more complicated. So this is the DAG I showed before. This is a node where you're just selecting
for a name and a version. What we're tuning in SPAC is this. So this is build configuration options, so particular parameters that you might pass to configure or different options on the package, different library implementations. So I may not depend on just one library. I might depend on MPI, of which there are three or four different implementations
with different versions on each of them, different configuration options, different networks. I'm tuning for different GPUs, different CUDA versions. I'm tuning for the compiler. There may be more than one compiler for my language ecosystem. All of this gets pretty complicated. So what we want is a dependency resolver that can select all the parameters here, not just this.
So SPAC enables that. It's designed to enable software distribution for HPC. We're automating the build and installation, so we're not just selecting from existing versions. We're actually generating a space of packages. We're generating DAGs to build different versions of things. The packages are templated, so there's one package, Python file per package,
per project, I guess, and then it has a lot of different parameters, so you can build this combinatorial explosion of packages. And so we're pulling a lot of lower-level aspects of the software ecosystem up to the package manager level. That's the build parameters and things that I just talked about. It's written in Python, but like I said, we can package whatever.
And so what we really want is the ease of use of mainstream tools, all the stuff that modern software developers are used to, but for this somewhat antiquated software ecosystem that we have to deal with in HPC. We're doing okay. It's a pretty popular project. It's not as popular as many JavaScript projects, but it is used all over the world at different HPC sites,
and so this is sort of proof that we are bringing the ecosystem together. We're getting lots of contributions on the package side from lots of different organizations. We have over 500 contributors now, and even the core is getting contributions from lots of different folks. And we're used on some of the biggest machines out there. So we're used on the number one system at Oak Ridge Summit, the number two system at Livermore,
which is a similar machine. That's where I am. And we're gonna be used for the upcoming ARM64FX system from Fujitsu that's gonna get deployed at weekend, so we have a partnership with them. So lots of interesting machines. This is what it looks like from sort of a user level. You can install a package just normally. You can say, I want this package. Just say the name of it,
and we'll give you something with sensible defaults. You can get a lot more specific, though. You can say, I want a particular version. You can say, I want a particular compiler and a particular version of that compiler. You can say that you want to have threads enabled, different build options. You can inject flags into the build, so you could basically build 60 versions of the same package with different flags. You can target specific microarchitectures,
so you can say, I want to build for Skylake. And you can also do that for all the dependencies, so you can get specific about your dependencies and what they do. And so this is what the command line configuration looks like, so if you install one thing. The packages, like I said, they're templated, and so if people are familiar with Homebrew, the package recipes look a lot like Homebrew.
They're just written in Python, but they're also templated, so you can have lots of different versions, lots of different options, lots of different dependencies that are potentially optional, and then there's build recipe stuff down here. And so with that, what we're doing is we're enabling you to build all of the things. We want you to be able to build this DAG,
but configured lots of different ways. And so for each configuration of that graph, we generate a hash, and we install everything in its own prefix. And so as many versions as you want of all these different packages can coexist together. And they're all R paths, so you don't have to worry about finding dependencies. You don't have to worry about setting up your LD library path. They all know where to find their dependencies
when we build them. So what does the dependency resolver do? We call it the concretizer in SPAC. We take an abstract spec like that. That's basically what does it look like on the command line. And then we basically normalize it, so we produce a DAG that has some of the constraints filled in.
And then if you think about what the dependency resolver is doing, it's solving this problem. It's filling in all the blanks in a consistent way. So we take that DAG, we turn it into the giant JSON thing that I showed you, and we store that in the file system with all this provenance. For an environment, we support virtual environments, and with sort of the manifest lot file model
that Bundler popularized. So we can do SPAC.yaml, which is sort of the input format. It's like a bunch of different specs, like the ones that I showed on the command line. And we produce a lot file with all that information for all the different dependencies in your environment. This has gotten to be pretty complicated. And so this is where this talk sort of picks up.
We're taking lots of constraints from lots of different places, and we're trying to integrate them into one gigantic SAT solve. And that's pretty nasty. So there's the stuff that I showed on the command line. There's all the constraints that came from the package file that I showed for all the dependencies in the project tree. There's constraints that can be in the environment, so users can actually specify their preferences
for how dependencies are resolved. And then there's other configurations. You can have local configuration for your user, for your site, and there's defaults from SPAC. And so all of this stuff sort of gets mushed into one solve, and we traverse the DAG repeatedly. We evaluate conditions, add dependencies, and we repeat this until the DAG doesn't change. So it's kind of a fixed point algorithm
in the current version. And the issue with this is that there's limited support for backtracking. It's pretty greedy. You can sort of decide the version of something over here and then discover a conflict over here and not have them resolved properly. And then the constraints are, yeah, so the constraints are ordered. So you may discover that you've selected the compiler,
but you wanted to build for an architecture that it turns out that compiler doesn't support. And really you have to kind of solve those things together to get a consistent DAG. And so this results in a whole lot of conditional complexity for a solver that isn't all that powerful compared to what some of these full backtracking solvers can do.
And so it's gotten to be hard to add new features and logic, and it can be slow, because we're basically building the DAG over and over and over again in Python. So we started looking into what are the options. Stat solving looks pretty appealing. There are lots of dependency managers that use stat solvers. Getting into the world of stat solving
is not for the faint of heart. There are lots and lots of different sub-communities there, and they all do sort of variants on the same thing. And so this took a lot of research to sort of figure out what's the best way to do this, or what do existing tools do? So PicoSat is probably your most simple portable C solver. It uses advanced techniques for actually doing a sat solve,
but it's pure Boolean logic. And so if you want to write your solver in pure Boolean sat, it turns out you have to do a lot of cumbersome things. You have to implement arithmetic in Boolean logic, if you want to do anything like optimization. So you're really building an adder in Boolean logic, which is nuts.
Conda does this. It ends up being kind of slow in Conda, and so people have looked at libsolve as a potential solution for that. Libsolve is also a sat solver. I think it does some of this, but it's very targeted towards a traditional package model. So it seems like libsolve solves mostly the node model that I showed on the first slide, where you're just thinking about packages and versions. And so it didn't seem like we could get inside something like that,
and really customize it to our needs. PubGrub is awesome. I think people have heard of that. Who's heard of PubGrub? This is sort of next-gen version solving. It's a CDCL solver, which it learns clauses and conflicts as it goes along. So it's a powerful sat solver. And it has some logic in it that basically maintains a list of conflicts
as it does the solve. And so if you get an error in PubGrub, it comes back to you and says, oh, hey, this depends on another version of this. This depends on another version of this. And so you need to adjust the version of this package to fix your solve, because it's not compatible right now. So it essentially gives you a proof of what's unsatisfiable about your DAG, which is cool.
But the model, again, is kind of limited. It's package and version for PubGrub. And to use it, we'd have to sort of integrate it into our own solver and do our own custom thing. And we really didn't want to do that. We needed multi-criteria optimization. I'll get into that a little bit in a second. And tons of people's life work has gone
into basically taking sat solvers, integrating them with optimization solvers, and making that fast. And so we really were worried about implementing a custom solver in Python. So we sort of stayed away from this. The two things that we kind of boiled down to in the end were, so there are these things called SMT solvers. This is like a sat solver,
but it actually has theories integrated into it. And what that means is that for your Boolean solve, it's doing basically all your advanced sat algorithms. For the actual clauses in the solve, you can do things like math. You don't need to implement math in Boolean sat. You can actually use other sort of theory solvers
for the equations themselves that go into the sat solve. So that's pretty cool. You can call out to a theory solver from within your sat solver. It also does multi-criteria optimization, and Z3 is really popular in the formal verification community. So this is for security people who want to say, this is a heap, and it only does heap things.
It will not attack your computer in addition to that. So this turned out to be pretty cool. And it also has some really advanced proof capabilities, which we're looking into. Answer set programming is the other one that we looked into. There's a really capable answer set solver called Patasko, or I guess the solver's called Clasp. The package is called Clingo,
and the project is called Patasko, so I don't know exactly what to call it. But that's the project. This seems like the most active ASP project right now. And note, this is not active server pages. This is answer set programming. And the cool thing about this is that it's a very high-level language. So you can write your constraints in something that looks like Prolog.
Who's programmed in Prolog? Yeah, which is kind of nice, right? It's nicer than Boolean clauses. And it makes for very short programs. It boils down to SAT, and they do optimization in some of these other things. So we ended up deciding to implement our new solver in ASP to see how that would do.
So this is what it looks like. We use Clingo. It's the package I'm talking about. The ASP program basically has two parts. Instead of what I was talking about before, where we would basically iteratively construct the DAG, what we're doing is we generate a big list of facts from all of our package files and all of the different preferences files
that we have for the solve. And so that tends to be, and these are surprising numbers, but if you think about the size of the package ecosystem, they make sense. It's like 6,000 to 9,000 facts for our typical solves. And so these are these really long files. They look like this. It just says, hey, this package has this version declared.
This package has this option. This package has these criteria or these conflicts. All of that goes into just a pure list of statements that say this is true. And then there's a really small logic program, like 130 lines, that we concatenate with that and throw into the solver. And the new algorithm, it's conceptually much simpler.
You generate all the facts. You concatenate it. You send it to the solver. You take the result that it spits back at you and you build the DAG out of that. And so this is a pretty big win. The solve time itself is much faster than the existing concretizer, just because we're calling out to a native package. So it's like a fraction of a second for the actual solve. But for the actual generation of the program,
that's the bottleneck right now. We're in Python, so actually generating all the strings to send to the solver takes the bulk of the time. So we're working on making that faster. And so just to give you sort of a flavor of what this looks like, ASP makes it pretty easy to put what was once very complicated logic
in sort of our custom solver into one place. So the things that you do when you're writing an ASP solver are you define the space. This just says that there's, you know, for every node in the DAG, it has one possible version. That's it. These are cardinality rules. They say I have one version per node. That's what my space looks like, at least for this part. This says don't allow conflicting versions.
And then this part down here just says, hey, if I declared a version with a particular weight, if I had a particular preference on it, then give it that weight in the DAG. And then this is a minimization statement. And it says minimize the total weight for all the versions in the DAG. And so this is really concise. It's pretty cool. It takes a bit of cognitive load to get into this mode of thinking
and to start writing these things down. So despite the fact that this is like four lines of code, it took me a lot longer to think about this than it did about other lines of code that I might write. Other stuff became simple too. This is the compiler target optimization I was talking about. We have stuff in SPAC that tells us
which compiler versions can generate code for which architectures. And so if you have a bunch of compilers available and you have a bunch of architectures that you could build for, because you know that you're on a Haswell system, and you know that the compilers can generate up to Ice Lake or something like that, picking a compiler and picking a target is not 100% straightforward. If the user said they want to build with a particular compiler, you may have to downgrade the target that you build for.
And so this allows us to solve for that at the same time. And it was previously like this sort of staged logic, but now we're able to do something much simpler where essentially we say there's one target per node, we say you can't have a node where the compiler doesn't support the target that's assigned to it, and then the rest is just optimization
like the other ones. And so this works out to be very simple. Like this was super exciting that all it took was like this line, and all of a sudden the targets are right because we told it what was wrong. So the dependency logic is also pretty concise. We can easily take constraints from different places. We can do virtual dependencies, and so this is all the logic that it takes to say
if I depend on MPI, I actually depend on MPitch and Vapitch or OpenMPI, the implementations of the MPI interface. So all that's in there. And constraints like I can only have one provider for MPI in my DAG. If I have both OpenMPI and MPitch in the same DAG,
that's bad because the symbols will conflict. And so I can put constraints like that in there. Not all of this was simple. Like I said, the learning curve is pretty high, and there's a lot of thought that goes into every line of code. And structuring the optimization criteria can be a challenge. So when I first started doing this, I wrote my criteria as sort of maximize constraints.
And so that led to some surprising behavior. So I would solve what I thought was a pretty small DAG, but I said maximize the number of build options set to their default value. And it was like, oh hey, I can just add more packages to this DAG to get more build options set to the default value.
And so I would get these giant DAGs out of the thing. And so you have to think about how you formulate the constraints. So most of the constraints are now minimizing so that the DAG stays pretty small. One interesting example that I think is kind of funny is the previous version of the solver, if you said, SPAC install HDF5 with MPitch,
users would get annoyed. That says, install the HDF5 library with the MPI implementation as MPitch. Users would get annoyed because it wasn't smart enough to say, oh, I have to turn on the MPI support to make that happen. And so users would have to write this instead. And so that's fine. That gives you a pretty nice small DAG. The new solver can be pretty smart.
And so I was like, okay, obviously this will fail if I say don't build it with MPI and build it with MPitch in the DAG. But no, it actually was like, oh, I see that if I make the, if I depend on libAEC, which depends on CMake, which depends on libArchive, which depends on LZ4, Valgrind, and then Valgrind has an option for MPI,
I can get MPitch in your DAG right there. So I'll make it happen for you. You have to put some other constraints in to make this sane. And so I think what we'll do is basically say, don't search through build dependencies for things like this where you're saying, definitely include this node in the DAG.
But in general, this is pretty exciting because it means you can solve for some pretty complicated things. You can see up here it tried 338 different models and compared them all, figured out this was the optimal one for that particular configuration, and it was pretty cool. Getting errors is still a little tough. The ASP solvers don't have good mechanisms
for getting what's called unsatisfiable cores out, sort of the minimum set of constraints that aren't satisfiable. They also don't have proof generation. So one interesting thing about Z3, the SMT solver, is that it can actually generate you a pretty cool proof of why was this DAG unsatisfiable.
And so I think we could take that and potentially parse it and do something with it to make it look like the good output from PubGrub. But the Z3 proofs are pretty involved. If anyone's ever seen a Z3 proof, it is not like, it's not in English. It is in some other language. And so parsing that will be interesting. So anyway, that's where we're at right now.
We have a working prototype. It's pretty satisfying to see it solve cases where we couldn't solve things before. And we've managed to pull a lot of stuff that is typically sort of assumed by the distro or assumed by the build system, or just kind of has to be tweaked by humans in the package curation process up into the solver so that you can actually solve for configurations.
And so the goal here, like I said, is to make it so that people can have nice things in HPC. So that it's easy to build on a new system and to get a new DAG working in a place you haven't built it before. It would be really cool to be able to use tools like Fasten for deeper solves. And so the C and C++ and Fortran world
are absolutely horrible at SemVer because it didn't exist when they started existing. And so we don't really know the compatibility between packages. And people tend to write their package constraints. Humans generate those. They generate them either based on what they know, what was the first version that I tested with, or what have they actually tested with.
And typically that's kind of over-constrained, right? You could get a DAG working with a different version of a library, most likely, if it was pretty close to what you had in the tested configuration. And so we could use information like the call graph stuff to figure out are the entry points and exit points of libraries compatible? Could we plug this other package in
at more versions than maybe the humans specified, but prefer the tested version while allowing more divergence to get things working? Other stuff that we'd like to be able to do that I think we can do with this new solver is solve for cross-compiled build DAGs. So actually do things like if something has a build and a link dependency on a library, build it once for the front-end environment
where we're compiling and build it again for the back-end environment where we would be running. And so figure out where to split nodes in the DAG. I think we could definitely do that. Do things like compile a runtime compatibility and make sure that your lib standard C++ library is consistent across your DAG. That's a thing that bytes our users very frequently if we get ahead of the system lib standard C++.
And then do things like integrate licenses into the solve. So that's where we're at. If you want stickers for SPAC, they're up there on the front row, so grab one. And I'll take questions.
Sorry, I can't hear you. Oh, 25, okay. Right here? Can you repeat? Why, to this solution?
This one right here? So this just says install hdf5 where hdf5 has MPI disabled. So on this node up here, it says turn off MPI support. And this says mPitch has to be a node in the graph. And mPitch is an MPI implementation.
And so what it does is it says, it searches all the configurations, right? This is like an NP complete solve. And it says, oh look, Valgrind can have an MPI option. So I can disable MPI on hdf5 and not link MPI to it. But I'll turn on MPI support for Valgrind, get mPitch in the DAG that way. And oh, this is how I get to it, right?
So it finds that pretty quickly. And yeah, so at first I thought this was a bug. And then I was like, no, no, it's right. For some definition of right, yeah. Sorry, you can't, I mean, so it considered 338, right?
And that's less than the total number of solutions that you could find for this. That's how many it had to consider to find an optimal one by the criteria that we used. So yes, it considered a lot of solutions. You can get this thing to spit out all the solutions, but if you try that on a DAG like this, it's gonna sit there for a long time generating different configurations.
So I guess if you consider that, we have more packages than NPM. But, sorry? No, this is the optimal one. So it's doing both a SAT solve to make sure that the constraints are correct. And it's saying, oh, if I go down that path, everything will get worse, right? And so I'm, no, it doesn't. Because I know that if I go down a certain path,
it can eliminate options and say, nothing down that path is good. So I'll consider, yeah. So yes, in the worst case, it would require you to do that. And so yes, this is NP-complete. It can get bad. Yeah. How does it know something like weights also? Yeah, we have weights. Give it points or? Yeah, the minimization criteria that I showed back here.
So see down here? In the thing that we generate, right? We have our preferences file, and so we say, okay, the user really likes this version, so we'll put it at the top. The next best version is the latest and the next latest and so on. We weight them that way, and then we take the weight and we put it in the solve. And so that's what this is doing. And so in the end,
we have about seven different criteria for this. And you pick an order lexicographically that you want them optimized, and it comes up with an optimal solution according to that. Other questions? Is it doing a greedy search to write the optimal solution? It's doing a CDCL solve. So it's conflict-driven clause learning.
So it's doing that at the same time as doing a simplex or some other kind of optimization algorithm, which is why I didn't want to write this myself, because integrating those two things seems like a nightmare. There's papers about it. But yeah, it's doing a lot of smart stuff to find the right solution. Yep. Is it doing the packaging itself too,
or is it just dedicating to something like RPM? Oh no, so SPAC builds packages too. So it's end-to-end. You have a bunch of package files that are basically recipes plus these constraints. For basically, they define the space of packages you can build. And once you get a configuration
like this, we hand that to the build, and we say, go build this. And the packages are written so that they query the DAG for what to build. And so if you wanted to think about reproducible builds in this context, it wouldn't be like there's one source and one binary that corresponds to it. It would be more like there's one source,
there's this configuration in a binary, and that should be reproducible. Paul says optional, and then that's optimized, and then the ones that can be solved
because they will be not satisfied then? I guess I didn't fully understand the question. Have we considered what? You have the requirements? Yes. To make them all, you can make them more optional? Yes. So and then you could solve and optimize that to satisfy as many as possible?
Yeah, so the iterative way of debugging these programs is typically to comment out constraints and see which ones make it work. Right? Yeah, yeah, yeah. That's sort of what the proof generator that I talked about for Z3 and what the sort of unsack core thing will do for you.
It'll say here's, these are the cores I found for this problem that are completely unsatisfiable. If these are in your problem, it won't be satisfiable. So I think we can do something based on that because that's essentially what PubGrub and other systems do. They build proofs or they look at the unsack cores. We just haven't done it yet.
From the first line to the second line, and you know there's a changing behavior where? So if you, so this depends on all the stuff that I said went into the concretizer, right? So it's what you wrote on the command line. It's all this stuff. This goes into the solve, right? But we do spit out a lock file, right?
So like, if you, once you solve and you get a solution, right? We spit it out as JSON and you can go and reload that and rebuild the same thing again if you want to exactly, right? And then in another sort of sense, you can take this and use it as sort of a reproducible description but cross-platform. You could take this and reconcreteize it on a new machine
and get something that meets these constraints, but you know, it may be slightly different underneath to make it work. It's reproducible on the same machine with the same inputs, right? Like that, and so you have the inputs. You can reproduce what you did. What's different is that you can tweak it more easily
and you can produce different configurations faster. Yep, all right, cool, thanks.