Home My Page Projects Dose: library and tools
Summary Activity Tracker Lists SCM Files

[#20984] Memory explosion on Algo.Depsolver.univcheck

Date:
2016-11-16 11:20
Priority:
3
State:
Open
Submitted by:
Louis Gesbert (altgr)
Assigned to:
Pietro Abate (abate)
Summary:
Memory explosion on Algo.Depsolver.univcheck

Detailed description
On some universes, it seems `univcheck` gets in an allocation loop, eating above 16G of RAM in a few seconds (and usually dying of OOM).

# How to reproduce

Note: first define a sensible ulimit before reproducing if you don't want to swap-freeze your machine! E.g. `ulimit -v 1000000` should make you safe.

The attached cudf file should be enough to reproduce: from the corresponding universe, run `Algo.Depsolver.univcheck`. A pef version and OCaml script to load the universe using opam-lib are also attached if that doesn't work.

The original case happened on dose3 5.0.1, and with the universe corresponding to opam-repository at commit ec4e5a296933f933cbfda3a1bb26d9d11e3b598d (https://github.com/ocaml/opam-repository/pull/7807/commits/ec4e5a296933f933cbfda3a1bb26d9d11e3b598d ; to which the cudf and pef files should correspond).

The attached OCaml script contains details and instructions to reproduce from the opam repository using opam-lib.

# Workaround

Setting `~explain:false` avoids the problem, so I temporarily switched to a modified version of `Depsolver.trim` that passes this option to `univcheck` in opam.

This may point to an issue with a high polynomial or exponential growth of the size of the explanations.
Message  ↓
Date: 2016-11-16 19:54
Sender: Roberto Di Cosmo

As a side remark, just a word of warning: package installability is equivalent to SAT solving, which is an NP-complete problem in general, so there are indeed universes that will make the solver explode, there is no way out.

As a rule of thumb, the more conflict and disjunctions are in the universe, the more likely is to get an explosion.

Attachments:
Size Name Date By Download
1.19 MiBboom.cudf2016-11-16 11:20altgrboom.cudf
1 KiBboom.ml2016-11-16 11:20altgrboom.ml
1.37 MiBboom.pef2016-11-16 11:20altgrboom.pef
Field Old Value Date By
File Added5899: boom.cudf2016-11-16 11:20altgr
File Added5900: boom.ml2016-11-16 11:20altgr
File Added5901: boom.pef2016-11-16 11:20altgr