dingo hunter Download - dingo hunter Source Download

dingo hunter

หมวดหมู่อื่นๆ

1.0.0

ดาวน์โหลด

นักล่า Dingo

เครื่องวิเคราะห์แบบคงที่สำหรับการค้นหาการหยุดชะงักใน GO

นี่คือเครื่องวิเคราะห์แบบคงที่เพื่อสร้างแบบจำลองพร้อมกันและค้นหาการหยุดชะงักในรหัส GO วัตถุประสงค์หลักของเครื่องมือนี้คือการอนุมานจากรหัสแหล่งที่มาของโมเดลพร้อมกันในทั้งสองรูปแบบ:

การสื่อสารเครื่องจักรสถานะ จำกัด (CFSMS)
ประเภท Migo

แบบจำลองที่อนุมานจะถูกส่งผ่านไปยังเครื่องมือแยกต่างหากสำหรับการวิเคราะห์อย่างเป็นทางการ ในทั้งสองวิธีเราใช้ระบบที่รู้จักกันในวรรณคดีเป็น ประเภทเซสชัน เพื่อมองหาการสื่อสารที่ไม่ตรงกันที่อาจเกิดขึ้นกับการหยุดชะงักที่อาจเกิดขึ้น

ติดตั้ง

สามารถติดตั้ง dingo-hunter ได้โดย go get , GO เวอร์ชัน go1.7.1 เป็นสิ่งจำเป็น

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

การใช้งาน

มีสองวิธี (CFSMS และประเภท MIGO) ตามงานวิจัยสองชิ้น

วิธีการ CFSMS

วิธีการนี้สร้าง CFSMS เป็นแบบจำลองสำหรับ goroutines ที่วางไข่ในโปรแกรมจากนั้น CFSM จะถูกส่งผ่านไปยังเครื่องมือการสังเคราะห์เพื่อสร้างท่าเต้นทั่วโลกและตรวจสอบความถูกต้อง (ดูกระดาษ)

ก่อนอื่นติดตั้งเครื่องมือสังเคราะห์ gmc-synthesis โดยการตรวจสอบ submodule:

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

ติดตาม README เพื่อติดตั้งและสร้าง gmc-synthesis เช่น

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

ในการเรียกใช้การสร้าง CFSMS ใน example/local-deadlock/main.go :

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

เอาท์พุทควรพูด 2 ช่องจากนั้นเรียกใช้เครื่องมือการสังเคราะห์บน CFSM ที่สกัด

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

สาย SMC check ระบุว่ากราฟทั่วโลกเป็นไปตาม SMC (เช่นปลอดภัย) หรือไม่

ข้อ จำกัด

ขณะนี้เครื่องมือของเรารองรับการสื่อสารแบบซิงโครนัส (ช่องทางที่ไม่ได้รับการยกเว้น) เท่านั้น
Goroutines เกิดขึ้นหลังจากการสื่อสารใด ๆ จะต้องไม่ขึ้นอยู่กับการสื่อสารเหล่านั้น แบบจำลองของเราถือว่า goroutines มีการวางไข่อย่างอิสระ

วิธีการประเภท Migo

วิธีการนี้สร้างประเภท MIGO ซึ่งเป็นประเภทพฤติกรรมที่แนะนำในงานนี้เพื่อตรวจสอบความปลอดภัยและความมีชีวิตชีวาโดยข้อ จำกัด ที่เรียกว่า การฟันดาบ ในการใช้ช่องทาง (ดูกระดาษ)

ตัวตรวจสอบสำหรับประเภท MIGO มีอยู่ที่ Nickng/Gong ทำตามคำแนะนำในการสร้างเครื่องมือ:

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

ในการเรียกใช้การสร้างประเภท migo ใน example/local-deadlock/main.go :

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

ข้อ จำกัด

ช่องสัญญาณเป็นค่าส่งคืนไม่ได้รับการสนับสนุนในขณะนี้
channel recv, การทดสอบ OK ไม่สามารถเป็นตัวแทนใน MIGO (ต้องมีการตรวจสอบค่า แต่เป็นแบบที่เป็นนามธรรม)

สิ่งพิมพ์วิจัย

การตรวจจับการหยุดชะงักแบบคงที่สำหรับ GO ที่เกิดขึ้นพร้อมกันโดยการสังเคราะห์กราฟเซสชันระดับโลก, Nicholas NG และ Nobuko Yoshida, Int'l Conference on Compiler Construction (CC 2016), ACM
Fencing Off Go: ความปลอดภัยและความปลอดภัยสำหรับการเขียนโปรแกรมตามช่องทาง, Julien Lange, Nicholas Ng, Bernardo Toninho และ Nobuko Yoshida, ACM Sigplan Symposium เกี่ยวกับหลักการของภาษาการเขียนโปรแกรม (Popl 2017), ACM, ACM, ACM, ACM, ACM, ACM