Spinroot

A forum for Spin users

You are not logged in.

#1 2012-06-08 11:22:15

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Compacter data structure causes larger state-vector

I wrote a Promela script to solve Sodukus.  The first version uses a byte to represent a table entry, so the table takes 9 X 9 = 81 bytes and this is the major part of the state-vector in the SPIN solver.  Then I thought that 1 byte for 1 entry was too wasteful because the value at each entry is smaller than 10 and took only 4 bits.  Accordingly I improved my script to put 2 entries into 1 byte; thus the table size is reduced to 9 X 5 = 45 bytes, almost half of the first version.  The code is then slightly more complex because I have to work on 4 bits on the byte.

I expect a reduction in the size of the state-vector and the total memory usage, but was really surprised by the outcome.

For the first version of 81 byte table, the state-vector is 112 bytes and the total actual memory usage is 64.391 M

For the second version of 45 byte table, the state-vector is 204 bytes and the total actual memory usage is 64.684 M

Do you feel this comparison strange?  What could be the cause for the larger state-vector produced by the compacter data structure?

I can send you the code if you want to have a closer look.  Thanks for your comments!

BR

Offline

#2 2012-06-09 18:45:39

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

Re: Compacter data structure causes larger state-vector

Not strange, but it is interesting. Note that you don't really have direct control over how the compiler represents the data structures -- Spin also performs some intermediate steps and could well be representing the 4-bit quantities as 1-byte quantities.
If you show the code I can do a more detailed comparison to see what's different between the two versions at the pan.c and pan.h level.
You can also take a look yourself by looking at which datastructures are generated (typically these are called struct P0 { ... } and struct P1 {...} for the proctypes in pan.h, and struct State { ... }, for the global state vector.

Offline

#3 2012-06-09 22:54:28

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Compacter data structure causes larger state-vector

I followed your hint and peeked inside pan.h.  I found the problem with my compact data structure.  With the compact data structure, I have to map a 9 X 9 table into a 9 X 5 matrix.  To simplify the code, I wrote two inline functions to manage the mapping.  Some "local" variables are defined inside the inline functions.  These variables are really the problem.  I realized that inline functions are just macros and then all variables defined inside the inline functions create new variables defined in the process.  Because the inline functions are called about 100 times, the same variables are then repetitively defined 100 times in "struct P0" in pan.h. 

I corrected this problem by declaring all variables outside the inline functions. Then I got a better comparison.

For the first version of 81 byte table, the state-vector is 112 bytes and the total actual memory usage is 64.391 M

For the second version of 45 byte table, the state-vector is 100 bytes and the total actual memory usage is 64.391 M

The compact data structure ends up with a small improvement in the state-vector size but no difference in the total actual memory usage.  The benefit of the compact data structure is really marginal.  I would appreciate your help if you can identify the problem with the compact data structure.  This may deepen my understanding on SPIN.

Offline

Board footer

Powered by FluxBB