Verification under Intel-x86 with PersistencyShow 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 Council2024-08-202024-08-202024-08-20Bibliographically approved