Simultaenous liveness and deadlock detection

[paulthomson]

On master branch. How do I get a hot monitor to cause an error?

See TestMasterHot.p.

event eStart;

main machine MainMachine
{
    start state Init 
    {
        entry 
        {
            monitor eStart;
        }
    }
}

spec M monitors eStart
{
    start hot state Init
    {
        on eStart goto Init;
    }
}

>> load TestMasterHot.p
2s
>> test /liveness
Writing TestMasterHot.zing ...
Compiling TestMasterHot.zing to TestMasterHot.dll ...
7s
>>

D:\pazure\testing3>zinger TestMasterHot.dll -et:et.txt -stats -p:4 /NDFSLiveness

##################
Check Passed
##################
4 distinct states explored
Maximum Depth Explored : 0
Elapsed time : 00:00:00
Memory Stats:
Peak Virtual Memory Size: 560.4453125 MB
Peak Paged Memory Size  : 145.0625 MB
Peak Working Set Size   : 144.09375 MB

D:\pazure\testing3>

I have tried other Zinger liveness flags.

[paulthomson]

OK, so it seems if I add an infinite cycle in the state-space then an error is found.

I would like to trigger an error at any terminal state if some condition does not hold. Is that possible?

[ankushdesai]

Hi Paul,

The deadlock property is encoded as a safety assertion in P. If you want to
check an eventually or finally property on a finite trace it is implemented
as an assertion that at the end of execution when all the process are
terminated or blocked the system should not be in a hot state. For checking
such properties you must compile P program without liveness flag and run
normal zinger search. This error will then be caught as a safety assertion
violation. You dont need to add a infinite looping process in this case.

Note that by adding infinite looping process you made the trace infinite.

On Thu, Feb 4, 2016 at 1:32 PM Paul Thomson notifications@github.com
wrote:

OK, so it seems if I add an infinite cycle in the state-space then an
error is found.

I would like to trigger an error at any terminal state if some
condition does not hold. Is that possible?

—
Reply to this email directly or view it on GitHub
#20 (comment).

[paulthomson]

Awesome! So doing the following makes it work:

>> load TestMasterHot.p
2s
>> test
Writing TestMasterHot.zing ...
Compiling TestMasterHot.zing to TestMasterHot.dll ...
7s
>>

The error message is not very clear though:

Error:
P Assertion failed:
Expression: assert(sizeof(SM_HANDLE.enabled) != 0 || sizeof(SM_HANDLE.hot) == 0)
Comment: Deadlock

Does it make sense to have both liveness and deadlock safety checks? So a program has infinite paths but also has some terminal states? E.g. A program might be able to get stuck in an infinite failure loop without making progress but might also be able to terminate in a hot state. If so, would it make sense for the safety check be added even when using the /liveness flag?

[ankushdesai]

Excellent point Paul !
I had exact same conversation with Shaz today morning but with the way
liveness checking and deadlock detection is implemented right now both the
checks cannot be enabled simultaneously.
But I agree with you that it would be nice to merge these two checks. I
will think about it.

On Thu, Feb 4, 2016 at 2:28 PM Paul Thomson notifications@github.com
wrote:

Awesome! So doing the following makes it work:

load TestMasterHot.p
2s
test
Writing TestMasterHot.zing ...
Compiling TestMasterHot.zing to TestMasterHot.dll ...
7s

The error message is not very clear though:

Error:
P Assertion failed:
Expression: assert(sizeof(SM_HANDLE.enabled) != 0 || sizeof(SM_HANDLE.hot) == 0)
Comment: Deadlock

Does it make sense to have both liveness and deadlock safety checks? So a
program has infinite paths but also has some terminal states? E.g. A
program might be able to get stuck in an infinite failure loop without
making progress but might also be able to terminate in a hot state. If so,
would it make sense for the safety check be added even when using the
/liveness flag?

—
Reply to this email directly or view it on GitHub
#20 (comment).

[shazqadeer]

I am not convinced yet that merging deadlock and livelock detection is a good idea. The current design requires the programmer to explicitly consider whether she is looking for a finite (assertions and deadlocks) or an infinite (livelocks) error trace. Different options should be passed to pc and zinger (consistently) depending on that choice. These options result in significantly different encodings and search techniques.