Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.10423 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929215848316928 |
|---|---|
| author | Abdulla, Parosh Aziz Atig, Mohamed Faouzi Furbach, Florian Garg, Shashwat |
| author_facet | Abdulla, Parosh Aziz Atig, Mohamed Faouzi Furbach, Florian Garg, Shashwat |
| contents | We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable). In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_10423 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Verification under TSO with an infinite Data Domain Abdulla, Parosh Aziz Atig, Mohamed Faouzi Furbach, Florian Garg, Shashwat Formal Languages and Automata Theory Programming Languages We examine verification of concurrent programs under the total store ordering (TSO) semantics used by the x86 architecture. In our model, threads manipulate variables over infinite domains and they can check whether variables are related for a range of relations. We show that, in general, the control state reachability problem is undecidable. This result is derived through a reduction from the state reachability problem of lossy channel systems with data (which is known to be undecidable). In the light of this undecidability, we turn our attention to a more tractable variant of the reachability problem. Specifically, we study context bounded runs, which provide an under-approximation of the program behavior by limiting the possible interactions between processes. A run consists of a number of contexts, with each context representing a sequence of steps where a only single designated thread is active. We prove that the control state reachability problem under bounded context switching is PSPACE complete. |
| title | Verification under TSO with an infinite Data Domain |
| topic | Formal Languages and Automata Theory Programming Languages |
| url | https://arxiv.org/abs/2401.10423 |