0
$\begingroup$

I want to verify semantics of a library of atomic primitives that I wrote. The idea is, only if the semantics of all the primitives are consistent with each other, an application that uses them could behave predictably.

For example, a composition of a primitive Fx(lck) which takes exclusive lock on an lck object could be - Fx(Fx(lck)). But this could lead to a dead lock when operated on a single thread. This is a valid scenario if lck is a non-recursive lock.

I wonder if I could create a Petri Net model of my primitives to check if they are present a perfect synchronization tool.

You can also propose an alternate solution.

Improve this question
$\endgroup$
2
  • $\begingroup$ Sorry, I don't understand the question. What verification method is appropriate might depend on the particular primitives you want to model and what properties you want to prove of them. I don't know what you mean by "the composition of a primitive" or "a perfect synchronization tool". I do not see how the question could be answered in its current form. $\endgroup$
    – D.W. ♦
    Commented Jan 20, 2021 at 7:03
  • $\begingroup$ @D.W. By composition of atomic primitive, I want to represent a sequence of applications of those primitives on a given lock object. The example I presented was applicable in a single thread context, when the lock object is not a recursive lock. As I understand the correct use of atomic libraries protects shared data from reaching an unpredictable state. So, by perfect synchronization tool I meant the semantics of primitives should not leave data in some inconsistent state. May be it is not the most accurate way to express the requirements as english is not my first language. $\endgroup$
    – ultimate cause
    Commented Jan 20, 2021 at 7:47

1 Answer 1

Reset to default
1
$\begingroup$

Definitely, but you may need something stronger than a standard Place/Transition net.

You could try a tool for colored Petri nets, such as CPN Tools.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.