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

Direct link
Sound and Complete Reachability Analysis under PSO
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.
2013 (English)Independent thesis Basic level (degree of Bachelor), 10 credits / 15 HE creditsStudent thesis
Abstract [en]

Modern multiprocessor systems use weak (relaxed) memory models in order to execute memory sharing multi-threaded code in an efficient manner, but are much harder for programmers to reason about than systems using the sequential consistency memory model.

The SB abstraction and its implementation in the Memorax tool allows sound and complete checking of control state reachability under the TSO memory model, used in modern x86 processors.

In this paper, I present a formalisation of the PSO memory model using the semantics of the Sun SPARC documentation and an alternate semantic, called Partial Write Serialisation, I conjecture to be equivalent with my formalisation under the control state reachability problem. PWS is proved to be a well-structured system which allows sound and complete reachability analysis. An implementation of PWS is presented  as part of the Memorax tool and demonstrated  experimentally to be capable of analysing reachability and inferring minimal fence sets on many non-trivial and real world examples in reasonable time and memory usage.

Place, publisher, year, edition, pages
IT, 13 086
National Category
Engineering and Technology
URN: urn:nbn:se:uu:diva-213286OAI: oai:DiVA.org:uu-213286DiVA: diva2:681505
Educational program
Bachelor Programme in Computer Science
Available from: 2013-12-20 Created: 2013-12-20 Last updated: 2013-12-20Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
Total: 275 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: 270 hits
ReferencesLink to record
Permanent link

Direct link