0
$\begingroup$

I am currently reading the extended Version of the Paper Online Detection of Effectively Callback Free Objects with Applications of Smart Contract.

I am trying to understand the proofs of Chapter 6. In particular, I cannot understand the premise of proofs 6.2. Indeed, the authors use a variant of SMAC, an Object-oriented and Turing Complete (SMAC) and they claim that (I underlined the suspicious claim with bold)

Thus, we focus on verifying $sECF$, namely, statically verifying whether all executions of an object are $dECF_{FS}$ or $ECF_{C}$, where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA). Such a PDA for an object o is able to simulate any modular well-formed execution $\kappa \in \pi$ where the active object of all states in $\pi$ is o.

In my understanding, this premise should be wrong, because although the state of this SMAC program is final, it is not computable by Push-Down-Automata (which compute total functions).

Foo:
     int x = 0 // field of the object
     enter // enter the single method of the object/contract
         while true do 
             x = 1
     return
Improve this question
$\endgroup$

1 Answer 1

Reset to default
0
$\begingroup$

where the domains of the object variables are restricted to finite sets. Hence, such objects can be modeled with a pushdown-automaton (PDA).

You are correct that if you understand it as using a pushdown-automaton to model the full behavior of the object, since as you indicated, you can put a Turing complete Turing machine inside any object.

However, I would believe that the authors intend to use a pushdown-automaton to mode an object in the domain with its possible states as defined by the values of its fields and its execution stack, since the whole paper is focusing on the ECF(Effectively Callback Free) property for objects. The actual moments when the object is still in the middle of changing from one state to another state are ignored/irrelevant/transparent/skipped. More specifically, the following shows the purpose of the object.

Such a PDA for an object o is able to simulate any modular well-formed execution $\kappa \in \pi$ where the active object of all states in $\pi$ is o

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you. Actually, the changes in between should be modelled, otherwise the state before the calls would not be correct and the state would be different. The fact that the states are finite, allows to model the computation with a Pushdown systems (which slightly differ from a pushdown automata and were introduced by Boujjani) $\endgroup$
    – Briomkez
    Oct 17, 2018 at 19:35
  • $\begingroup$ It looks like either you or I have not been crystally clear. In fact, I should NOT mention those moments when the object is still in the middle of changing from one state to another, since they are invisible/out of consideration. But since I have introduced this confusion, which might be the cause of your question as well, let me given an example. $\endgroup$
    – John L.
    Oct 18, 2018 at 4:09
  • $\begingroup$ Yes it is quite confusingv(it is not your fault :)) , but in one of the proofs in the technical report, they explicitly say that the automaton simulates the step of the code of the object o. So the automaton really model the code of o. $\endgroup$
    – Briomkez
    Oct 18, 2018 at 6:58
  • $\begingroup$ In essence, this paper is rather easy once written. The significance of the paper is, from my point of view, proposing new concepts and implementing some simple but new kind of algorithms, thus initiating a new direction and approach of research and practice. $\endgroup$
    – John L.
    Oct 18, 2018 at 7:02
  • $\begingroup$ I am not sure whether I can complete a concrete example soon (maybe Fig 9 and 10 are enough, though). My example will be used to show the stating change moments that are tracked/modelled by this PDA and the computation moments that are invisible to the "execution" as defined in the paper. Then how to intuitively understand "Given an execution $\kappa\vdash\pi$, checking if it is $dECF^o_{fs}$ is undecidable" but "assuming a finite domain for variables. Then there is an algorithm that decides if $o$ is $sECF_{fs}$" $\endgroup$
    – John L.
    Oct 18, 2018 at 7:15

Your Answer

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

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