Spinroot

srirajpaul

Member

Registered: 2013-09-07

Posts: 13

Assert fails when the value it is asserting is true

Hi,
I am getting an assert failure, but the value is true.

My program is structured as follows:

do
:: case_1 ->
:: case_2 ->
    d_step{
   
    .
    .
    .
    printf("%d\n", func(me));
    assert(func(me));
    }
od;

I am model checking the same in multicore mode(32 threads). This is resulting in an assert failure.
The value of func(me) is printed as 1, yet the assert fails. From the trace I manually
evaluated the  value of func(me) and that also turns out to be true.

Model checking does not terminate immediately after the 'claimed' assertion violation.
The process stops after case_2 in the next iteration, and then reports the assertion violation;
this was determined from the trace generated via spin -t.

The assertion violation can be seen at line 360 of output.txt [1]
This assertion is called on line 2965 on the file new_pe.pml [1]
The trace file is new_pe.pml.trail [1]

To get an idea of what would be happening I tried to run using the trace file as
spin -t new_pe.pml > trace.txt

My understanding is that the problem is coming from "proc 5"
Proc 5 represents process_[4] in our model since init{} occupies proc 0.
Line 236 of trace.txt outputs - "[4]: transient_count_phase_node 1"
shows that the assert is evaluated to true and also the d_step is over.
After that other processes are executing. Later control comes back to
process 5 and it executes case_2 (line 2835 of new_pe.pml) and it fails
reporting assertion failure from previous iteration.

The model was a large and hence I changed the Spin source.
I changed Line 16 in Src/dstep.c to "#define MAXDSTEP        8196    /* was 512 */"
The default value was 2048.

I ran it in an AMD opteron platform as follows
I compiled the code as
gcc -O3 -DVECTORSZ=72000 -DCOLLAPSE -DSAFETY -DMEMLIM=62000 -DNCORE=32 -DFULL_TRAIL pan.c -o phaser_f_32_ft
And ran as just ./phaser_f_32_ft

I also tried it in IBM POWER 7 using xlc compiler. There also the same problem happens.

I am running the same program using different starting configuration. The problem occurred only in this one.

Thank you
Sriraj

[1] Files are uploaded at http://srp7.web.rice.edu/

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Assert fails when the value it is asserting is true

Which version of Spin did you use?
Do you get the same type of error with a standard (single-core) DFS?

srirajpaul

Member

Registered: 2013-09-07

Posts: 13

Re: Assert fails when the value it is asserting is true

Hi, I am using version 6.4.0.
The same error comes in older versions also, like 6.2.7.

With 32 cores it took around 3 hours to get this error. I am not sure whether I can get the same error with single core DFS version.
I have given two runs for 24 and 72 hours in the standard (single-core) DFS version. I will report it as soon as it completes.

Thank you

srirajpaul

Member

Registered: 2013-09-07

Posts: 13

Re: Assert fails when the value it is asserting is true

Hi,
Sorry for the post.
The single core run found an assert violation which was a real assert violation.
But we were not able to see it in multicore run because, the trace was not full. We enabled -FULL_TRAIL, but still the trace didn't had the error.
The violation was happening in future. If the trace had printed a few more lines it would have reached the assert violation.

Thank you