Spinroot

abet

Member

Registered: 2014-02-28

Posts: 14

How to use -DMA option

Hello,

I am Tatsuya, a Spin user.  Now I am wondering how to use the
-DMA option.  I would be glad to hear how to use it.

I am trying to verify large Promela codes.  To decrease memory
sizes to be consumed by Spin, I started to use the -DMA option
while I have used the -DCOLLAPSE option only.

For some small Promela codes, it seeems that I succeeded in using
the -DMA option correctly as follows:

$ gcc -O0 -w -g -DVECTORSZ=5678 -DMEMLIM=6144 -DMA=98765 -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Graph Encoding (-DMA=98765)
...
State-vector 4708 byte, depth reached 2263, errors: 0
MA stats: -DMA=4578 is sufficient
Minimized Automaton:    151982 nodes and 272208 edges
      257 states, stored
      176 states, matched
      433 transitions (= stored+matched)
    49062 atomic steps

cf.
$ gcc -O0 -w -g -DVECTORSZ=5678 -DMEMLIM=6144 -DCOLLAPSE -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Compression
...
State-vector 4708 byte, depth reached 2263, errors: 0
      254 states, stored
      170 states, matched
      424 transitions (= stored+matched)
    49062 atomic steps
hash conflicts:         0 (resolved)

However, for a large Promela code, it seems that I failed to run
Spin correctly as follows:

$ gcc -O0 -w -g -mcmodel=large -DVECTORSZ=521098 -DMEMLIM=131900 -DMA=429531 -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Graph Encoding (-DMA=429531)
...
State-vector 419644 byte, depth reached 0, errors: 0
MA stats: -DMA=419531 is sufficient
Minimized Automaton:     72631 nodes and 108947 edges
        1 states, stored
        1 states, matched
        2 transitions (= stored+matched)
        0 atomic steps

Stats on memory usage (in Megabytes):
    0.400       equivalent memory usage for states (stored*(State-vector + overhead))
   99.287       actual memory usage for states
   26.703       memory used for DFS stack (-m500000)
  125.990       total actual memory usage

cf.
$ gcc -O0 -w -g -mcmodel=large -DVECTORSZ=521098 -DMEMLIM=131900 -DCOLLAPSE -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Compression
...
State-vector 419660 byte, depth reached 174976, errors: 0
    87594 states, stored
    94087 states, matched
   181681 transitions (= stored+matched)
2.3812352e+08 atomic steps
hash conflicts:       351 (resolved)

Stats on memory usage (in Megabytes):
35059.787       equivalent memory usage for states (stored*(State-vector + overhead))
32761.915       actual memory usage for states (compression: 93.45%)
                state-vector as stored = 392152 byte + 36 byte overhead
  128.000       memory used for hash table (-w24)
   26.703       memory used for DFS stack (-m500000)
  185.697       memory lost to fragmentation
32759.338       total actual memory usage

I cannot find any error/warning message that Spin returns.
Could you give me any help?

Best,
Tatsuya

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: How to use -DMA option

That is mysterious. It is a seriously large model, with a statevector of almost half a megabyte, but it should still work.
Would it be possible to send a version of this model, so that I can check what happens in this case?
You can also try to see why it stops after one state by compiling with -DVERBOSE and check the output of the run.

abet

Member

Registered: 2014-02-28

Posts: 14

Re: How to use -DMA option

Thank you so much for the quick response, information, and
proposal to check my code.

After I submitted my question to the forum, I tried to find the
smallest in my codes that raises the same trouble.

I found such a small code (code size: 53KiB, lines: 1219,
state-vector: 3KiB).

I.
>You can also try to see why it stops after one state by
>compiling with -DVERBOSE and check the output of the run.

I applied it (compiling with -DVERBOSE) to the small code.
A result is as follows.  Any suggestion is welcome.

$ gcc -O0 -w -g -mcmodel=large -DVERBOSE -DVECTORSZ=45678 -DMEMLIM=6144 -DMA=3408748 -DSAFETY -o sequential_tso_diff_Sequential.exe sequential_tso_diff_Sequential_guards.c sequential_tso_diff_Sequential_asserts.c pan.c
...
0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 188
  0: proc 0 exec 188, 1 to 2, x_at_0_on_0 = 0   non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
on-stack
1: Up - program
  1: proc 0 reverses 188, 1 to 2
        x_at_0_on_0 = 0 [abit=0,adepth=0,tau=0,0]
0: zapping
old state

(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Graph Encoding (-DMA=3408748)
        + FullStack Matching

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +

State-vector 3356 byte, depth reached 0, errors: 0
MA stats: -DMA=3238 is sufficient
Minimized Automaton:      1753 nodes and   2629 edges
        1 states, stored
        1 states, matched
        0 matches within stack
        2 transitions (= stored+matched)
        0 atomic steps
stackframes: 0/0

stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
Stats on memory usage (in Megabytes):
    0.003       equivalent memory usage for states (stored*(State-vector + overhead))
    4.356       actual memory usage for states
  106.812       memory used for DFS stack (-m2000000)
  111.168       total actual memory usage

cf. decrease size of -DMA
$ gcc -O0 -w -g -mcmodel=large -DVERBOSE -DVECTORSZ=45678 -DMEMLIM=6144 -DMA=98765 -DSAFETY -o sequential_tso_diff_Sequential.exe sequential_tso_diff_Sequential_guards.c sequential_tso_diff_Sequential_asserts.c pan.c
...
0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 188
  0: proc 0 exec 188, 1 to 2, x_at_0_on_0 = 0   non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 189
  1: proc 0 exec 189, 2 to 3, mem_at_0_on_0[x_at_0_on_0] = 0   non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 190
  2: proc 0 exec 190, 3 to 4, x_at_1_on_0 = 0   non-accepting [tau=0]

...(167266 lines)...

468: Down - program non-accepting [pids 1-1]
Pr: 1 Tr: 107
468: proc 1 exec 107, 171 to 1162, kind_counter = 0   non-accepting [tau=8]
469: Down - program non-accepting [pids 2-0]
on-stack
469: Up - program
469: proc 1 reverses 107, 171 to 1162
    kind_counter = 0 [abit=0,adepth=0,tau=0,8]
468: Up - program
468: proc 1 reverses 2, 173 to 171
    else [abit=0,adepth=0,tau=8,8]

...(167265 lines)...

3: zapping
old state
3: Up - program
  3: proc 0 reverses 190, 3 to 4
        x_at_1_on_0 = 0 [abit=0,adepth=0,tau=64,64]
2: zapping
old state
2: Up - program
  2: proc 0 reverses 189, 2 to 3
        mem_at_0_on_0[x_at_0_on_0] = 0 [abit=0,adepth=0,tau=64,64]
1: zapping
old state
1: Up - program
  1: proc 0 reverses 188, 1 to 2
        x_at_0_on_0 = 0 [abit=0,adepth=0,tau=64,64]
0: zapping
old state

(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Graph Encoding (-DMA=98765)
        + FullStack Matching

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +

State-vector 3372 byte, depth reached 2262, errors: 0
MA stats: -DMA=3242 is sufficient
Minimized Automaton:    123986 nodes and 216099 edges
      255 states, stored
      174 states, matched
        0 matches within stack
      429 transitions (= stored+matched)
    49062 atomic steps
stackframes: 3/12

stats: fa 0, fh 0, zh 0, zn 0 - check 10 holds 6
stack stats: puts 0, probes 0, zaps 0
Stats on memory usage (in Megabytes):
    0.829       equivalent memory usage for states (stored*(State-vector + overhead))
   81.942       actual memory usage for states
  106.812       memory used for DFS stack (-m2000000)
    4.019       memory lost to fragmentation
  184.783       total actual memory usage

II.
>Would it be possible to send a version of this model, so that I
>can check what happens in this case?

Sure.  My code (the small code that raises the same problem) is public.
The code is generated by my open-source tool McSPIN.
https://bitbucket.org/abet/mcspin/

How should I send the code?
i. Should I simply send a set of codes (and a tiny shell script to run Spin)?
   The code is generated, but I guess that it is not impossible to be read.
   Can I attach it with a reply on this forum? (although I do not know how to do)
ii. Or, should I send an instruction to start to use my tool McSPIN?
    I guess that it is not better since installation of some softwares
    (GHC, GHC libraries, etc.) are required.

Best,
Tatsuya

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: How to use -DMA option

That is interesting -- I do notice that you link the pan.c with external code, which probably means that you're using c_code and/or c_expr statements. That makes it possible that the bug is elsewhere, e.g. when not all relevant state is tracked with c_track statements.
On the other hand -- the state match after a single step could point in a different direction -- as does the change in behavior when the size of -DMA changes.
The size of the state-vector shouldn't matter, but I don't think this has ever been tested to this extreme. The could well be some overflow condition somewhere in the MA code.  I wrote this part in 1997, so it's been 18 years. Somewhat lowers my confidence that I still understand that code!

abet

Member

Registered: 2014-02-28

Posts: 14

Re: How to use -DMA option

Thank you so much for the detailed explanation.
As you completely understand,

1. I use c_code {...} and c_expr {...}, and
2. I designate too large MA size.

I am afraid if my experiments (under overflow condition) would be
stresses to Spin.  I try to re-consider design of my tool
(to return better Promela codes).

At the end of the post, let me explain why I did the above 1 and 2.
I would be glad if they are useful to development of Spin.

Thank you,
Tatsuya

1.
My tool generates Promela codes that contain a large size of
guards (for if/do statements).  Spin translates the Promela codes
into C codes.  However, it seems that GCC is not good at
compiling the C codes, and GCC requires much time (e.g., two hours)
to compile the C codes.

Therefore, I brushed up my tool.  My tool generates C codes that
contain functions corresponding to the guards, and generated
Promela codes that call the functions written in C.

To include the C codes, my tool writes c_code {...} in Promela
codes.  To call the functions in the C codes, my tool writes
c_expr {...} in Promela codes.

GCC can compile the C codes into which Spin translates the
Promela code with c_expr {...}, compile the C codes that
contain functions corresponding to the guards, and link them in a
few minutes.  Results of verifications (for a test suite that I
developed) are exactly the same.

2.
In my previous post, it sounds that not size of Promela code but
size of MA (that I designated) raises the trouble.

Let me explain why I designated too large MA while the small
code (53KiB) can be correctly verified under -DMA=98765.

The original code that I would like to verify is so large (around
6MiB).  When I first tried to check the code as follows:

$ spin -a a_Sequential.pml
$ gcc -O0 -w -g -DVERBOSE -DVECTORSZ=645678 -DMEMLIM=6144 -DMA=500000 -DSAFETY -o a_Sequential.exe a_Sequential_guards.c a_Sequential_asserts.c pan.c
...

Spin returned the following:
0: Down - program non-accepting [pids 0-0]
pan: error, MA too small, recompile pan.c with -DMA=N with N>511925
pan:1: aborting (at depth 0)
pan: wrote a_Sequential.pml.trail
...

Therefore, I executed the following command:

$ spin -a a_Sequential.pml
$ gcc -O0 -w -g -DVERBOSE -DVECTORSZ=645678 -DMEMLIM=6144 -DMA=511926 -DSAFETY -o a_Sequential.exe a_Sequential_guards.c a_Sequential_asserts.c pan.c

and found the trouble since Spin returned the following:

0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 2239
  0: proc 0 exec 2239, 1 to 2, hs_req_at_0_on_0 = 0   non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
on-stack
1: Up - program
  1: proc 0 reverses 2239, 1 to 2
        hs_req_at_0_on_0 = 0 [abit=0,adepth=0,tau=0,0]
0: zapping
old state

(Spin Version 6.4.4 -- 1 November 2015)
        + Partial Order Reduction
        + Graph Encoding (-DMA=511926)
        + FullStack Matching

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +

State-vector 512044 byte, depth reached 0, errors: 0
Minimized Automaton:    106349 nodes and 159524 edges
        1 states, stored
        1 states, matched
        0 matches within stack
        2 transitions (= stored+matched)
        0 atomic steps
stackframes: 0/0
...