基于CSP的PSTM框架形式化分析與驗證
發(fā)布時間：2021-11-07 06:58
并行編程技術(shù)由于其運(yùn)算效率高且性能好的能力,一直是學(xué)術(shù)界和工業(yè)界的熱點研究對象。作為其中一種解決方案的事務(wù)內(nèi)存處理技術(shù)（Transactional Memory,TM）,采用以事務(wù)代替鎖的方式,解決了其他傳統(tǒng)解決方案中的種種問題。而在當(dāng)前市場上,TM的應(yīng)用還局限于傳統(tǒng)的交易系統(tǒng)和服務(wù)行業(yè)。原因可歸納為（1）支持TM技術(shù)的多核設(shè)備沒有得到普及,且當(dāng)下流行的編程語言并不支持TM;（2）并非所有類型的應(yīng)用程序都適用于TM類型的編程模型;（3）對TM技術(shù)應(yīng)用并行性的評估系統(tǒng)不夠完善。因此,將TM范式推廣到更多的應(yīng)用領(lǐng)域受到了阻礙。為解決這三種問題,PSTM（Python Software Transactional Memory）框架應(yīng)運(yùn)而生。本文從該框架的源代碼出發(fā),采用進(jìn)程代數(shù)演算中的通信順序進(jìn)程（Commu-nicating Sequential Processes,CSP）方法對 PSTM 框架進(jìn)行了深層次的形式化分析與建模。對PSTM框架中的通信過程與組件進(jìn)行多角度的抽象與分析,包括建立多層次的請求事務(wù)模型,循環(huán)提供服務(wù)的PSTMAPI、PSTM-Server組...
【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】：87 頁
【學(xué)位級別】：碩士
【部分圖文】：
圖２＿１：?ＰＳＴＭ框架??
證了事務(wù)請求通信的正確性和完整性。??２丄４功能演示??我們以一個最簡單的例子說明ＰＳＴＭ框架實現(xiàn)的功能＾如圖２．３所亂當(dāng)前系??統(tǒng)字典中僅有一個項，元對（Ｍ，３０）ｓ現(xiàn)在．．，總共有七個請求事務(wù)想要對該項??進(jìn)行更新，它們的鍵值均為１。其中，僅有前三個請求事務(wù)的版本和字典項的版本??匹配，因此Ｔ４至Ｔ７直接被系統(tǒng)忽略掉６假設(shè)Ｔ２的執(zhí)行速度快于Ｔ１和Ｔ３，率先成??功執(zhí)行了更新操作，則該字典項被更新為（１，１，７５），此時其版本值為１。因此，Ｔ１??和Ｔ３的版本不再和該字典項匹配，不能再執(zhí)行更新操作，被系統(tǒng)中止掉。所以，在??這次并行執(zhí)行請求的過程中，僅有Ｔ２成功執(zhí)行了更新操作，將字典項從（１，０，３０）??更新為（１，１，７５）。其他的事務(wù)不再滿足匹配條件，一次并行請求結(jié)東。??至此
的一個字典項。每個進(jìn)程都對該字典項執(zhí)行相同的操作，即將當(dāng)前值取出，自加一??并提交。由于起到的效果和計數(shù)器的一般功能一致，且稱之為共享計數(shù)器。??如圖５．１所示，這個案例由ｉＶ個相同的事務(wù)進(jìn)程并行組成，每個事務(wù)進(jìn)程都??執(zhí)行相同的事務(wù)函數(shù)所有的事務(wù)進(jìn)程共享一個共享計數(shù)器變量，也就??是說，所有的事務(wù)進(jìn)程都可以通過調(diào)用ＡＰＩ公共函數(shù)對該共享變量進(jìn)行操作。該??案例主要執(zhí)行兩個函數(shù)，除了上述提到的事務(wù)函數(shù)ｔｅｎＦｎ（ｇ），還有一個即是主函??．?dāng)?shù)?ｍａｉｎ（）。??主進(jìn)程（Ｔｈｅ?Ｍａｉｎ?Ｐｒｏｃｅｓｓ）執(zhí)行主函數(shù)如Ｐｙｔｈｏｎ偽代碼１所示。首??先，我們定義事務(wù)進(jìn)程的個數(shù)＝?６。然后，創(chuàng)建一個隊列ｇ，用于連接請求進(jìn)程??和服務(wù)器端。創(chuàng)建一個事務(wù)請求主進(jìn)程ｐｔｍ，用于做一些準(zhǔn)備工作，即將共享計數(shù)??器添加到系統(tǒng)字典中并對其進(jìn)行初始化。然后，便開始調(diào)用添加函數(shù)向系統(tǒng)字典中??添加以ｃｏｉｍｔｅｒ為關(guān)鍵字的字典項，此時該字典項的版本為０。該字典項即為共享??變量
【參考文獻(xiàn)】：
期刊論文
[1]多核多線程技術(shù)綜述[J]. 眭俊華,劉慧娜,王建鑫,秦慶旺. 計算機(jī)應(yīng)用. 2013(S1)
[2]任務(wù)并行編程模型研究與進(jìn)展[J]. 王蕾,崔慧敏,陳莉,馮曉兵. 軟件學(xué)報. 2013(01)
[3]多核處理器并行編程模型的研究與設(shè)計[J]. 曹折波,李青. 計算機(jī)工程與設(shè)計. 2010(13)
[4]軟件開發(fā)中的形式化方法[J]. 鄭紅軍,張乃孝. 計算機(jī)科學(xué). 1997(06)
本文編號：3481388
【文章來源】：華東師范大學(xué)上海市 211工程院校 985工程院校 教育部直屬院校
【文章頁數(shù)】：87 頁
【學(xué)位級別】：碩士
【部分圖文】：
圖２＿１：?ＰＳＴＭ框架??
證了事務(wù)請求通信的正確性和完整性。??２丄４功能演示??我們以一個最簡單的例子說明ＰＳＴＭ框架實現(xiàn)的功能＾如圖２．３所亂當(dāng)前系??統(tǒng)字典中僅有一個項，元對（Ｍ，３０）ｓ現(xiàn)在．．，總共有七個請求事務(wù)想要對該項??進(jìn)行更新，它們的鍵值均為１。其中，僅有前三個請求事務(wù)的版本和字典項的版本??匹配，因此Ｔ４至Ｔ７直接被系統(tǒng)忽略掉６假設(shè)Ｔ２的執(zhí)行速度快于Ｔ１和Ｔ３，率先成??功執(zhí)行了更新操作，則該字典項被更新為（１，１，７５），此時其版本值為１。因此，Ｔ１??和Ｔ３的版本不再和該字典項匹配，不能再執(zhí)行更新操作，被系統(tǒng)中止掉。所以，在??這次并行執(zhí)行請求的過程中，僅有Ｔ２成功執(zhí)行了更新操作，將字典項從（１，０，３０）??更新為（１，１，７５）。其他的事務(wù)不再滿足匹配條件，一次并行請求結(jié)東。??至此
的一個字典項。每個進(jìn)程都對該字典項執(zhí)行相同的操作，即將當(dāng)前值取出，自加一??并提交。由于起到的效果和計數(shù)器的一般功能一致，且稱之為共享計數(shù)器。??如圖５．１所示，這個案例由ｉＶ個相同的事務(wù)進(jìn)程并行組成，每個事務(wù)進(jìn)程都??執(zhí)行相同的事務(wù)函數(shù)所有的事務(wù)進(jìn)程共享一個共享計數(shù)器變量，也就??是說，所有的事務(wù)進(jìn)程都可以通過調(diào)用ＡＰＩ公共函數(shù)對該共享變量進(jìn)行操作。該??案例主要執(zhí)行兩個函數(shù)，除了上述提到的事務(wù)函數(shù)ｔｅｎＦｎ（ｇ），還有一個即是主函??．?dāng)?shù)?ｍａｉｎ（）。??主進(jìn)程（Ｔｈｅ?Ｍａｉｎ?Ｐｒｏｃｅｓｓ）執(zhí)行主函數(shù)如Ｐｙｔｈｏｎ偽代碼１所示。首??先，我們定義事務(wù)進(jìn)程的個數(shù)＝?６。然后，創(chuàng)建一個隊列ｇ，用于連接請求進(jìn)程??和服務(wù)器端。創(chuàng)建一個事務(wù)請求主進(jìn)程ｐｔｍ，用于做一些準(zhǔn)備工作，即將共享計數(shù)??器添加到系統(tǒng)字典中并對其進(jìn)行初始化。然后，便開始調(diào)用添加函數(shù)向系統(tǒng)字典中??添加以ｃｏｉｍｔｅｒ為關(guān)鍵字的字典項，此時該字典項的版本為０。該字典項即為共享??變量
【參考文獻(xiàn)】：
期刊論文
[1]多核多線程技術(shù)綜述[J]. 眭俊華,劉慧娜,王建鑫,秦慶旺. 計算機(jī)應(yīng)用. 2013(S1)
[2]任務(wù)并行編程模型研究與進(jìn)展[J]. 王蕾,崔慧敏,陳莉,馮曉兵. 軟件學(xué)報. 2013(01)
[3]多核處理器并行編程模型的研究與設(shè)計[J]. 曹折波,李青. 計算機(jī)工程與設(shè)計. 2010(13)
[4]軟件開發(fā)中的形式化方法[J]. 鄭紅軍,張乃孝. 計算機(jī)科學(xué). 1997(06)
本文編號：3481388
本文鏈接：http://sikaile.net/kejilunwen/jisuanjikexuelunwen/3481388.html
最近更新
教材專著
