(3.215.77.193) 您好!臺灣時間:2021/04/17 01:19
字體大小: 字級放大   字級縮小   預設字形  
回查詢結果

詳目顯示:::

我願授權國圖
: 
twitterline
研究生:王維道
研究生(外文):Wei-Tao Wang
論文名稱:運用切割分析於JavaMethod不可切割性之驗證
論文名稱(外文):Verifying the Atomicity of Java Methods using Chopping Analysis
指導教授:徐立群徐立群引用關係
指導教授(外文):Lih-Chyun Shu
學位類別:碩士
校院名稱:國立成功大學
系所名稱:會計學系碩博士班
學門:商業及管理學門
學類:會計學類
論文種類:學術論文
論文出版年:2004
畢業學年度:92
語文別:英文
論文頁數:40
中文關鍵詞:不可切割性並行控制Java切割分析
外文關鍵詞:Chopping AnalysisJavaConcurrency ControlAtomicity
相關次數:
  • 被引用被引用:0
  • 點閱點閱:110
  • 評分評分:系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔系統版面圖檔
  • 下載下載:6
  • 收藏至我的研究室書目清單書目收藏:0
  驗證並行程式的正確性是相當困難的,因為我們無法在靜態的狀況下描繪程式在執行時的行為,Serializability 的理論不僅可用於異動處理上,對於確證並行程式的正確性也很有幫助,本研究的目的在於將原本用於資料庫異動處理的切割分析應用到並行程式分析上,特別是用於驗證Java method 的不可切割性,我們修改了Shasha 等人[SSV92]所提出之chopping graph 的原始定義,使其可以處理lock 的行為,我們也根據修改後的chopping graph 實作出工具,並分析Java 函式庫來顯示此分析的應用性,我們也可說明切割分析(chopping analysis)比起Flanagan 和Qadeer[FQ03a,FQ03b]所提出之type system 來得更精確。
  Reasoning about the correctness of concurrent programs is very difficult, because it is hard to characterize run-time behaviors of concurrent programs statically. Principle of serializability is useful not only for transaction processing, but also beneficial for reasoning about the correctness of concurrent programs. The goal of this research is to adapt the chopping analysis from database
transaction processing to concurrent program analysis, in particular to verify atomicity specification of Java methods. We modify the original definition of chopping graphs due to Shasha et al.[SSV92] by incorporating locks into the graphs. We implement a tool based on our revised chopping graphs and show the applicability of our approach by analyzing some Java libraries. We show that the chopping analysis is more precise than another static analysis—type system proposed by Flanagan and Qadeer.[FQ03b,FQ03a]
Contents
1 Introduction 5
2 Background and Motivation 7
2.1 Database Concurrency Control . . . . . . . . . 7
2.2 Atomicity at the Action Level. . . . . . . . . 9
3 Applying Chopping Analysis to Verify the Atomicity of Java Methods 11
3.1 Revised Chopping Graph . . . . . . . . . . . 11
3.2 Efficiently Generating Useful Information . . . . . . . . . . . 18
4 Tool Construction 22
5 Empirical Studies 28
5.1 Some Non-SR Examples Found in JDK . . . . . . . . . . . 28
5.2 Performance of Our Tool . . . . . . . . . . . . 31
6 Related Work 34
7 Conclusion and Future Work 38
[AG91] J. Anderson and M. Gouda. A criterion for atomicity. Formal Aspects of Computing: The International Journal of Formal Methods, June 1991.
[And99] Gregory R. Andrews. Foundations of Multithreaded, Parallel, and Distributed Programming.
Pearson Addison Wesley, 1999.
[Apa03] The Apache Software Foundation. Byte Code Engineering Library, 2003.
[ASU85] Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques and Tools. Pearson Higher Education, January 1985.
[BHG87] Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, 1987.
[FF00] C. Flanagan and S. N. Freud. Type-based race detection for java. Programming Language Design and Implementation, pages 219–232, 2000.
[FQ03a] Cormac Flanagan and Shaz Qadeer. A type and effect system for atomicity. PLDI03,
June 2003.
[FQ03b] Cormac Flanagan and Shaz Qadeer. Types for atomicity. TLDI03, January 2003.
[Har98] S. Hartly. Concurrent Programming – The Java Programming Language. Oxford University Press, 1998.
[Hsu03] Jiahua Hsu. Concurrent program analysis and concurrency control: Their relationship and synergy. Master’s thesis, National Cheng Kung University, 2003.
[Lea00] Doug Lea. Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley, 2nd edition edition, 2000.
[Lip75] R. Lipton. A method of proving properties of parallel programs. Comm. of the ACM , 18(12), pages 717–721, December 1975.
[OG76] Susan Owicki and David Gries. An axiomatic proof technique for parallel programs i. Acta Informatica, 6:319–340, 1976.
[RND77] Edward M. Reingold, Jurg Nievergelt, and Narsingh Deo. Combinatorial Algorithms : Theory and Practice. Prentice-Hall, 1977.
[SS88] Dennis Shasha and Marc Snir. Efficient and correct execution of parallel programs that share memory. ACM Transaction on Programming Languages and Systems, 10(2):282–312, 1988.
[SSV92] Dennis Shasha, Eric Simon, and Patrick Valduriez. Simple rational guidance for chopping up transactions. Proc. ACM SIGMOD Intl Conf, pages 298–307, June 1992.
[SY95] LihChyun Shu and Michal Young. A generalization of shasha’s chopping graph analysis,1995.
[SY02] LihChyun Shu and Michal Young. Chopping programs. Manuscript in preparation,2002.
[Whi99] David M. Whitelock. The Bloat Book. Secure Software Systems Laboratory, Purdue University, October 1999.
QRCODE
 
 
 
 
 
                                                                                                                                                                                                                                                                                                                                                                                                               
第一頁 上一頁 下一頁 最後一頁 top
無相關論文
 
系統版面圖檔 系統版面圖檔