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