Question: How to analyse entire Project with this tool ?

[vigneshr6]

When I run this command dingo-hunter cfsms --prefix deadlock mycom/rootdirectory
It gives the below error message

cannot import absolute path mycom/rootdirectory

no initial packages were loaded

How to solve this?

[nickng]

A possible reason why

no initial packages were loaded

is that this tool only analyses applications and not packages. It looks for the main package in the directory supplied by the command line argument. The main package should also contain a func main() (entry point to the application).

If mycom/rootdirectory is already a main package, could you please provide more information about the environment, package/structure of the project?

[vigneshr6]

my projects root directory contains a file with main function.
my project structure looks like this.
--myproject
--------UtilPackage
---------------util.go
--------CustomLogger
----------------log.go
--------main.go

when I run this command

dingo-hunter cfsms --prefix deadlock /home/mycom/myproject
I gets the below error

cannot import absolute path /home/mycom/myproject
no initial packages were loaded

If I run this tool with main.go
dingo-hunter cfsms --prefix deadlock /home/mycom/myproject

It says there is no method "unzipfunc" in my project

function unzipfunc is written in my UtilPackage

[nickng]

Could you please post the full output of the tool? The package structure and your comment:

It says there is no method "unzipfunc" in my project

They not sufficient for me to debug or understand what went wrong. If you do not wish to post this in public please contact me at nickng@imperial.ac.uk.

Also, when you run this tool with main.go, I guess you meant you used the following command?

dingo-hunter cfsms --prefix deadlock /home/mycom/myproject/main.go

Thanks.

[vigneshr6]

Hi @nickng
The issue I mentioned was my mistake.
Now I gets this kind of output.

Goto (*encoding/xml.Decoder).unmarshalAttr#9; }},(Empty); Goto (*encoding/xml.Decoder).unmarshalAttr#6; },(Empty); Goto (*encoding/xml.Decoder).unmarshalAttr#4; },(Empty); Goto (*encoding/xml.Decoder).unmarshalAttr#2; children: 2 &{(Empty); ,(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; }},(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#82; ,(Empty); Goto (*encoding/xml.Decoder).unmarshal#80; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#80; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; },(Empty); children: 2 &{(Empty); (*encoding/xml.Decoder).unmarshal#78; children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; ,(Empty); Goto (*encoding/xml.fieldInfo).value#1; Goto (*encoding/xml.Decoder).unmarshal#75; },(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#78; ,(Empty); children: 2 &{(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; ,(Empty); Goto (*encoding/xml.fieldInfo).value#1; Goto (*encoding/xml.Decoder).unmarshal#75; },(Empty); children: 2 &{(Empty); (*encoding/xml.Decoder).unmarshal#90; children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; ,(Empty); Goto (*encoding/xml.fieldInfo).value#1; Goto (*encoding/xml.Decoder).unmarshal#75; },(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#90; ,(Empty); children: 2 &{(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; ,(Empty); Goto (*encoding/xml.fieldInfo).value#1; children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; ,(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).savedOffset#2; ,(Empty); Goto (*encoding/xml.Decoder).savedOffset#2; Goto (*encoding/xml.Decoder).unmarshal#75; }}},(Empty); Goto (*encoding/xml.Decoder).unmarshal#75; }}}}}}},(Empty); Goto (*encoding/xml.Decoder).unmarshal#100; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#64; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#69; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#66; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#64; }}}}},(Empty); }}}}}}}}}}}}}}}}}}},(Empty); Goto (*encoding/xml.Decoder).unmarshal#26; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#26; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#23; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#19; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#19; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#16; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#14; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#12; },(Empty); children: 2 &{(Empty); children: 2 &{(Empty); Goto (*encoding/xml.Decoder).unmarshal#7; ,(Empty); Goto (*encoding/xml.Decoder).unmarshal#7; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#7; }},(Empty); Goto (*encoding/xml.Decoder).unmarshal#7; },(Empty); Goto (*encoding/xml.Decoder).unmarshal#2; }}},(Empty); Goto (*encoding/xml.Decoder).unmarshal#1; children: 2 &{(Empty); children: 2 &{(Empty); Goto os.Exit#2; ,(Empty); Goto os.Exit#2; Goto myProject/Kernel.main#3; },(Empty); Goto myProject/Kernel.main#3; }}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}
t70_7385: t70_7385; myProject/Kernel.main$1#1; Recv t70_7385<-??myProject/Kernel.main.t58@0; children: 2 &{(Empty); Goto myProject/Kernel.main$1#1; ,(Empty); Goto myProject/Kernel.main$1#1; }

Total of nodes per role (2 roles)
7 : t70_7385
5905 : main
2017/03/13 12:11:07 Machine 1 is empty
CFSMs written to third_party/gmc-synthesis/inputs/deadlock_cfsms
Total of 2 CFSMs (1 are channels)
0 = myProject/Kernel.main.t58@0 (channel)
1 = t70_7385

I can not understand anything from this.Can You explain this to me? or any documentation about this?
Thanks

[nickng]

The output looks correct, and generated files correctly for the 2nd part of the deadlock analysis.
Ignoring the debug outputs, it looks like there are 2 goroutines (i.e. 2 roles), but only 1 goroutine involve communication (because one of the CFSM Machine 1 is empty), and a total of 1 channel was created.

The output of this tool, third_party/gmc-synthesis/inputs/deadlock_cfsms, is a CFSM representation, and is input for a separate tool gmc-synthesis in the third_party/gmc-synthesis directory. You'll need Haskell (ghc) to build the synthesis tool following instructions on the README.

This is a research prototype --- unfortunately the only documentation for the tool I have right now is README, or the research paper for the details of the analysis.