goncurrency analysis framework

演示工具用於GO並發分析框架

基本工具由可運行的代碼編輯器組成（用於遊樂場軟件包）。設計用於將GO代碼轉換為中間格式的2階段轉換，然後使用外部工具進行分析。

工具支持

• CFSM方法
  • CFSM合成
  • 論文：並發的靜態僵局檢測通過全局會話圖合成
• 鑼的方法
  • 鑼安全和寬鬆檢查器
  • 論文：圍欄：基於渠道的編程的耐受性和安全性
• Godel Checker
  • Migoinfer和Godel-Checker
  • 論文：使用行為類型的靜態驗證框架，用於傳遞消息的靜態驗證框架

配置和用法

服務器端：HTTP處理程序

WebService處理程序是在webservice/webservice.go中定義的，定義為名稱和INIT函數。 InitFunc設置HTTP處理程序路徑（使用默認的http.HandleFunc ）。

 type Handler struct {
    Name     string
    InitFunc func()
}

可以通過可執行文件中的標誌選擇性地加載HTTP處理程序。默認情況下，只有Godel被加載。

客戶端：JavaScript

事件處理程序以AJAX調用為static/script.js設置，應將響應編碼為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 }