lps2lts --cached fails for some examples in the performance measurements

[jgroote]

Issue migrated from trac ticket # 1012

component: lps2lts | priority: major | resolution: fixed

2012-04-10 10:51:31: @jkeiren created the issue

---

State space generation fails using lps2lts -rjittyc --cached spec.lps with an exit code of 1 in the performance measurements of a number of specifications (see http://www.mcrl2.org/performance). The lps is generated using the following command:

mcrl22lps -fD spec.mcrl2  | lpsconstelm | lpsparelm | lpssuminst > spec.lps

lps2lts fails for the following specifications:

1394-fin
brp
chatbox
clobber
lift3-final
lift3-init
othello

For domineering the same command fails with exit status 6.

[jgroote]

2012-04-10 13:40:56: @jkeiren changed status from new to assigned

[jgroote]

2012-04-10 13:40:56: @jkeiren changed owner from jkeiren to jfg

[jgroote]

2012-04-10 13:40:56: @jkeiren commented

---

For the cases with the exit status 1, the expected cause is the process using > 1GB of main memory, which exceeds the memory limit of the performance measurements.

To reproduce on Linux (for roughly 1GB of main memory):

ulimit -v 1000000
lps2lts -vrjittyc 1394-fin.lps

It seems this is related to the changes to the ATerm library.

[jgroote]

2012-04-10 13:42:18: @jkeiren edited the issue description

[jgroote]

2012-04-11 08:02:11: @jkeiren commented

---

The issues that were present without caching have been resolved. With caching, the exit status 1 still occurs with r10471. To reproduce:

ulimit -v 1000000
lps2lts -vrjittyc --cached 1394-fin.lps

[jgroote]

2012-04-12 08:04:42: @jkeiren commented

---

All cases that failed with exit status 1 have been resolved in r10475. The remaining issues are the following:

Executing: lps2lts -rjittyc --cached ./cases/clobber.lps
  Recording Time
  Recording Memory
  Time limit is: 300 seconds
  Execution FAILED with code 6 

Executing: lps2lts -rjittyc --cached ./cases/domineering.lps
  Recording Time
  Recording Memory
  Time limit is: 300 seconds
  Execution FAILED with code 6

[jgroote]

2012-04-12 08:52:23: @jkeiren changed owner from jfg to jkeiren

[jgroote]

2012-04-12 08:52:23: @jkeiren commented

---

The problem seems to be caused by a large memory footprint when caching is enabled. On my system, for clobber, the memory usage exceeds 2.5GB (and I have not generated the state space completely).

[jgroote]

2012-04-22 16:14:25: @jkeiren changed status from assigned to closed

[jgroote]

2012-04-22 16:14:25: @jkeiren set resolution to fixed

[jgroote]

2012-04-22 16:14:25: @jkeiren commented

---

For the moment, I consider the issue resolved. Some experimentation should be done with the different optimisation techniques.