Blocking bugs with more than one channels

[julien-lange]

Hello!

Thanks for the very impressive work!

I was trying out GCatch, after reading your paper. I wasn't too sure whether or not GCatch can detect bugs that arise between circular dependencies between more than one channels. Reading the paper, I thought 'yes' (cf. beginning of Section 3.2) but trying out the tool, I thought 'no', e.g., no bug is detected in the following example:

package main

func main() {
    a := make(chan int)
    b := make(chan int)
    go func() {
        <- b
        a <- 1
    }()
    <- a
    b <- 1  
}

I am using GCatch -path=$GOPATH/src/<my-working-dir> -checker=BMOC -compile-error

Is that the expected results or am I missing something?

Cheers,

J.

[lzhfromustc]

Hello Dr. Lange,

Thanks for being interested in our project and reporting this issue to us! GCatch should be able to catch circular wait bugs like this.

This issue might be caused by the input or output. BTW, you might want to use the -include= and -r flags, so the command is: GCatch -path=$GOPATH/src/<my-working-dir> -include=<my-working-dir> -checker=BMOC -compile-error -r Note: <my-working-dir> is something like github.com/docker/docker

I will also try this out on my machine and see if this is caused by the output of GCatch (my output is kinda messy~). I will let you know soon.

Best regards, Ziheng Liu

[system-pclub]

@lzhfromustc can you post the current command and the output on your machine here? It would be good if you can commit Julien's example into our repo.

[lzhfromustc]

Good idea. I will add this into our testdata and put the output in this issue later

[julien-lange]

Thanks for getting back to me.

Just in case it helps, the output I get when I run the command above (with the example I listed) is:

Successfully built whole program. Now running checkers
-----count_unbuffer_bug: 0 ---buffer_bug: 0
-----count_ch: 1
-----count_unbuffer_bug: 0 ---buffer_bug: 0
-----count_ch: 2
Exit. If you want to scan subdirectories and use -race, please use -r

Time of main(): seconds 0.08069748

If, say, I comment out the receive from a (<- a), I get

Successfully built whole program. Now running checkers
Satisfiable!
------Thread  0
Node  0 : Go
    Order:  0
Node  1 : Chan_op
    Order:  1
------Thread  1
Node  0 : Chan_op
    Order:  1
Node  1 : Chan_op
    Order:  4
(>= G_0_N_0_Order 0)
(< G_0_N_0_Order 4)
(>= G_0_N_1_Order 0)
(< G_0_N_1_Order 4)
(> G_0_N_1_Order G_0_N_0_Order)
(>= G_1_N_0_Order 0)
(< G_1_N_0_Order 4)
(= G_1_N_1_Order 4)
(> G_1_N_1_Order G_1_N_0_Order)
(> G_1_N_0_Order G_0_N_0_Order)
true
(=> Pair_G_0_N_1G_1_N_0_use (= G_0_N_1_Order G_1_N_0_Order))
-------Confirmed blocking path 
-----Blocking at:
    File: /Users/USERNAME/go/src/temp2/dummy.go:9
-----Blocking Path:
Chan_op :/Users/USERNAME/go/src/temp2/dummy.go:8:3   '✓'
Chan_op :/Users/USERNAME/go/src/temp2/dummy.go:9:5   Blocking
Return :/Users/USERNAME/go/src/temp2/dummy.go:9:5    '✗'
-----Path NO. 0     Entry func at: temp2.main
ChanMake :/Users/USERNAME/go/src/temp2/dummy.go:5:11     '✓'
ChanMake :/Users/USERNAME/go/src/temp2/dummy.go:6:11     '✓'
Go :/Users/USERNAME/go/src/temp2/dummy.go:7:2    '✓'
Chan_op :/Users/USERNAME/go/src/temp2/dummy.go:12:4  '✓'
Return :/Users/USERNAME/go/src/temp2/dummy.go:12:4   '✓'

-----count_unbuffer_bug: 1 ---buffer_bug: 0
-----count_ch: 1
-----count_unbuffer_bug: 1 ---buffer_bug: 0
-----count_ch: 2
Exit. If you want to scan subdirectories and use -race, please use -r

Time of main(): seconds 0.109697634

[lzhfromustc]

Hi Dr. Lange,

Thanks again for pointing out the problem to us! I updated the repo, added this example into the testdata, changed some code and the format of bug outputs. Now when I run the following commands:

GOPATH=/The/GOPATH/Of/GCatch sudo $GOPATH/src/github.com/system-pclub/GCatch/GCatch/install.sh GCATCH=$GOPATH/bin/GCatch export GOPATH=$GOPATH/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram sudo $GCATCH -path=$GOPATH/src/circularWait -include=circularWait -checker=BMOC -r

I can get the following results:

Successfully built whole program. Now running checkers ----------Bug[1]---------- Type: BMOC Reason: One or multiple channel operation is blocked. -----Blocking at: File: /data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:10 File: /data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:7 -----Blocking Path NO. 0 ChanMake :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:4:11 '✓' ChanMake :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:5:11 '✓' Go :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:6:2 '✓' Chan_op :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:10:2 Blocking Chan_op :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:11:4 '✗' Return :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:11:4 '✗' -----Blocking Path NO. 1 Chan_op :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:7:3 Blocking Chan_op :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:8:5 '✗' Return :/data/ziheng/shared/gcatch/src/github.com/system-pclub/GCatch/GCatch/testdata/toyprogram/src/circularWait/main.go:8:5 '✗'

Now trying to build unchecked packages separately...

Time of main(): seconds 0.106532089

[julien-lange]

That's great, thanks!

[songlh]

thanks a lot for the example.