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
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
2013.
Series
IT, 13 086
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-213286OAI: oai:DiVA.org:uu-213286DiVA: diva2:681505
Educational program
Bachelor Programme in Computer Science
Supervisors
Examiners
Available from: 2013-12-20 Created: 2013-12-20 Last updated: 2013-12-20Bibliographically approved

Open Access in DiVA

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

By organisation
Department of Information Technology
Engineering and Technology

Search outside of DiVA

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