DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
16 stars 2 forks source link

DeepSec uses too much memory #44

Open VincentCheval opened 4 years ago

VincentCheval commented 4 years ago

Large sets of constraint systems consume too much memory. Mostly due to the full renaming of names and variables.

In particular, that occurs when using the classic semantics on non-determinate processes.

VincentCheval commented 4 years ago

There were no bug in reality. However I manage to compact the memory size quite a lot (devided by 4 to 5 the memory consumption on some examples) by reworking the functions instantiate and instantiate_and_rename. These functions now guarantee that physical equality is preserved when there was nothing to instantiate or to rename. Moreover the names does not directly indicates whether they are deducible or not, i.e. we don't need to rename them anymore. (See 5f4dc84)

I also identified the main problem with the heavy consumption of memory : It's due to the generation of jobs. In some cases, a job can become heavy with something like 10M constraint systems. In itself it's fine for the workers when they evaluate the jobs since they don't store them. However, in generation phase, the workers store the jobs that they will send to the main process which is where the problem lies.

Possible solutions (not exclusive)