ymandel marked 3 inline comments as done. ymandel added a comment. In D152732#4415168 <https://reviews.llvm.org/D152732#4415168>, @mboehme wrote:
> In D152732#4414707 <https://reviews.llvm.org/D152732#4414707>, @ymandel wrote: > >> In D152732#4414661 <https://reviews.llvm.org/D152732#4414661>, @xazax.hun >> wrote: >> >>> Huge +1, I think most solvers need to have some resource limits in place as >>> the runtime can explode. I am just not 100% what is the best approach here, >>> putting a global limit on the solver instance vs having a limit per query. >>> Any thoughts on that? >> >> Excellent question. Ultimately what matters for a user is the global limit. >> So, in that sense, a global limit makes sense. But, it also makes it harder >> (in principle) to pinpoint the problem, because you could have it timeout on >> a small query right after a large query that was actually responsible for >> consuming the resources. That said, I'm guessing in practice it's binary, >> because of the exponential: either a single call exhausts all resources or >> it barely uses them. I suspect we'll ~never hit the case I described. So, >> I'm inclined to start global (to keep it simple) and then refine if >> necessary. As you probably noticed, this patch actually has both -- the user >> specifies the global limit, but the implementation is local. So, changing >> this would be easy. > > I'm a bit late to this discussion but still wanted to chime in. At a high level, I really don't care much -- I just want one mechanism that works well enough. With that said, here are my (weak) arguments in favor of global vs local. If you feel strongly though, feel free to push back and I'll change it (I have some small things to fix anyhow based on Dmitri's comments) or even just send a patch. > I would actually argue that a local limit more accurately reflects what we > want to limit. The functions we analyze will be distributed across a fairly > broad range of size and complexity. It seems reasonable to allow more > resources to be used to analyze a large and complex function than a small and > simple function, and I think this is aligned with users' expectations. So I > think it would be reasonable to allow the analysis to use an amount of > resources that's proportional to the number of `solve()` invocations; we just > want to limit the amount of resources consumed in a given `solve()` > invocation. I agree about resource usage, but this is about a ceiling. Like timeouts that we place on our clang-tidy invocations and elsewhere, we're looking for a cap. This lets you cap the total, regardless of size. If you want to account for larger functions, just set the cap higher. I'd say that a local mechanism, then, is basically a way to be more restrictive on smaller functions, which begs the question of: what is the particular benefit? > I do follow your argument that "local versus global" likely won't make much > of a difference in practice -- the number of `solve()` invocations is > polynomial in the size of the function (I believe?), and that pales against > the exponential blowup that can potentially occur inside `solve()`. Yeah, that's the key and drives the decision here. > However, I don't follow the argument that you want to "start global (to keep > it simple)". I think a "local" limit would be simpler: > `WatchedLiteralsSolverImpl::solve()` wouldn't need to return the final value > of its parameter `MaxIterations`, and `WatchedLiteralsSolver::solve()` > wouldn't need to write that back into its member variable `MaxIterations` > (which would instead be `const`). True - the code would be simpler and maybe we should just go by this. What I meant is that it is simpler in terms of tuning, since the user is setting the cap for the function. I find the predictability of a total cap simpler to reason about. > I don't think, in any case, that we should have a global _and_ a local limit > -- that would really be overcomplicating things. I actually think you just made the case for both: these accomplish different things. So, if it turns out we want both global caps (for catastrophes) and function-proportional limits, then two limits make sense. It doesn't make sense at the outset for sure -- just if we need, at which point by definition we need it. :) ================ Comment at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:37 + // measurements like CPU cycles or time to ensure deterministic results. + std::int64_t MaxIterations = std::numeric_limits<std::int64_t>::max(); + ---------------- gribozavr2 wrote: > Consider renaming to `RemainingWorkUnits` I like that. Will do in followup. ================ Comment at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:42 + + // `Work` specifies a computational limit on the solver. Units of "work" + // roughly correspond to attempts to assign a value to a single ---------------- gribozavr2 wrote: > ack (for followup patch). ================ Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:462 + // Returns the `Result` and the number of iterations "remaining" from + // `MaxIterations` (that is, `MaxIterations` - iterations in this call). + std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && { ---------------- gribozavr2 wrote: > Why not add a separate getter for the remaining work amount? It's a different object -- `WatchedLiteralsSolverImpl` (here) vs `WatchedLiteralsSolver` (where the field `MaxIterations` is located). ================ Comment at: clang/unittests/Analysis/FlowSensitive/SolverTest.cpp:378 + // A ^ B + EXPECT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut); +} ---------------- mboehme wrote: > Do we really need such a complex formula to test this? Couldn't we make the > formula simpler (can we get as simple as "a && !a"?) and reduce the maximum > number of iterations accordingly so we still get a timeout? No, I simply copied this from elsewhere. I just wanted an example that had a non trivial number of variables. I think its worth commenting that it's an arbitrary choice, but I don't seen particular value in trying to fine tune this for simplicity. But, if you have some argument for it, by all means. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D152732/new/ https://reviews.llvm.org/D152732 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
