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
The benefits of duality in verifying concurrent programs under TSO
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
2016 (English)In: 27th International Conference on Concurrency Theory: CONCUR 2016, Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2016, p. 5:1-15Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of verifying safety properties of concurrent programs running over the Total Store Order (TSO) memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove the correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes.

In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO semantics that is more amenable to efficient algorithmic verification and for the extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the safety analysis under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows obtaining a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.

Place, publisher, year, edition, pages
Dagstuhl, Germany: Leibniz-Zentrum für Informatik , 2016. p. 5:1-15
Series
Leibniz International Proceedings in Informatics (LIPIcs), ISSN 1868-8969 ; 59
Keywords [en]
Total Store Order, Weak Memory Models, Reachability Problem, Parameterized Systems, Well-quasi-ordering
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-298663DOI: 10.4230/LIPIcs.CONCUR.2016.5ISBN: 978-3-95977-017-0 (print)OAI: oai:DiVA.org:uu-298663DiVA, id: diva2:946791
Conference
CONCUR 2016, August 23–26, Québec City, Canada
Projects
UPMARCAvailable from: 2016-08-16 Created: 2016-07-06 Last updated: 2018-11-20

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full texthttp://drops.dagstuhl.de/opus/volltexte/2016/6171/pdf/LIPIcs-CONCUR-2016-5.pdf

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: 936 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