How can we get meaning of the results of kjrun.sh --search

[kensh]

I have run following command , and I got those as its result. But I don't understand the meaning of each tags, such as which tag shows deadlock or race condition ,etc. Does anyone know any document of how to use this command and get meaning of its result.

$ kjrun.sh --search -v --timeout=0 ./java-semantics/model-check/73_examples/Philosopher.java

preprocess:

execute:

EXEC cmd: aux-kjrun.sh --time=true --timeout=0 --mode=search --output=pretty --input=kast --pattern=" Threads:Bag Out:List " --ltlmc="" --config="false" --verbose=true --cmd-suffix="" Philosopher.java.pkast

Search results:

Solution 1: Threads:Bag -->

synchronized ( objectRef ( 10 , class .Fork ) :: class .Fork ) { [ cast ( void , 'Invoke('Method('MethodName(cast ( class java.io.PrintWriter , class java.lang.System . out ),, println)),, [ cast ( class java.lang.Object , cast ( class java.lang.String , cast ( class java.lang.String , "Philosopher " :: class java.lang.String + cast ( int , cast ( class .Philosopher , cast ( class .Philosopher , class .Philosopher . this ) ) . id ) ) + " dined." :: class java.lang.String ) ) ]) ) ; ] } ~> [ .KList ] ~> env ( .Map ) ~> finallyBlock ( releaseLock ( 12 ) ) ~> [ return 'None(.KList) ; ] ~> env ( .Map ) ~> return 'Some(nothing :: void) ; ``` ListItem(sl ( HOLE ; , .K noClass .Map )) 3 false 12 |-> 1 37 class .Philosopher .Map ``` synchronized ( objectRef ( 11 , class .Fork ) :: class .Fork ) { [ cast ( void , 'Invoke('Method('MethodName(cast ( class java.io.PrintWriter , class java.lang.System . out ),, println)),, [ cast ( class java.lang.Object , cast ( class java.lang.String , cast ( class java.lang.String , "Philosopher " :: class java.lang.String + cast ( int , cast ( class .Philosopher , cast ( class .Philosopher , class .Philosopher . this ) ) . id ) ) + " dined." :: class java.lang.String ) ) ]) ) ; ] } ~> [ .KList ] ~> env ( .Map ) ~> finallyBlock ( releaseLock ( 10 ) ) ~> [ return 'None(.KList) ; ] ~> env ( .Map ) ~> return 'Some(nothing :: void) ; ``` ListItem(sl ( HOLE ; , .K noClass .Map )) 1 false 10 |-> 1 19 class .Philosopher .Map ``` synchronized ( objectRef ( 12 , class .Fork ) :: class .Fork ) { [ cast ( void , 'Invoke('Method('MethodName(cast ( class java.io.PrintWriter , class java.lang.System . out ),, println)),, [ cast ( class java.lang.Object , cast ( class java.lang.String , cast ( class java.lang.String , "Philosopher " :: class java.lang.String + cast ( int , cast ( class .Philosopher , cast ( class .Philosopher , class .Philosopher . this ) ) . id ) ) + " dined." :: class java.lang.String ) ) ]) ) ; ] } ~> [ .KList ] ~> env ( .Map ) ~> finallyBlock ( releaseLock ( 11 ) ) ~> [ return 'None(.KList) ; ] ~> env ( .Map ) ~> return 'Some(nothing :: void) ; ``` ListItem(sl ( HOLE ; , .K noClass .Map )) 2 false 11 |-> 1 28 class .Philosopher .Map ``` Out:List --> ListItem(#buffer ( "" ))

[laurayuwen]

I haven't played with the model checking part yet, but I assume that users need to model check properties against certain formulas (e.g. LTL). From the cmd above, I cannot infer that we want to check a deadlock. But the fact that every thread stuck in synchronized stmt probably indicate there is a dead lock here.

[laurayuwen]

Which version of Java semantics are you using? When I was doing the transferring from abstract to concrete syntax and from K maude backend to K Java backend, I neglected model checking, you need to go for the version Denis recommended in order to play with that.

[kensh]

laurayuwen, I'm really appreciated your quick answer. I had checkout 9840cfd from github.

I've read the paper written by Bogdanas in popl 2015. And the paper. http://fsl.cs.illinois.edu/FSL/papers/2015/bogdanas-rosu-2015-popl/bogdanas-rosu-2015-popl-public.pdf

The paper said that they successfully used this approach to detect the deadlock in the Dining Philosophers problem at 5. Applications. So what I wanted to do was re-examining this paper in order to get my own knowledge about java-semantics and K-framework.

Denis recommended me following url. Is this what you are saying? https://github.com/kframework/java-semantics/tree/popl-artifact-evaluation

I just want to know anything about java-semantics. If there are any step-by-step learning-websites about java-semantics, I am eager to know them.

thanks.

[laurayuwen]

Ok, I see. So the version you checked out may not be consistant with what Denis declared in his paper, exspecially model checking. That part was temporarily ignored when we decided to do all the upgrades (to work on new K, to express in concrete syntax) ...

I would recommend you to work with the branch of popl-artifact-evaluation as you are trying to use Java semantics in versatile ways, and also, that version is quite stable. The main branch could be changed on a daily basis. Unfortunately, I don't think we have a website about Java-semantics, there aren't that mant people working on this project to afford that, sorry about that and thank you so much for your interests ;)

[kensh]

laurayuwen, thank you.

I would try checking out https://github.com/kframework/java-semantics/tree/popl-artifact-evaluation and figure out if I could re-exame what paper is saying. Please don't be sorry about less information about new ideas and applications, your generous support are really appreciated.

[kensh]

I was using https://github.com/kframework/java-semantics/tree/popl-artifact-evaluation version, and I still got errors with following command. I'm not sure how to fix this. I need your help.

$ kjrun.sh --debug ../tests/01_smoke_tests/helloWorld.java preprocess:

execute:

org.kframework.krun.KRunExecutionException: Warning: "maude_in.maude", line 3: didn't expect token ,:

<_>_ ( generatedTop , <_>_ ( T , ( <_>_ ( threads , <_>_ ( thread , ( <_>_ ( k , _`(_`) ( 'unfoldingPhase , .KList ) , k ) ) ( <_>_ ( stack , .List , stack ) ) ( <_>_ ( methodContext , ( <_>_ ( env , .Map , env ) ) ( <_>_ ( crntClass , _`(_`) ( 'noClass , .KList ) , crntClass ) ) ( <_>_ ( location , .K , location ) ) , methodContext ) ) ( <_>_ ( threadData , ( <_>_ ( tid , _`(_`) ( #_ ( 0 ) , .KList ) , tid ) ) ( <_>_ ( holds , .Map , holds ) ) ( <_>_ ( interrupted , _`(_`) ( #_ ( false ) , .KList ) , interrupted ) ) , threadData ) ) , thread ) , threads ) ) ( <_>_ ( classes , .Bag , classes ) ) ( <_>_ ( globalPhase , _`(_`) ( 'UnfoldingPhase , .KList ) , globalPhase ) ) ( <_>_ ( lastGlobalPhase , _`(_`) ( 'ExecutionPhase , .KList ) , lastGlobalPhase ) ) ( <_>_ ( phStart , ( <_>_ ( program , , <---_HERE_ Warning: "maude_in.maude", line 3: no parse for term. ``` at org.kframework.backend.maude.krun.MaudeKRun.executeKRun(MaudeKRun.java:87) at org.kframework.backend.maude.krun.MaudeKRun.run(MaudeKRun.java:124) at org.kframework.backend.maude.krun.MaudeKRun.step(MaudeKRun.java:148) at org.kframework.krun.api.KRunApiDebugger.(KRunApiDebugger.java:72) at org.kframework.backend.maude.krun.MaudeKRun.debug(MaudeKRun.java:751) at org.kframework.krun.Main.debugExecution(Main.java:633) at org.kframework.krun.Main.execute_Krun(Main.java:1460) at org.kframework.main.Main.main(Main.java:64) ``` [Error] Critical: Warning: "maude_in.maude", line 3: didn't expect token ,: <_>_ ( generatedTop , <_>_ ( T , ( <_>_ ( threads , <_>_ ( thread , ( <_>_ ( k , _`(_`) ( 'unfoldingPhase , .KList ) , k ) ) ( <_>_ ( stack , .List , stack ) ) ( <_>_ ( methodContext , ( <_>_ ( env , .Map , env ) ) ( <_>_ ( crntClass , _`(_`) ( 'noClass , .KList ) , crntClass ) ) ( <_>_ ( location , .K , location ) ) , methodContext ) ) ( <_>_ ( threadData , ( <_>_ ( tid , _`(_`) ( #_ ( 0 ) , .KList ) , tid ) ) ( <_>_ ( holds , .Map , holds ) ) ( <_>_ ( interrupted , _`(_`) ( #_ ( false ) , .KList ) , interrupted ) ) , threadData ) ) , thread ) , threads ) ) ( <_>_ ( classes , .Bag , classes ) ) ( <_>_ ( globalPhase , _`(_`) ( 'UnfoldingPhase , .KList ) , globalPhase ) ) ( <_>_ ( lastGlobalPhase , _`(_`) ( 'ExecutionPhase , .KList ) , lastGlobalPhase ) ) ( <_>_ ( phStart , ( <_>_ ( program , , <---_HERE_ Warning: "maude_in.maude", line 3: no parse for term. real 0m14.128s user 0m29.019s sys 0m1.237s

[laurayuwen]

The error is caused by a failure is preprocessing stage. I didn't maintain this branch. This branch is a branch Denis used for popl artifact evaluation. So This kind of failure is unexpected. Could you tell me your k version by "krun --version", and your operating system, java version, and I will try to reproduce the error and see what's going on. You are using the latest commit of that branch, right?

[kensh]

Thanks, laurayuwen

$ krun --version K-framework version 3.4. Git Revision: 08c9271 Build date: Tue Aug 26 13:56:56 PDT 2014

$ java -version java version "1.8.0_31" Java(TM) SE Runtime Environment (build 1.8.0_31-b13) Java HotSpot(TM) 64-Bit Server VM (build 25.31-b07, mixed mode)

and I got the latest of that branch following is the copy of SHA 348e7f421b95e120e206266bd0d08ac6eb4f57a4

[laurayuwen]

Ok, I got the same error. Very sorry about that, that is a branch Denis used for his paper evaluation, so I assumed that things are working there. Since he has graduated, I won't depend on him to fix this issue, I will debug it. Or find you some version that is working. You use Mac, right? Is Linux ok?

Is model-checking the main part of interests from K-JAVA for you? Because this year we have made lots of changes to incorporate new K framework, but that framework hasn't provide model checking yet. Generally we want to focus on making new things better instead of fixing old things.

[kensh]

Yes, I m using Mac Book, And Linux on my VirtualBox. Both OS are fine to me. Just prefer Mac. What I wanted to do is model-checking larger amount of codes like popular libraries in order to detect dead-code or race-condition.

I am also a professional software engineer, so I understood that making new things better instead of fixing old things.

How great it is, if you are fixing k-java and model-checking features for us.

thanks.

[laurayuwen]

OK. I fixed the problem on my laptop, it is not really the semantics' problem in my case. Could you check class-lib folder and delete the .kast files? That is a folder for library classes, and are loaded together with the input program. The problem is, in order to speed up, we store the parsed files (kast files) so our parser does not repeat this job every time a new program feed in to parse. Those files are not tracked by git, so when you check out a different commit, those files stay there. If the two commits you were using and are about to use have different parsers, these files might trap you. I can run programs after this fix, but it might be other issue in your case, let's try this first, ok?

[kensh]

Thank you for your explanations about how k-java speeds up. I deleted *.kast files in class-lib folder. But I still got exactly the same error. I think that is other issue happening on mine.

[laurayuwen]

If I cannot reproduce the bug, that is really hard for me to debug. On the other hand, back to the version you where you can run basic execution: 9840cfde929795e834397fb7f4ac98f87ee88c64, did you kompile with the right option? I mean: kjkompile.sh --threading

That you will get 7 solutions as claimed, and the one you copied above is the deadlock situation.