Fine-Grained Complexity of Safety Verification.
Saved in:
| Title: | Fine-Grained Complexity of Safety Verification. |
|---|---|
| Authors: | Chini, Peter1 p.chini@tu-bs.de, Meyer, Roland1, Saivasan, Prakash1 |
| Source: | Journal of Automated Reasoning. Oct2020, Vol. 64 Issue 7, p1419-1444. 26p. |
| Subjects: | Dynamic programming, Functional programming languages, Machine learning, Polynomials, Software verification |
| Abstract: | We study the fine-grained complexity of Leader Contributor Reachability (LCR ) and Bounded-Stage Reachability (BSR ), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis (ETH ), the problem Set Cover , and cross-compositions. LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain D and the size of the leader L , and (2) by the size of the contributors C . We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in O ∗ ((L · (D + 1)) L · D · D D) and O ∗ (2 C) time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on ETH and Set Cover . Moreover, we prove the absence of polynomial kernels. For BSR , we consider programs involving t different threads. We restrict the analysis to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s -stage computation. When parameterized by P , the maximum size of a thread, and t , the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain D or the number of stages s to a polynomial dependence on P and t . This indicates that symbolic methods may be harder to find for this problem. [ABSTRACT FROM AUTHOR] |
| Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 146105255 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Fine-Grained Complexity of Safety Verification. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Chini%2C+Peter%22">Chini, Peter</searchLink><relatesTo>1</relatesTo><i> p.chini@tu-bs.de</i><br /><searchLink fieldCode="AR" term="%22Meyer%2C+Roland%22">Meyer, Roland</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Saivasan%2C+Prakash%22">Saivasan, Prakash</searchLink><relatesTo>1</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Journal+of+Automated+Reasoning%22">Journal of Automated Reasoning</searchLink>. Oct2020, Vol. 64 Issue 7, p1419-1444. 26p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Dynamic+programming%22">Dynamic programming</searchLink><br /><searchLink fieldCode="DE" term="%22Functional+programming+languages%22">Functional programming languages</searchLink><br /><searchLink fieldCode="DE" term="%22Machine+learning%22">Machine learning</searchLink><br /><searchLink fieldCode="DE" term="%22Polynomials%22">Polynomials</searchLink><br /><searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: We study the fine-grained complexity of Leader Contributor Reachability (LCR ) and Bounded-Stage Reachability (BSR ), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis (ETH ), the problem Set Cover , and cross-compositions. LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain D and the size of the leader L , and (2) by the size of the contributors C . We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in O ∗ ((L · (D + 1)) L · D · D D) and O ∗ (2 C) time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on ETH and Set Cover . Moreover, we prove the absence of polynomial kernels. For BSR , we consider programs involving t different threads. We restrict the analysis to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s -stage computation. When parameterized by P , the maximum size of a thread, and t , the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain D or the number of stages s to a polynomial dependence on P and t . This indicates that symbolic methods may be harder to find for this problem. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Journal of Automated Reasoning is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=146105255 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10817-020-09572-x Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 26 StartPage: 1419 Subjects: – SubjectFull: Dynamic programming Type: general – SubjectFull: Functional programming languages Type: general – SubjectFull: Machine learning Type: general – SubjectFull: Polynomials Type: general – SubjectFull: Software verification Type: general Titles: – TitleFull: Fine-Grained Complexity of Safety Verification. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Chini, Peter – PersonEntity: Name: NameFull: Meyer, Roland – PersonEntity: Name: NameFull: Saivasan, Prakash IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 10 Text: Oct2020 Type: published Y: 2020 Identifiers: – Type: issn-print Value: 01687433 Numbering: – Type: volume Value: 64 – Type: issue Value: 7 Titles: – TitleFull: Journal of Automated Reasoning Type: main |
| ResultId | 1 |
