一種ARM存儲模型的快速檢測方法

呂正　陳昊　陳峰

摘要：針對ARM多核處理器存儲模型正確性的快速檢測問題，提出了一種利用時間序和懸空窗口的有界特性的快速檢測方法，并實現了檢測工具。該方法給出了ARM存儲模型基于barrier的弱一致性模型的公理語義，通過定期掃描處理器的性能計數器獲得訪存指令操作間的時間約束關系。檢測工具由隨機指令發生模塊、多核處理器性能計數器記錄模塊和結果分析模塊3部分組成，它的低算法時間復雜度特性使其能夠有效處理上百萬行ARM訪存指令程序。檢測工具使用C++語言實現，可以在運行時動態調整指令流的長度參數，具有很好的擴展性。利用支持ARMMPC0re的模擬器進行了實驗，并用手工的方法在指令流執行序列中注入了幾個錯誤，以驗證程序結果是否違反ARM存儲模型。實驗結果表明，檢測工具能夠正確發現上述注入錯誤，檢測方法和檢測工具可以有效檢測ARM多核處理器存儲模型的正確性。關鍵詞：ARM處理器；存儲模型；正確性檢測