uu.seUppsala University Publications
Change search
ReferencesLink to record
Permanent link

Direct link
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
IT, 13 085
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-217137OAI: oai:DiVA.org:uu-217137DiVA: diva2:692138
Educational program
Master Programme in Computer Science
Available from: 2014-01-30 Created: 2014-01-30 Last updated: 2014-01-30Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

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

Total: 330 hits
ReferencesLink to record
Permanent link

Direct link