A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

Pages: **1**

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

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

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

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

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

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

Pages: **1**