Verifying Concurrent Programs by Memory Unwinding

详细信息    查看全文

• 作者：Ermenegildo Tomasco (15)
  Omar Inverso (15)
  Bernd Fischer (16)
  Salvatore La Torre (17)
  Gennaro Parlato (15)
  
  15. Electronics and Computer Science ; University of Southampton ; Southampton ; UK
  16. Division of Computer Science ; Stellenbosch University ; Stellenbosch ; South Africa
  17. Universit脿 degli Studi di Salerno ; Salerno ; Italy
  
• 刊名：Lecture Notes in Computer Science
• 出版年：2015
• 出版时间：2015
• 年：2015
• 卷：9035
• 期：1
• 页码：551-565
• 全文大小：267 KB
• 参考文献：1. Alglave, J., Kroening, D., Tautschnig, M. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In: Sharygina, N., Veith, H. eds. (2013) Computer Aided Verification. Springer, Heidelberg, pp. 141-157 CrossRef
  2. Atig, M.F., Bouajjani, A., Parlato, G. Getting rid of store-buffers in TSO analysis. In: Gopalakrishnan, G., Qadeer, S. eds. (2011) Computer Aided Verification. Springer, Heidelberg, pp. 99-115 CrossRef
  3. Beyer, D.: SV-COMP home page, http://sv-comp.sosy-lab.org/
  4. Bouajjani, A., Emmi, M. Bounded phase analysis of message-passing programs. In: Flanagan, C., K枚nig, B. eds. (2012) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Heidelberg, pp. 451-465 CrossRef
  5. Bouajjani, A., Emmi, M., Parlato, G. On Sequentializing Concurrent Programs. In: Yahav, E. eds. (2011) Static Analysis. Springer, Heidelberg, pp. 129-145 CrossRef
  6. Chaki, S., Gurfinkel, A., Strichman, O.: Time-bounded analysis of real-time systems. In: FMCAD, pp. 72鈥?0 (2011)
  7. Clarke, E.M., Kroening, D., Lerda, F. A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. eds. (2004) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Heidelberg, pp. 168-176 CrossRef
  8. Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. POPL, 411鈥?22 (2011)
  9. Fischer, B., Inverso, O., Parlato, G.: CSeq: A Concurrency Pre-Processor for Sequential C Verification Tools. In: ASE, pp. 710-713 (2013)
  10. Fischer, B., Inverso, O., Parlato, G.: CSeq: A Sequentialization Tool for C (Competition Contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.聽7795, pp. 616鈥?18. Springer, Heidelberg (2013)
  11. Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G. Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. eds. (2014) Computer Aided Verification. Springer, Heidelberg, pp. 585-602 CrossRef
  12. Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). In: 脕brah谩m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.聽8413, pp. 398鈥?01. Springer, Heidelberg (2014)
  13. La Torre, S., Madhusudan, P., Parlato, G. Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. eds. (2009) Computer Aided Verification. Springer, Heidelberg, pp. 477-492 CrossRef
  14. Lahiri, S.K., Qadeer, S., Rakamaric, Z. Static and precise detection of concurrency errors in systems code using SMT solvers. In: Bouajjani, A., Maler, O. eds. (2009) Computer Aided Verification. Springer, Heidelberg, pp. 509-524 CrossRef
  15. Lal, A., Qadeer, S., Lahiri, S.K. A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. eds. (2012) Computer Aided Verification. Springer, Heidelberg, pp. 427-443 CrossRef
  16. Lal, A., Reps, T.W. (2009) Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35: pp. 73-97 CrossRef
  17. Lu, S., Park, S., Seo, E., Zhou, Y. (2008) Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. SIGOPS Oper. Syst. Rev. 42: pp. 329-339 CrossRef
  18. Qadeer, S. Poirot - a concurrency sleuth. In: Qin, S., Qiu, Z. eds. (2011) Formal Methods and Software Engineering. Springer, Heidelbergpp. 15 CrossRef
  19. Qadeer, S., Rehof, J. Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. eds. (2005) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Heidelberg, pp. 93-107 CrossRef
  20. Qadeer, S., Wu, D.: Kiss: keep it simple and sequential. In: PLDI, pp. 14鈥?4 (2004)
  21. Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). In: 脕brah谩m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.聽8413, pp. 402鈥?04. Springer, Heidelberg (2014)
  
• 作者单位：Tools and Algorithms for the Construction and Analysis of Systems
• 丛书名：978-3-662-46680-3
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

We describe a new sequentialization-based approach to the symbolic verification of multithreaded programs with shared memory and dynamic thread creation. Its main novelty is the idea of memory unwinding (MU), i.e., a sequence of write operations into the shared memory. For the verification, we nondeterministically guess an MU and then simulate the behavior of the program according to any scheduling that respects it. This approach is complementary to other sequentializations and explores an orthogonal dimension, i.e., the number of write operations. It also simplifies the implementation of several important optimizations, in particular the targeted exposure of individual writes. We implemented this approach as a code-to-code transformation from multithreaded into nondeterministic sequential programs, which allows the reuse of sequential verification tools. Experiments show that our approach is effective: it found all errors in the concurrency category of SV-COMP15.