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

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

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