Digitala Vetenskapliga Arkivet

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
Verification under Intel-x86 with Persistency
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology.ORCID iD: 0000-0001-6832-6611
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computer Systems.ORCID iD: 0000-0001-8229-3481
Univ Paris Cite, Paris, France..
Chennai Math Inst, Chennai, Tamil Nadu, India.;IRL ReLaX, Chennai, Tamil Nadu, India..
Show others and affiliations
2024 (English)In: Proceedings of the ACM on Programming Languages, E-ISSN 2475-1421, Vol. 8, no PLDI, article id 195Article in journal (Refereed) Published
Abstract [en]

The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2024. Vol. 8, no PLDI, article id 195
Keywords [en]
model checking, program verification, TSO memory model, persistency
National Category
Computer Sciences Computer Systems Embedded Systems
Identifiers
URN: urn:nbn:se:uu:diva-536369DOI: 10.1145/3656425ISI: 001264464100050OAI: oai:DiVA.org:uu-536369DiVA, id: diva2:1890779
Conference
ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI), JUN 24-28, 2024, Copenhagen, DENMARK
Funder
Swedish Research Council, P-04/2019Swedish Research CouncilAvailable from: 2024-08-20 Created: 2024-08-20 Last updated: 2024-08-20Bibliographically approved

Open Access in DiVA

fulltext(1371 kB)72 downloads
File information
File name FULLTEXT01.pdfFile size 1371 kBChecksum SHA-512
3b6aa223e12a2ce288adc2ffc5a9b8e3309c6d95d4b49e66ad06917f6f89acaf687b63757f71fb83cc7afdf2ee5c8bc6b12a4a8f35933c5b443ea8693679b7c3
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Search in DiVA

By author/editor
Abdulla, ParoshAtig, Mohamed Faouzi
By organisation
Department of Information TechnologyDivision of Computer Systems
In the same journal
Proceedings of the ACM on Programming Languages
Computer SciencesComputer SystemsEmbedded Systems

Search outside of DiVA

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

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 350 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