Simultaenous liveness and deadlock detection about p HOT 5 CLOSED

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?

from p.

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 [email protected]
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).

from p.

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?

from p.

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 [email protected]
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).

from p.

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.

from p.