Dissertation > Excellent graduate degree dissertation topics show

Certifying Concurrent Porgrams Using Transactional Memory

Author: LiLong
Tutor: ChenYiYun
School: University of Science and Technology of China
Course: Computer Software and Theory
Keywords: software safety concurrency verification assembly language trusted computing base proof-carrying code transactional memory
CLC: TP311.11
Type: PhD thesis
Year: 2008
Downloads: 169
Quote: 1
Read: Download Dissertation

Abstract


The multicore architecture, which has provided infrastructures of better performance, has become popular. To benefit from this growth in performance, programmers are required to develop multi-threaded programs. Whereas it is difficult to ensure correctness for sequential programs, it is even more so for concurrent programs due to the interaction between multiple threads. Traditionally, programmers use locks to achieve mutual exclusion on concurrent access to shared resources. But lock-based programming is difficult to reason about and may lead to problems such as deadlock. Transactional memory (TM) is proposed as an alternate concurrency-control mechanism to avoid many of the pitfalls of the lock-based one. TM systems manage data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound.This dissertation presents a reasoning method for programs using TM and formalizes it into a Hoare-style verification framework. The reasoning method is based on invariance proof and Hoare-style reasoning and supports modular verification. The proof-carrying code (PCC) style framework is proved sound with respect to the TM semantics. And a comparison between lock-based reasoning and TM-based reasoning is presented and shows the convenience of the latter. This dissertation makes the following contributions:It presents a Hoare-style reasoning method to reason about source-level programs using TM. Even though programming using transactions is supposed to reason about easily, there are subtle properties expected by multithreaded programs. To ensure such properties are correctly enforced in a concurrent program, programmers must reason about the behaviors of their programs thoroughly. This dissertation presents a method to perform such TM-based reasoning. And the presented reasoning is based on the same intended semantics of different TM systems: to provide a programming structure that executes atomically and in isolation. This makes the presented reasoning compatible with various TM systems that respect the same intended semantics.It also presents a proof-carrying code style framework to certify the properties of assembly level programs using TM. The presented framework brings PCC into the brand-new TM area. The inference rules of the framework are proved sound with respect to the TM semantics. And examples are also given to illustrate the construction of the proofs for programs in the framework, demonstrating the effectiveness of the framework.The presented framework addresses safety issues at assembly-level directly as PCC systems do. So the complicated and error-prone compilation and optimization do not need to be trusted. And the presented reasoning method is formalize into framework and is sound due to the soundness of the framework. All the work on the framework, including its soundness proof and examples, is mechanized in proof assistant Coq. This makes our work more reliable.Through thorough comparison, it shows the convenience of TM-based reasoning over lock-based reasoning.

Related Dissertations

  1. File Protection System Research Based on Hardware Assisted Virtualization,TP309
  2. Parallel computing software transactional memory programming algorithm research and optimization,TP338.6
  3. Intelligent temperature alarm Research and Design,TP277
  4. Based on the OpenMP Fortran programming language transactional storage and realization of environmental studies,TP333
  5. A Close Stduy of Cohesive Devices Used in C-Einterretation,H315.9
  6. Hardware Transactional Memory Architecture,TP333
  7. Research and Implementation of Embedded Assembly and Pragma Based on IMPACT,TP368.1
  8. Design of high-performance server software memory Affairs,TP368.5
  9. Study on Software Transaction Memory under Multi-thread Condition,TP332
  10. The Research of Anti-Trojan Technology Based JAVA Bytecode,TP393.08
  11. Support for scalable speculative parallelization transactional storage architecture design and performance evaluation,TP333
  12. DICOM image processing technology efficient data,TP391.41
  13. Research on Nested Transactional Memory,TP311.11
  14. Research and Development on Network Assisted Teaching System of Assembly Language Programming Course,TP311.52
  15. PE file encryption Design,TP309.7
  16. ARM-based large-screen LED display system design study,TN873
  17. Research of Inter-Frame Prediction Algorithm of H.264 Video Coding Standard and DSP Implementation,TN919.81
  18. Research on Optimal Design and Implement of DSP-based XVID Video Decoder,TN764
  19. Multi- link structure of city street lights energy-saving micro ultimate wireless controller,TU994
  20. The Realization of HCO Network Operating System with Cx51,TP316.8
  21. Software Development Platform of the Single Chip Microcomputer Based on VC,TP311.52

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Program design,software engineering > Programming > Programming method
© 2012 www.DissertationTopic.Net  Mobile