Unduh dingo hunter - Unduh Kode Sumber dingo hunter

dingo hunter

Kategori lainnya

1.0.0

Unduh

Dingo-Hunter

Penganalisa statis untuk menemukan kebuntuan di go

Ini adalah penganalisa statis untuk memodelkan konkurensi dan menemukan kebuntuan dalam kode GO. Tujuan utama dari alat ini adalah untuk menyimpulkan dari kode sumber go model konkurensi di salah satu dari dua format:

Mengkomunikasikan mesin negara terbatas (CFSMS)
Jenis Migo

Model yang disimpulkan kemudian diteruskan ke alat yang terpisah untuk analisis formal. Dalam kedua pendekatan tersebut, kami menerapkan sistem yang dikenal dalam literatur sebagai jenis sesi untuk mencari ketidaksesuaian komunikasi potensial untuk mencegah kebuntuan potensial.

Memasang

dingo-hunter dapat diinstal oleh go get , Go Versi go1.7.1 diperlukan.

 $ go get -u github.com/nickng/dingo-hunter

Penggunaan

Ada dua pendekatan (tipe CFSM dan MIGO) berdasarkan dua pekerjaan penelitian.

Pendekatan CFSMS

Pendekatan ini menghasilkan CFSMS sebagai model untuk goroutine yang ditimbulkan dalam program ini, CFSM kemudian diteruskan ke alat sintesis untuk membangun koreografi global dan memeriksa validitas (lihat kertas).

Pertama instal alat sintesis gmc-synthesis dengan memeriksa submodule:

 $ cd $GOPATH/src/github.com/nickng/dingo-hunter; git submodule init; git submodule update
$ cd third_party/gmc-synthesis

Ikuti README untuk menginstal dan membangun gmc-synthesis , yaitu

 $ cabal install MissingH split Graphalyze
$ ./getpetrify # and install to /usr/local/ or in $PATH
$ ghc -threaded GMC.hs --make && ghc --make BuildGlobal

Untuk menjalankan pembuatan CFSMS pada example/local-deadlock/main.go :

 $ dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go

Output harus mengatakan 2 saluran, lalu jalankan alat sintesis pada CFSM yang diekstraksi

 $ cd third_party/gmc-synthesis
$ ./runsmc inputs/deadlock_cfsms 2 # where 2 is the number of channels

Garis SMC check menunjukkan apakah grafik global memenuhi SMC (yaitu aman) atau tidak.

Keterbatasan

Alat kami saat ini hanya mendukung komunikasi sinkron (saluran unbuffered) saja
Goroutine melahirkan setelah operasi komunikasi apa pun tidak boleh bergantung pada komunikasi tersebut. Model kami mengasumsikan goroutine ditelurkan secara independen.

Pendekatan Jenis Migo

Pendekatan ini menghasilkan tipe Migo, jenis perilaku yang diperkenalkan dalam pekerjaan ini, untuk memeriksa keamanan dan lives dengan pembatasan yang disebut pagar pada penggunaan saluran (lihat kertas).

Pemeriksa untuk jenis MIGO tersedia di Nickng/Gong, ikuti instruksi untuk membangun alat:

 $ git clone ssh://github.com/nickng/gong.git
$ cd gong; ghc Gong.hs

Untuk menjalankan generasi jenis migo pada example/local-deadlock/main.go :

 $ dingo-hunter migo example/local-deadlock/main.go --no-logging --output deadlock.migo
$ /path/to/Gong -A deadlock.migo

Keterbatasan

Saluran sebagai nilai pengembalian tidak didukung sekarang
Saluran RECV, OK Test Tidak mungkin untuk mewakili di MIGO (membutuhkan nilai memeriksa tetapi diabstraksikan berdasarkan jenis)

Publikasi Penelitian

Deteksi Deadlock Statis Untuk Sintesis Grafik Sesi Global GO GO GO Global, Nicholas Ng dan Nobuko Yoshida, Konferensi Int'l tentang Konstruksi Kompiler (CC 2016), ACM
Fencing Off Go: Liveness and Safety untuk pemrograman berbasis saluran, Julien Lange, Nicholas NG, Bernardo Toninho dan Nobuko Yoshida, ACM Sigplan Simposium tentang Prinsip-prinsip Bahasa Pemrograman (POPL 2017), ACM

Catatan

Ini adalah prototipe penelitian, dan mungkin tidak berfungsi untuk semua kode sumber Go. Harap ajukan masalah untuk masalah yang terlihat seperti bug.