連結式全域述句偵測中無用事件之排除

Abstract

針對分散式程式進行除錯及測試工作時, 一項很重要的關鍵技術是偵測全域述句(globalpredicates) 的真偽值。因為一般形式的全域述句須處理呈組合爆炸(combinatorialexplosion) 成長的可能狀態, 故傳統上多以偵測表達能力較弱但可處理 (tractable) 的連結式 (conjunctive) 全域述句。這種作法將全域述句在邏輯層次上分解成多個區域述句, 每個區域述句皆可由單一的程序來個別偵測。各個程式會將引發區域述句成立的事件統一送至一偵測程序 (checker process), 由偵測程序來決定這些個別的區域事件是否可形成一致的全域事件, 進而決定此全域述句是否成立。本計畫即針對傳統連結式全域述句的偵測方法, 提出可以利用偵測程序的空閒時間 (idle time), 預先找出並除去事件佇列中無用 (useless) 事件的改進方法。這個方法可以減低佇列的空間需求並加快述句偵測的處理時間。以往研究者所做的結果並無法找出並除去所有無用的事件。我們計畫改進這個缺點,找出所有不必要的事件, 而且希望所提出的方法可以平行處理, 以減低演算法本身的複雜度。