Humongous amounts of memory needed to parse large models

[pranavashok]

We are trying develop some new algorithms for CTMDP reachability in PRISM and are facing some major issues with the parsing of large models. As discussed in issue #27, I had made just a few modifications in order to input CTMDPs in the same format as MDPs.

The amount of memory PRISM needs to parse a model of size 160MB exceeds 25GB. I was wondering why this happens, and why parsing is so slow (took around 6-7 minutes with 52 threads, not all running simultaneously). Would there be any relatively simple way to get around this limitation? In comparison, IMCA is able to solve this CTMDP in around the same time.

My first thoughts were to use the explicit format (tra). I assumed that the ModulesFile object coming out of parsing the explicit format can be used to instantiate a ModelGenerator in the same way as earlier, but it doesn't seem to be the case. The ModelGenerator object doesn't populate the transition list at all (on calling getTransitionList). I wonder if I am doing something wrong here.

Any hints or thoughts on how to proceed would be appreciated.

[kleinj]

Hi,

The amount of memory PRISM needs to parse a model of size 154MB exceeds 25GB. I was wondering why this happens, and why parsing is so slow (took around 6-7 minutes with 52 threads, not all running simultaneously).

We had problems with such large models before as well. It would be useful to see with a profiler where the time is actually spent. Some time ago, I had started on refactoring some parts of the parse tree analysis; there, some things rely on looking up variable/constant/... names in Vectors using indexOf(), which can lead to quadratic complexity. I wanted to replace those vectors by a combined array list + hash map to allow efficient lookup by index and finding the index via the entry itself. That might be your bottleneck, but it might also be something else.

BTW, depending on your configuration (if you allow a huge heap), it might be the case that the use of 25GB of RAM arises because garbage collection is not called, as there is no memory pressure. This is something that we've seen in practice before.

My first thoughts were to use the explicit format (tra). I assumed that the ModulesFile object coming out of parsing the explicit format can be used to instantiate a ModelGenerator in the same way as earlier, but it doesn't seem to be the case. The ModelGenerator object doesn't populate the transition list at all (on calling getTransitionList).

If I remember correctly, the ModulesFile generated for explicit import is just a minimal scaffolding to provide other parts of PRISM the required meta-data (pseudo variable name, ...).

The actual model building (you are using the explicit engine, right?) is triggered at

prism/prism/src/prism/Prism.java

Line 2021 in 072e0c7

currentModelExpl = new ExplicitFiles2Model(this).build(explicitFilesStatesFile, explicitFilesTransFile, explicitFilesLabelsFile, currentModulesFile, explicitFilesNumStates);

I think you could just add a case for CTMDPs like that for MDPs here

prism/prism/src/explicit/ExplicitFiles2Model.java

Lines 107 to 117 in 072e0c7

	case MDP:
	MDPSimple mdp = new MDPSimple();
	mdp.buildFromPrismExplicit(transFile.getAbsolutePath());
	model = mdp;
	break;
	case CTMDP:
	case LTS:
	case PTA:
	case SMG:
	case STPG:
	throw new PrismNotSupportedException("Currently, importing " + modulesFile.getModelType() + " is not supported");

as a CTMDPSimple inherits the import functionality from MDPSimple, and there are currently no sanity checks for the probabilities on import.

[davexparker]

Yes, agreed with @kleinj.

On the first issue (slow parsing), if you could send us an example of the model file, that would be very helpful for debugging/profiling purposes.

On the second issue (.tra files), the proposed modification should definitely allow import from files more efficiently.

[pranavashok]

Thanks for the really quick answers @kleinj and @davexparker

Here is a link to 3 models of increasing size. I was trying to run on the largest one out of those. I shall try to do some profiling myself and post the findings here. Meanwhile you may also have a look.

Regarding the second issue, like @kleinj has pointed out, I did notice that the ModulesFile is just a scaffolding. Just to make things clear, I would like to emphasize that we are trying to use ModelGenerator as our window into the actual model. This means that the model is never explicitly built. Just to make sure, I checked if my working code calls the doBuildModel() of the Prism class -- and the answer is no.

What currently happens in my code is as follows. The run() method calls doParsing() which seems to create this "scaffolding" ModulesFile object. Then modelCheck() is called, which initializes my CTMDP ModelChecker. inside this, I use

ModelGenerator model = new ModulesFileModelGenerator(modulesFile, this);

which from now on will be the only way I'm going to access the model.

This way of accessing the model works perfectly when the input is in PRISM language. But when I use explicit input, suddenly things don't work. Should one do something more in order to access the model using ModelGenerator?

[kleinj]

Hi,

thanks for the models. I did a bit of profiling using the medium sized one to get some first impression. It looks like quite a lot of time is spent allocating memory structures during parsing, which is not that unexpected. It's clear that storing the parse tree with all the annotated information (location in the source code, ...) will have quite a bit of overhead compared to the plain source code size. Afterwards, during the tidyUp and instantiation preparations, quite a bit of time is spent doing deepCopy of the ModulesFile, which essentially has to do a complete copy of the parse tree. Unfortunately, there wasn't anything that immediately looked like an easy fix.

If there is a lot of memory pressure, garbage collection can lead to additional extreme slow downs, we have seen situations where 99% of the time is spent doing garbage collection.

For the ModelGenerator stuff: Normally, if you have the explicit files, you'd skip the model generation as you can directly build the model. But in principle, you could code a ModelGenerator that is "backed" by an already constructed explicit model. So, you'd build the explicit model and than wrap some ModelGenerator instance around that for your code. That way you would only have to code your extension against the ModelGenerator interface. Or you add support for handling an explicit CTMDP directly...

[pranavashok]

Unfortunately, there wasn't anything that immediately looked like an easy fix.

That's bad news! Thanks a lot for the effort.

For the ModelGenerator stuff: Normally, if you have the explicit files, you'd skip the model generation as you can directly build the model. But in principle, you could code a ModelGenerator that is "backed" by an already constructed explicit model. So, you'd build the explicit model and than wrap some ModelGenerator instance around that for your code. That way you would only have to code your extension against the ModelGenerator interface. Or you add support for handling an explicit CTMDP directly...

Right. I think I get your point. Since our code is built to work with this "grey-box" like system, I think it makes sense to wrap the constructed model with the ModelGenerator. I'll try and see what happens when I call doBuildModel() with the additions you suggested earlier.

[pranavashok]

Hi, just an update.

I was able to use the buildModel() which only takes ~6 seconds to run. With this, the second part of the issue I raised stands resolved. Thanks a lot for the suggestions.

The first part is still at large.

[merkste]

I am curios, does your model contain a lot of formulas?

I am asking, since I experienced a huge performance hit with those kinds of models. It turned out that this was due to a huge amount of duplicate nodes generated during AST modifications: Replacing references to formulas and constants and such turns the AST into a DAG. In general, you want to keep that structure, since it it compact. However, the current implementation of deepCopy unfolds it to a tree, which can cause an exponential blowup in the number of nodes.

I do have a modification that solves this problem, but it is not ready for a PR, since it is based on an older Prism version. But if you are interested, I could still provide you the code.

[pranavashok]

Hi @merkste, no the model didn't contain a lot of formulas. Your finding is quite interesting nevertheless. I'm also on an older codebase and would like to try out your code and see if it makes any changes to my use case.

[merkste]

Hi @pranavashok, after some clean-ups I'll push a branch to my github repository.

[merkste]

Hi @pranavashok , I've just pushed a branch to my fork of prism: DAG-aware-copying. It's not quite ready for a pull request, but all tests pass. Please have a look. I'd be happy to hear a) whether it works for you and b) whether you have comments on the solution.

[merkste]

Hi, I've cleaned up the code and created a PR: #66 .