Spinroot

A forum for Spin users

You are not logged in.

#1 2018-09-11 16:20:32

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Optimally configuring hash-compact method

Hi,

I would like to configure Spin so that it uses hash-compact with 14GB without running out of memory.

Unfortunately, playing with the -DHC makes no difference, case 1 with -DHC0 and case 2 with -DHC4 yield the same out of memory (see below).

So: Is this a bug or do I have to additionaly modify some other options? Which ones?


Thanks,
David


Case 1)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC0 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth=     753 States=    1e+06 Transitions= 1.01e+06 Memory=   166.672    t=     0.94 R=   1e+06
....
Depth=     813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660    t=      661 R=   5e+05
pan: reached -DMEMLIM bound
    1.47324e+10 bytes used
    102400 bytes more needed
    1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts:  77109092 (resolved)

Stats on memory usage (in Megabytes):
78944.851    equivalent memory usage for states (stored*(State-vector + overhead))
12002.095    actual memory usage for states (compression: 15.20%)
             state-vector as stored = 14 byte + 28 byte overhead
2048.000    memory used for hash table (-w28)
    0.054    memory used for DFS stack (-m1000)
14049.914    total actual memory usage


Case 2)
gcc -DMEMLIM=14050 -DSAFETY -DNOCLAIM -DXUSAFE -DHC4 -w -o pan pan.c; ./pan -m1000 -E -n -c1
Depth=     753 States=    1e+06 Transitions= 1.01e+06 Memory=   166.672    t=     1.12 R=   9e+05
...
Depth=     813 States= 2.99e+08 Transitions= 3.17e+08 Memory= 14014.660    t=      596 R=   5e+05
pan: reached -DMEMLIM bound
    1.47324e+10 bytes used
    102400 bytes more needed
    1.47325e+10 bytes limit
...
State-vector 248 byte, depth reached 813, errors: 0
2.9992636e+08 states, stored
18053505 states, matched
3.1797987e+08 transitions (= stored+matched)
4.6789036e+08 atomic steps
hash conflicts:  77109092 (resolved)

Stats on memory usage (in Megabytes):
78944.851    equivalent memory usage for states (stored*(State-vector + overhead))
12002.095    actual memory usage for states (compression: 15.20%)
             state-vector as stored = 14 byte + 28 byte overhead
2048.000    memory used for hash table (-w28)
    0.054    memory used for DFS stack (-m1000)
14049.914    total actual memory usage

Offline

#2 2018-09-25 18:15:17

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Optimally configuring hash-compact method

Yes, that is confusing at best -- or misleading really.
There is actually only one hashcompact mode -- all others (HC0, HC1, and HC3) map to the behavior of HC4.
I should document that somewhere in the manpages, sorry!

Offline

#3 2018-10-05 08:12:57

DavidFarago
Member
Registered: 2011-10-17
Posts: 21

Re: Optimally configuring hash-compact method

Thanks for the clarification.

Too bad -DHC0 does not have the effect as described in the spin book, since I have a huge state space and only 14GB of memory available. Thus using 32bit values would be a good approach in spite of the higher collision risk.

So is there a possibility to do this?

Offline

#4 2018-10-06 18:21:26

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Optimally configuring hash-compact method

Bitstate would be a good alternative.
I'll see if I can resurrect the HC0..3 modes in the next update.

Offline

Board footer

Powered by FluxBB