Java并發(fā)程序的模型提取與模型檢測(cè)技術(shù)研究.pdf

1、隨著多核心處理器系統(tǒng)的發(fā)展，分布式并發(fā)系統(tǒng)已成為當(dāng)前主流的軟件體系結(jié)構(gòu)。分布式軟件的特性導(dǎo)致錯(cuò)誤不可重現(xiàn)，使軟件排錯(cuò)工作非常困難。Java是在語(yǔ)言級(jí)別支持并發(fā)的高級(jí)語(yǔ)言，其提供的語(yǔ)言特性和大量的類庫(kù)很好地支持了并發(fā)程序的編寫。但這些類庫(kù)都有各自的特點(diǎn)，如果使用不當(dāng)會(huì)造成一些難以發(fā)現(xiàn)，卻危害嚴(yán)重的問(wèn)題。同時(shí)，Java內(nèi)存模型JMM（Java Memory Model）允許編譯器在優(yōu)化過(guò)程中改變程序的執(zhí)行順序，這會(huì)讓多線程Java程序產(chǎn)生許

2、多意想不到的錯(cuò)誤。Java規(guī)范中程序的正確性僅僅依賴于程序員編寫正確的，不會(huì)沖突的代碼，很難滿足高可靠性軟件的要求。 針對(duì)上述問(wèn)題，本文提出了一套對(duì)Java多線程并發(fā)程序錯(cuò)誤進(jìn)行檢測(cè)的方法。第一部分工作提出了一種自動(dòng)化模型檢測(cè)的技術(shù)，并制作了工具JTS（Java To SPIN），實(shí)現(xiàn)了對(duì)Java并發(fā)程序的模型檢測(cè)與驗(yàn)證。JTS對(duì)Java程序進(jìn)行分析，產(chǎn)生抽象語(yǔ)法樹(shù)，建立程序的抽象模型。分析中特別針對(duì)Java虛擬機(jī)的并發(fā)機(jī)制和類

3、庫(kù)實(shí)現(xiàn)進(jìn)行了建模，并利用模型檢測(cè)工具SPIN進(jìn)行了模型檢測(cè)。在實(shí)驗(yàn)中JTS成功地對(duì)多個(gè)Java程序進(jìn)行了模型提取和模型檢測(cè)，給出了錯(cuò)誤路徑。JTS建立的模型準(zhǔn)確地再現(xiàn)了Java程序的執(zhí)行過(guò)程，發(fā)現(xiàn)了其中隱藏的并發(fā)程序錯(cuò)誤。這種檢測(cè)方法為發(fā)現(xiàn)和修正這類不可重現(xiàn)，難以測(cè)試的并發(fā)錯(cuò)誤提供了一種新的方法和思路，是傳統(tǒng)測(cè)試方法在并行程序領(lǐng)域的的一種嘗試與補(bǔ)充。 第二部分工作提出了另一種新的方法，針對(duì)JMM所允許的程序順序變化，結(jié)合程序中的