基于約束求解的并發(fā)程序錯誤探測.pdf

1、為保證正確性，并發(fā)程序中某個方法或代碼塊中的語句序列必須原子執(zhí)行。若該語句序列與其他并發(fā)單元中語句存在預(yù)期之外的交織，且其執(zhí)行結(jié)果不同于原子性執(zhí)行結(jié)果，則產(chǎn)生原子違背。原子違背是常見的并發(fā)缺陷，可導(dǎo)致讀寫值不一致、讀取中間結(jié)果等嚴重后果。現(xiàn)有原子違背探測技術(shù)大多采用較為保守的并發(fā)程序執(zhí)行模型進行原子違背探測，存在漏報和誤報等問題。
　　為提高原子違背探測能力，本文提出一種基于約束求解的原子違背探測方法，可有效探測原子違背，且一般不

2、產(chǎn)生誤報。該方法通過融合程序控制流信息，擴大可搜索的并發(fā)執(zhí)行交織空間大小，提高其探測能力。在探測過程中，該方法首先將程序的控制流信息和并發(fā)執(zhí)行交織的可行性要求轉(zhuǎn)化為一組約束等式，然后通過約束求解進行原子違背探測。此外，為提高探測效率，本文還提出一種分支事件可行性松弛的近似優(yōu)化算法，去除探測過程中不必要的約束等式，減少約束求解時間。
　　在上述工作的基礎(chǔ)上，本文實現(xiàn)了基于約束求解的原子違背探測工具ConAV，并與基于錯誤模式的并發(fā)錯