Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Thread-Modular Model Checking of Concurrent Programs under TSO using Code Rewriting
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.
2010 (English)Independent thesis Advanced level (degree of Master (One Year)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

Model checking is a well understood method for verifying correctness of concurrent programs. Commonly instructions in the verified programs are assumed to be executed in the order they occur in the programs. Most actual architectures, however, perform a number of optimizations when executing a program. Some such optimizations have the effect of reordering instructions or making the instructions appear to be reordered. The possible code reorderings are governed by the architecture's memory model. The particular memory model considered in this text is called TSO and is used on for example Intel x86 and SPARC V9.

A method for verifying safety properties of concurrent programs under TSO by model checking is presented. The method works by exploring the set of reachable program states to verify that certain predefined error states can never be reached.

The main optimization allowed by TSO is storing write instructions in an on-processor write buffer and later writing through the value to memory asynchronously with the other program instructions. Rather than concretely modelling the write buffers of a TSO architecture, the state exploration described in this paper works by successively rewriting the code of the program being analysed. The rewriting closely corresponds to the instruction reordering analogy sometimes used when describing the semantics of memory models.

An extension of the method is also given, which allows verification of safety properties for programs with an unbounded number of threads.

Place, publisher, year, edition, pages
2010.
Series
IT ; 10 068
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-145240OAI: oai:DiVA.org:uu-145240DiVA, id: diva2:395705
Educational program
Master Programme in Computer Science
Uppsok
Technology
Supervisors
Examiners
Projects
Weak Memory ModelsUPMARCAvailable from: 2011-02-07 Created: 2011-02-07 Last updated: 2011-10-10Bibliographically approved

Open Access in DiVA

fulltext(542 kB)426 downloads
File information
File name FULLTEXT01.pdfFile size 542 kBChecksum SHA-512
3e4dcee6bb319e7235c10bc85f29cd6bf6f0e3e855cf068c38af8252e5bceddde89a2d8c6f6c010d7dda4c84862f4f18fe9cd8f6c1a68ad2748e2fdb091cd2d2
Type fulltextMimetype application/pdf

By organisation
Division of Computer Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 426 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 791 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf