Spinroot

A forum for Spin users

You are not logged in.

#1 2012-04-19 13:08:28

Beth
Member
Registered: 2012-03-19
Posts: 11

Bitstate Hashing

Hi,

In the process of verifying my model(a security protocol), an exhaustive search was infeasible due to limitations in memory. I therefore resorted to using bitstate hashing since it faster and consumes less memory compared to the other optimization techniques currently supported by SPIN. Well, the verification output did not generate an error yet there was a huge list of unreachable code within the model. What does this exactly mean??was this verification effective??

Offline

#2 2012-04-20 05:10:17

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

Re: Bitstate Hashing

did you set the size of the hash-array as large as possible? (using the -w parameter to pan)
also: did you run on a 64-bit machine or a 32-bit machine?
32-bit machines are rather limited in the amount of memory they can address
i'd recommend running with the largest -w parameter possible, and then checking again how much was uncovered

Offline

#3 2012-04-23 09:18:59

Beth
Member
Registered: 2012-03-19
Posts: 11

Re: Bitstate Hashing

Hi again,

Well am working on a 32-bit laptop and i verified my model using -w32 as advised but the same "unreached code" popped up. I moved to a 64-bit laptop later on and used -w33 but the same problem persists from the .pml code(BS process) in my model and onwards. A snippet of the verification run is shown below:

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

State-vector 940 byte, depth reached 1612, errors: 0
2.7560651e+09 states, stored
8.7938966e+08 states, matched
3.6354548e+09 transitions (= stored+matched)
1.2513312e+08 atomic steps

hash factor: 3.11674 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
2512739.431     equivalent memory usage for states (stored*(State-vector + overh
ead))
1024.000       memory used for hash array (-w33)
    0.038       memory used for bit stack
    0.343       memory used for DFS stack (-m10000)
    1.092       other (proc and chan stacks)
1025.515       total actual memory usage

unreached in proctype BS
        ReMT2ndProtocol2.pml:233, state 7, "BSindex_i = 0"
        ReMT2ndProtocol2.pml:235, state 11, "BSindex_i = 2"
        ReMT2ndProtocol2.pml:236, state 13, "BSindex_i = 3"
        ReMT2ndProtocol2.pml:237, state 15, "BSindex_i = 4"
        ReMT2ndProtocol2.pml:248, state 50, "Nbs = (Nbs-20)"
        ReMT2ndProtocol2.pml:270, state 73, "BSCommit = -(1)"
        ReMT2ndProtocol2.pml:276, state 105, "PK_BS = (PK_BS-20)"
        ReMT2ndProtocol2.pml:277, state 115, "BSRunning = -(1)"
        (8 of 129 states)
unreached in proctype SS
        ReMT2ndProtocol2.pml:338, state 25, "SSTSSI = (SSTSSI-20)"
        ReMT2ndProtocol2.pml:360, state 47, "SSRunning = -(1)"
        ReMT2ndProtocol2.pml:368, state 105, "PN_index = (PN_index-20)"
        ReMT2ndProtocol2.pml:369, state 168, "PN_index = (PN_index-20)"
        ReMT2ndProtocol2.pml:370, state 203, "PK = (PK-20)"
        ReMT2ndProtocol2.pml:377, state 240, "Nss = (Nss-20)"
        ReMT2ndProtocol2.pml:409, state 272, "SSCommit = -(1)"
        ReMT2ndProtocol2.pml:410, state 278, "SSCommit = 1"
        ReMT2ndProtocol2.pml:410, state 280, "SSCommit = -(1)"
        ReMT2ndProtocol2.pml:410, state 283, "((0==Legit))"
        ReMT2ndProtocol2.pml:410, state 283, "else"
        (10 of 288 states)
unreached in proctype Intruder
        ReMT2ndProtocol2.pml:572, state 140, "KPK_BS = 1"
        ReMT2ndProtocol2.pml:574, state 160, "KSSResult = 1"
        ReMT2ndProtocol2.pml:574, state 162, "KBSResult = 1"
        ReMT2ndProtocol2.pml:588, state 190, "KSSResult = 1"
        ReMT2ndProtocol2.pml:588, state 192, "KBSResult = 1"
        (5 of 202 states)
unreached in claim SecrecyProperty
        _spin_nvr.tmp:8, state 8, "-end-"
        (1 of 8 states)

pan: elapsed time 4.21e+04 seconds
pan: rate 65417.642 states/second

What could the problem be?? can i really trust bitstate hashing since from what i have read, its best when the hash factor is greater than 100??

I also tried to use -w34 and onwards but got the message >> "Segmentation fault (core dumped)", does it mean that -w33 is the limit??

Offline

#4 2012-04-23 15:57:25

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

Re: Bitstate Hashing

yes bitstate is an approximation technique -- it performed well in this case
note that your search reached 2.7 billion states, each of 940 bytes
which would have taken 2.5 TerraBytes of RAM if you would have tried to do this
with a standard algorithm...
it means that your model is very very large -- too large to search exhaustively.
best is to simplify it.
the limit of -w?? is only determined by how much RAM memory you have on your machine
if you have a 32-bit machine, then the limit is likely 2 or 3 GB.
on a 64-bit machine it can be much larger of course.

Offline

Board footer

Powered by FluxBB