TY - GEN
T1 - Reachability in concurrent uninterpreted programs
AU - Torre, Salvatore La
AU - Parthasarathy, Madhusudan
N1 - Acknowledgements This material is based upon work supported by the National Science Foundation under Grant CCF-1527395, GNCS 2019 grant and MIUR-FARB 2018-19 grant.
PY - 2019/12
Y1 - 2019/12
N2 - We study the safety verification (reachability problem) for concurrent programs with uninterpreted functions/relations. By extending the notion of coherence, recently identified for sequential programs, to concurrent programs, we show that reachability in coherent concurrent programs under various scheduling restrictions is decidable by a reduction to multistack pushdown automata, and establish precise complexity bounds for them. We also prove that the coherence restriction for these various scheduling restrictions is itself a decidable property.
AB - We study the safety verification (reachability problem) for concurrent programs with uninterpreted functions/relations. By extending the notion of coherence, recently identified for sequential programs, to concurrent programs, we show that reachability in coherent concurrent programs under various scheduling restrictions is decidable by a reduction to multistack pushdown automata, and establish precise complexity bounds for them. We also prove that the coherence restriction for these various scheduling restrictions is itself a decidable property.
KW - Concurrent programs
KW - Shared memory
KW - Uninterpreted programs
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85077467272&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85077467272&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.FSTTCS.2019.46
DO - 10.4230/LIPIcs.FSTTCS.2019.46
M3 - Conference contribution
AN - SCOPUS:85077467272
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019
A2 - Chattopadhyay, Arkadev
A2 - Gastin, Paul
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019
Y2 - 11 December 2019 through 13 December 2019
ER -