Nội dung được dịch bởi AI, chỉ mang tính chất tham khảo
Độ phức tạp tinh vi của xác minh an toàn
Tóm tắt
Chúng tôi nghiên cứu độ phức tạp tinh vi của {Leader Contributor Reachability} ($${\textsf {LCR}} $$) và {Bounded-Stage Reachability} ($${\textsf {BSR}} $$), hai biến thể của bài toán xác minh an toàn cho các chương trình đồng thời sử dụng bộ nhớ chia sẻ. Đối với cả hai bài toán, bộ nhớ là một biến đơn trên miền dữ liệu hữu hạn. Những đóng góp của chúng tôi là các thuật toán xác minh mới và các giới hạn thấp mới. Các giới hạn thấp này dựa trên Giả thuyết Thời gian Đặc biệt ( $${\textsf {ETH}} $$), bài toán {Set Cover} và các thành phần chéo. $${\textsf {LCR}} $$ là câu hỏi liệu một luồng lãnh đạo được chỉ định có thể đạt đến trạng thái không an toàn khi tương tác với một số lượng nhất định các luồng đóng góp bằng nhau hay không. Chúng tôi đề xuất hai thông số hóa: (1) Theo kích thước của miền dữ liệu $${\texttt {D}}$$ và kích thước của lãnh đạo $${\texttt {L}}$$, và (2) theo kích thước của những người đóng góp $${\texttt {C}}$$. Chúng tôi trình bày các thuật toán cho cả hai trường hợp. Các kỹ thuật chính là các nhân chứng nhỏ gọn và lập trình động. Các thuật toán chạy trong thời gian $${\mathcal {O}}^*(({\texttt {L}}\cdot ({\texttt {D}}+1))^{{\texttt {L}}\cdot {\texttt {D}}} \cdot {\texttt {D}}^{{\texttt {D}}})$$ và $${\mathcal {O}}^*(2^{{\texttt {C}}})$$, cho thấy rằng cả hai thông số hóa đều khả thi với tham số cố định. Chúng tôi bổ sung các giới hạn trên bằng các giới hạn dưới (khớp) dựa trên $${\textsf {ETH}} $$ và $${\textsf {Set Cover}} $$ . Hơn nữa, chúng tôi chứng minh sự không tồn tại của các hạt nhân đa thức. Đối với $${\textsf {BSR}} $$, chúng tôi xem xét các chương trình liên quan đến $${\texttt {t}}$$ luồng khác nhau. Chúng tôi hạn chế phân tích vào các tính toán mà quyền viết thay đổi $${\texttt {s}}$$ lần giữa các luồng. $${\textsf {BSR}} $$ đặt ra câu hỏi liệu một cấu hình nhất định có thể đạt được thông qua một tính toán $${\texttt {s}}$$ giai đoạn như vậy hay không. Khi được thông số hóa bởi $${\texttt {P}}$$, kích thước tối đa của một luồng, và $${\texttt {t}}$$, quan sát thú vị là vấn đề này có một số lượng lớn các trường hợp khó. Một cách chính thức, chúng tôi chỉ ra rằng không có hạt nhân đa thức, không có thuật toán nén nào giảm kích thước của miền dữ liệu $${\texttt {D}}$$ hoặc số giai đoạn $${\texttt {s}}$$ theo một phụ thuộc đa thức vào $${\texttt {P}}$$ và $${\texttt {t}}$$. Điều này chỉ ra rằng các phương pháp biểu tượng có thể khó tìm hơn cho vấn đề này.
Từ khóa
#LCR #BSR #xác minh an toàn #độ phức tạp tinh vi #bộ nhớ chia sẻ #thuật toán xác minhTài liệu tham khảo
Atig, M.F., Bouajjani, A., Kumar, K.N., Saivasan, P.: On bounded reachability analysis of shared memory systems. In: FSTTCS, LIPIcs, vol. 29, pp. 611–623. Schloss Dagstuhl (2014)
Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. In: TACAS, LNCS, vol. 5505, pp. 107–123. Springer, Berlin (2009)
Atig, M.F., Bouajjani, A., Touili, T.: On the reachability analysis of acyclic networks of pushdown systems. In: CONCUR, LNCS, vol. 5201, pp. 356–371. Springer, Berlin (2008)
citation_journal_title=Algorithmica; citation_title=Constrained multilinear detection and generalized graph motifs; citation_author=A Björklund, P Kaski, L Kowalik; citation_volume=74; citation_issue=2; citation_publication_date=2016; citation_pages=947-967; citation_doi=10.1007/s00453-015-9981-1; citation_id=CR4
citation_journal_title=JCSS; citation_title=On problems without polynomial kernels; citation_author=HL Bodlaender, RG Downey, MR Fellows, D Hermelin; citation_volume=75; citation_issue=8; citation_publication_date=2009; citation_pages=423-434; citation_id=CR5
citation_journal_title=SIDAM; citation_title=Kernelization lower bounds by cross-composition; citation_author=HL Bodlaender, BMP Jansen, S Kratsch; citation_volume=28; citation_issue=1; citation_publication_date=2014; citation_pages=277-305; citation_doi=10.1137/120880240; citation_id=CR6
Calabro, C., Impagliazzo, R., Paturi, R.: The complexity of satisfiability of small depth circuits. In: IWPEC, LNCS, vol. 5917, pp. 75–85. Springer, Berlin (2009)
Cantin, J.F., Lipasti, M.H., Smith, J.E.: The complexity of verifying memory coherence. In: SPAA, pp. 254–255. ACM (2003)
Chini, P., Kolberg, J., Krebs, A., Meyer, R., Saivasan, P.: On the complexity of bounded context switching. In: ESA, LIPIcs, vol. 87, pp. 27:1–27:15. Schloss Dagstuhl (2017)
Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. In: TACAS, LNCS, vol. 10806, pp. 20–37. Springer, Berlin (2018)
Chini, P., Meyer, R., Saivasan, P.: Fine-grained complexity of safety verification. CoRR 2018.
arXiv:1802.05559
citation_journal_title=ACM TALG; citation_title=On problems as hard as CNF-SAT; citation_author=M Cygan, H Dell, D Lokshtanov, D Marx, J Nederlof, Y Okamoto, R Paturi, S Saurabh, M Wahlström; citation_volume=12; citation_issue=3; citation_publication_date=2016; citation_pages=41:1-41:24; citation_id=CR12
citation_title=Parameterized Algorithms; citation_publication_date=2015; citation_id=CR13; citation_author=M Cygan; citation_author=FV Fomin; citation_author=Ł Kowalik; citation_author=D Lokshtanov; citation_author=D Marx; citation_author=M Pilipczuk; citation_author=M Pilipczuk; citation_author=S Saurabh; citation_publisher=Springer
Demri, S., Laroussinie, F., Schnoebelen, P.: A parametric analysis of the state explosion problem in model checking. In: STACS, LNCS, vol. 2285, pp. 620–631. Springer, Berlin (2002)
citation_title=Fundamentals of Parameterized Complexity; citation_publication_date=2013; citation_id=CR15; citation_author=RG Downey; citation_author=MR Fellows; citation_publisher=Springer
Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. In: CAV, LNCS, vol. 9206, pp. 67–84. Springer, Berlin (2015)
Enea, C., Farzan., A.: On atomicity in presence of non-atomic writes. In: TACAS, LNCS, vol. 9636, pp. 497–514. Springer, Berlin (2016)
Esparza, J., Ganty, P., Majumdar, R.: Parameterized verification of asynchronous shared-memory systems. In: CAV, LNCS, vol. 8044, pp. 124–140. Springer, Berlin (2013)
citation_journal_title=ACM TOPLAS; citation_title=Pattern-based verification for multithreaded programs; citation_author=J Esparza, P Ganty, T Poch; citation_volume=36; citation_issue=3; citation_publication_date=2014; citation_pages=9:1-9:29; citation_doi=10.1145/2629644; citation_id=CR19
Farzan, A., Madhusudan, P.: The complexity of predicting atomicity violations. In: TACAS, LNCS, vol. 5505, pp. 155–169. Springer, Berlin (2009)
citation_journal_title=JCSS; citation_title=A multi-parameter analysis of hard problems on deterministic finite automata; citation_author=H Fernau, P Heggernes, Y Villanger; citation_volume=81; citation_issue=4; citation_publication_date=2015; citation_pages=747-765; citation_id=CR21
Fernau, H., Krebs, A.: Problems on finite automata and the exponential time hypothesis. In: CIAA, LNCS, vol. 9705, pp. 89–100. Springer, Berlin (2016)
Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP, LNCS, vol. 2305, pp. 262–277. Springer, Berlin (2002)
Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN, LNCS, vol. 2648, pp. 213–224. Springer, Berlin (2003)
Fomin, F.V., Kratsch, D., Woeginger, G.J.: Exact (exponential) algorithms for the dominating set problem. In: WG, LNCS, vol. 3353, pp. 245–256. Springer, Berlin (2004)
Fortin, M., Muscholl, A., Walukiewicz, I.: On parametrized verification of asynchronous, shared-memory pushdown systems. CoRR (2016).
arXiv:1606.08707
Fortin, M., Muscholl, A., Walukiewicz, I.: Model-checking linear-time properties of parametrized asynchronous shared-memory pushdown systems. In: CAV, LNCS, vol. 10427, pp. 155–175. Springer, Berlin (2017)
citation_journal_title=JCSS; citation_title=Infeasibility of instance compression and succinct PCPs for NP; citation_author=L Fortnow, R Santhanam; citation_volume=77; citation_issue=1; citation_publication_date=2011; citation_pages=91-106; citation_id=CR28
citation_journal_title=ACM TECS; citation_title=Memory-model-aware testing: A unified complexity analysis; citation_author=F Furbach, R Meyer, K Schneider, M Senftleben; citation_volume=14; citation_issue=4; citation_publication_date=2015; citation_pages=63:1-63:25; citation_id=CR29
citation_journal_title=SIAM J. Comput.; citation_title=Testing shared memories; citation_author=PB Gibbons, E Korach; citation_volume=26; citation_issue=4; citation_publication_date=1997; citation_pages=1208-1244; citation_doi=10.1137/S0097539794279614; citation_id=CR30
Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: PLDI, pp. 266–277. ACM (2007)
Hague, M.: Parameterised pushdown systems with non-atomic writes. In: FSTTCS, LIPIcs, vol. 13, pp. 457–468. Schloss Dagstuhl (2011)
Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: CAV, LNCS, vol. 7358, pp. 260–276. Springer, Berlin (2012)
Holík, L., Meyer, R., Vojnar, T., Wolff, S.: Effect summaries for thread-modular analysis–sound analysis despite an unsound heuristic. In: SAS, LNCS, vol. 10422, pp. 169–191. Springer, Berlin (2017)
citation_journal_title=JCSS; citation_title=On the complexity of k-sat; citation_author=R Impagliazzo, R Paturi; citation_volume=62; citation_issue=2; citation_publication_date=2001; citation_pages=367-375; citation_id=CR35
Kahlon, V.: Parameterization as abstraction: a tractable approach to the dataflow analysis of concurrent programs. In: LICS, pp. 181–192. IEEE (2008)
Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations, The IBM Research Symposia Series, pp. 85–103. Plenum Press (1972)
La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: CAV, LNCS, vol. 6174, pp. 629–644. Springer, Berlin (2010)
Lokshtanov, D., Marx, D., Saurabh, S.: Slightly superexponential parameterized problems. In: SODA, pp. 760–776. SIAM (2011)
Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: TACAS, LNCS, vol. 3440, pp. 93–107. Springer, Berlin (2005)
Wareham, T.: The parameterized complexity of intersection and composition operations on sets of finite-state automata. In: CIAA, LNCS, vol. 2088, pp. 302–310. Springer, Berlin (2000)
citation_journal_title=TCS; citation_title=Some consequences of non-uniform conditions on uniform classes; citation_author=CK Yap; citation_volume=26; citation_publication_date=1983; citation_pages=287-300; citation_doi=10.1016/0304-3975(83)90020-8; citation_id=CR42