Spinroot

memin

Member

Registered: 2014-11-02

Posts: 3

Consume all existing memory

Dear all, I have memory consumption problem when verifying ltl properties.
My computer configuration is : Windows 7 professional 64 bit, Intel core i7-2600 CPU @3.40 GHz, 3,40GHz.  Installed memory 16GB RAM.
I am using spin 32 bit and when I run ltl verification, spin produces following output. It consumes [b]only 2003.894 [/b] MB memory. My question is, why spin does not try to consume all memory as I specified with “-DMEMLIM=12288” parameter.  Is there an upper memory limit that spin can use?
I just want to use all my memory and try to see spin can verify the property. (P.S. I do not want to use collapse compression or bitstate).
I really need to sort out that problem.  Any help will be much appreciated.

spin -a  pulseGen1x1.pml
ltl prop1: ! ([] ((c[0].x[proteinGFP_]==0)))
gcc -DMEMLIM=12288 -O2 -DXUSAFE -w -o pan pan.c
./pan -m10000  -a -c0
Pid: 4792
pan:1: acceptance cycle (at depth 310)
Depth=     320 States=   1e+006 Transitions= 4.59e+006 Memory=   390.027	t=     6.49 R=  2e+005
Depth=     320 States=   2e+006 Transitions= 9.96e+006 Memory=   715.613	t=     14.2 R=  1e+005
Depth=     320 States=   3e+006 Transitions= 1.56e+007 Memory=  1041.199	t=     22.2 R=  1e+005
Depth=     323 States=   4e+006 Transitions= 2.16e+007 Memory=  1366.687	t=     30.8 R=  1e+005
Depth=     323 States=   5e+006 Transitions= 2.78e+007 Memory=  1692.273	t=     39.7 R=  1e+005
pan: out of memory
	2.10124e+009 bytes used
	102400 bytes more needed
	1.28849e+010 bytes limit
hint: to reduce memory, recompile with
  -DCOLLAPSE # good, fast compression, or
  -DMA=672   # better/slower compression, or
  -DHC # hash-compaction, approximation
  -DBITSTATE # supertrace, approximation

(Spin Version 6.2.5 -- 3 May 2013)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (prop1)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 672 byte, depth reached 323, errors: 2684616
  2978585 states, stored (5.95713e+006 visited)
 27969153 states, matched
 33926282 transitions (= visited+matched)
1.4052565e+008 atomic steps
hash conflicts:   1495812 (resolved)

Stats on memory usage (in Megabytes):
 1954.333	equivalent memory usage for states (stored*(State-vector + overhead))
 1946.315	actual memory usage for states (compression: 99.59%)
         	state-vector as stored = 669 byte + 16 byte overhead
   64.000	memory used for hash table (-w24)
    0.343	memory used for DFS stack (-m10000)
    6.780	memory lost to fragmentation
 2003.894	total actual memory usage

pan: elapsed time 48.6 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"

memin

Member

Registered: 2014-11-02

Posts: 3

Re: Consume all existing memory

Heeelllppp!!!

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Consume all existing memory

If you're using the 32-bit version of Spin, then the maximum amount of memory you can use is 2 GB (simply because a 32-bit application cannot address more memory than that on Windows).  To be able to use more memory, you'll have to use a 64-bit version of Spin.
You can find a precompiled version at: http://spinroot.com/spin/Bin/

memin

Member

Registered: 2014-11-02

Posts: 3

Re: Consume all existing memory

Thank you so much. Yes it was the reason. I had to 64-bit gcc compiler and Spin-64.