goncurrency analysis framework

เครื่องมือสาธิตสำหรับกรอบการวิเคราะห์พร้อมกัน GO

เครื่องมือพื้นฐานประกอบด้วยตัวแก้ไขรหัสที่เรียกใช้งานได้ (สำหรับใช้กับแพ็คเกจสนามเด็กเล่น) ออกแบบมาสำหรับการแปลงรหัส GO 2 ขั้นตอนเป็นรูปแบบกลางจากนั้นวิเคราะห์ด้วยเครื่องมือภายนอก

การสนับสนุนเครื่องมือ

• วิธี CFSM
  • การสังเคราะห์ CFSM
  • กระดาษ: การตรวจจับการหยุดชะงักแบบคงที่สำหรับการไปพร้อมกันโดยการสังเคราะห์กราฟเซสชันทั่วโลก
• แนวทางฆ้อง
  • ตัวตรวจสอบความปลอดภัยของฆ้อง
  • กระดาษ: Fencing Off Go: Liventi และ Safety สำหรับการเขียนโปรแกรมตามช่อง
• Godel Checker
  • Migoinfer และ Godel-checker
  • กระดาษ: กรอบการตรวจสอบแบบคงที่สำหรับข้อความที่ส่งผ่านไปโดยใช้ประเภทพฤติกรรม

การกำหนดค่าและการใช้งาน

ด้านเซิร์ฟเวอร์: HTTP Handler

Webservice Handler ถูกกำหนดไว้ใน webservice/webservice.go ซึ่งกำหนดเป็นชื่อและฟังก์ชั่น init InitFunc ตั้งค่าพา ธ HTTP Handler (ใช้ค่าเริ่มต้น http.HandleFunc )

 type Handler struct {
    Name     string
    InitFunc func()
}

HTTP Handlers สามารถโหลดได้โดยการตั้งค่าสถานะในการปฏิบัติการ โดยค่าเริ่มต้นจะมีการโหลด Godel เท่านั้น

ฝั่งไคลเอ็นต์: JavaScript

ตัวจัดการเหตุการณ์ถูกตั้งค่าใน static/script.js เป็นการเรียก AJAX การตอบสนองควรเข้ารหัสเป็นวัตถุ JSON

• Migo (V1 และ V2)
  • จุดสิ้นสุด: '/migo.v1' และ '/migo.v2'
  • การตอบสนอง: { 'MiGo': migo_output, 'time': execution_time, 'Error': error }
• การสังเคราะห์ CFSM
  • จุดสิ้นสุด: '/cfsm'
  • การตอบสนอง: { 'CFSM': cfsm_output, 'time': execution_time, 'Error': error }
• ฆ้อง
  • จุดสิ้นสุด: '/gong'
  • การตอบสนอง: { 'Gong': gong_output, 'time': execution_time, 'Error': error }
• Godel Checker
  • จุดสิ้นสุด: '/godel'
  • การตอบสนอง: { 'Godel': godel_output, 'time': execution_time, 'Error': error }