Context-bounded analysis for POWER

(creator_code:org_t)

2017-03-31
2017
English.
In: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer. - 9783662545799 ; , s. 56-74

Related links:: https://link.springe...; show more...; https://urn.kb.se/re...; https://doi.org/10.1...; show less...

Abstract Subject headings

We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded analysis initiated by Qadeer et al. in 2005 for detecting bugs in concurrent programs (supposed to be running under the classical SC model). To that end, we first introduce a new notion of context-bounding that is suitable for reasoning about computations under POWER, which generalizes the one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a polynomial size reduction of the context-bounded state reachability problem under POWER to the same problem under SC: Given an input concurrent program P, our method produces a concurrent program P' such that, for a fixed number of context switches, running P' under SC yields the same set of reachable states as running P under POWER. The generated program P' contains the same number of processes as P and operates on the same data domain. By leveraging the standard model checker CBMC, we have implemented a prototype tool and applied it on a set of benchmarks, showing the feasibility of our approach.

By the author/editor: Abdulla, Parosh ...; Atig, Mohamed Fa ...; Bouajjani, Ahmed; Ngo, Tuan Phong

About the subject

ENGINEERING AND TECHNOLOGY: ENGINEERING AND ...; and Electrical Engin ...; and Computer Systems

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.