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

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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
Precise and sound automatic fence insertion procedure under PSO
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0003-4993-0092
2015 (English)In: Networked Systems: NETYS 2015, Springer, 2015, p. 32-47Conference paper, Published paper (Refereed)
Abstract [en]

We give a sound and complete procedure for fence insertion for concurrent finite-state programs running under the PSO memory model. This model allows ''write to read'' and ''write-to-write'' relaxations corresponding to the addition of an unbounded store buffers between processors and the main memory. We introduce a novel machine model, called the Hierarchical Single-Buffer (HSB) semantics, and show that the reachability problem for a program under PSO can be reduced to the reachability problem under HSB. We present a simple and effective backward reachability analysis algorithm for the latter, and propose a counter-example guided fence insertion procedure. The procedure infers automatically a minimal set of fences that ensure correctness of the program. We have implemented a prototype and run it successfully on all standard benchmarks, together with several challenging examples.

Place, publisher, year, edition, pages
Springer, 2015. p. 32-47
Series
Lecture Notes in Computer Science ; 9466
Keywords [en]
PSO, weak memory model, well-quasi order, well-structured transition system, concurrent program, verification
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-253647DOI: 10.1007/978-3-319-26850-7_3ISBN: 978-3-319-26849-1 (print)OAI: oai:DiVA.org:uu-253647DiVA, id: diva2:815352
Conference
NETYS 2015, May 13–15, Agadir, Morocco
Projects
UPMARCAvailable from: 2016-03-23 Created: 2015-05-29 Last updated: 2018-11-20

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Abdulla, Parosh AzizAtig, Mohamed FaouziNgo, Tuan Phong

Search in DiVA

By author/editor
Abdulla, Parosh AzizAtig, Mohamed FaouziNgo, Tuan Phong
By organisation
Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 1174 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • 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