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
Ensuring The Correctness of Concurrent Programs under TSO Memory Models
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2013 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesis
Abstract [en]

For efficiency reasons, most modern processor architectures allow the reordering of CPU instructions, resulting in weak memory models. These models add extra program executions that are not intended by the programmer, often causing subtle run-time errors.  To help solve this problem, such architectures also provide memory fences that allow to eliminate undesired behaviors. However, manual fence insertion, is a tedious and time- consuming activity, that also needs to be repeated each time the program is updated. Therefore, the development of efficient tools for automatic fence insertion is a crucial challenge in concurrent program design.

In this thesis, we present, for the first time, a tool for automatic fence placement that is able to break the scalability barrier both concerning the added complexity due to the presence of event reorderings, and also concerning the number of threads that participate in the execution of the program. To this end, we propose a novel notion of correctness  for concurrent  programs, called persistence, that compares the behavior of the program under the weak memory semantics with that under the classical interleaving semantics.

To make our ideas concrete, we consider the Total Store Ordering (TSO) memory model, and show how our method (i) allows modular reasoning that limits state space explosion due to the presence of parallel processes (threads), and (ii) abstracts away complex behaviors caused by weak memory models by translating the problem, in linear time, into a verification problem that is defined under the interleaving semantics. We have implemented a prototype  and run it successfully on all standard benchmarks, together with several challenging examples that are beyond the capability of existing methods.

Place, publisher, year, edition, pages
2013.
Series
IT, 13 085
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-217137OAI: oai:DiVA.org:uu-217137DiVA: diva2:692138
Educational program
Master Programme in Computer Science
Supervisors
Examiners
Available from: 2014-01-30 Created: 2014-01-30 Last updated: 2014-01-30Bibliographically approved

Open Access in DiVA

fulltext(1218 kB)238 downloads
File information
File name FULLTEXT01.pdfFile size 1218 kBChecksum SHA-512
8457df596fbf20f13404b55dedbeb6b4fb93f17f1da898d45167b3d85429de81b07bf2203adfdfe320dc9aa725e209329af52690f9f873825c2ebb030554801b
Type fulltextMimetype application/pdf

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 238 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: 540 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