Verifying a quantitative relaxation of linearizability via refinement
Tóm tắt
The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensuring that the implementation satisfies the quantitative aspect of this new correctness condition is often an arduous task. In this paper, we propose the first automated method for formally verifying quasi linearizability of the implementation model of a concurrent data structure with respect to its sequential specification. The method is based on checking a relaxed version of the refinement relation between the implementation model and the specification model through explicit state model checking. Our method can directly handle concurrent systems where each thread or process makes infinitely many method calls. Furthermore, unlike many existing verification methods, it does not require the user to supply annotations of the linearization points. We have implemented the new method in the PAT verification framework. Our experimental evaluation shows that the method is effective in verifying the new quasi linearizability requirement and detecting violations.
Tài liệu tham khảo
Afek, Y., Korland, G., Yanovsky, E.: Quasi-linearizability: relaxed consistency for improved concurrency. In: International Conference on Principles of Distributed Systems, pp. 395–410 (2010)
Aspnes, J., Herlihy, M., Shavit, N.: Counting networks. J. ACM. 41(5), 1020–1048 (1994)
Attiya, H., Welch, J.: Distributed computing: fundamentals, simulations, and advanced topics, 2nd edn. John Wiley and Sons Inc., Publication, New Jersey (2004)
Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 330–340 (2010)
Cerný, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: International Conference on Computer Aided Verification, pp. 465–479 (2010)
Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: International Conference on Computer Aided Verification, pp. 52–65 (2008)
Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 338–349 (2003)
Ganai, M.K., Arora, N., Wang, C., Gupta, A., Balakrishnan, G.: BEST: A symbolic testing tool for predicting multi-threaded program failures. In: IEEE/ACM International Conference on Automated Software Engineering, (2011)
Haas, A., Lippautz, M., Henzinger, T.A., Payer, H., Sokolova, A., Kirsch, C.M., Sezgin, A.: Distributed queues in shared memory: multicore performance and scalability through quantitative relaxation. In: Conference Computing Frontiers, p. 17 (2013)
Henzinger, T.A., Sezgin, A., Kirsch, C.M., Payer, H., Sokolova, A.:. Quantitative relaxation of concurrent data structures. In: ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 317–328 (2013)
Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann, USA (2008)
Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM. Trans. Program. Lang. Syst. 12(3), 463–492 (1990)
Hoare, C.A.R.: Communicating sequential processes. Prentice Hall, Englewood Cliffs (1985)
Kirsch, C.M. Payer, H.: Incorrect systems: it’s not the problem, it’s the solution. In: Proceedings of the Design Automation Conference, pp. 913–917 (2012)
Kirsch, C.M., Payer, H., Röck, H., Sokolova, A.: Performance, scalability, and semantics of concurrent fifo queues. In: ICA3PP, pp. 273–287 (2012)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE. Trans. Comput. 28(9), 690–691 (1979)
Liu, Y., Chen, W., Liu, Y., Zhang, S., Sun, J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE. Trans. Softw. Eng. (2013)
Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: International Symposium on Formal Methods, pp. 321–337 (2009)
Lynch, N.: Distributed algorithms. Morgan Kaufmann, USA (1997)
Michael, M.M., Vechev, M.T., Saraswat, V.A.: Idempotent work stealing. In: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Raleigh, pp. 45–54 (2009)
Payer, H., Röck, H., Kirsch, C.M., Sokolova, A.: Scalability versus semantics of concurrent fifo queues. In: ACM Symposium on Principles of Distributed Computing, pp. 331–332 (2011)
Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: NASA Formal Methods, pp. 313–327 (2011)
Sinha, A., Malik, S., Wang, C., Gupta, A.: Predicting serializability violations: SMT-based search vs. DPOR-based search. In: Haifa Verification Conference, pp. 95–114 (2011)
Sinha, A., Malik, S., Wang, C., Gupta, A.: Predictive analysis for detecting serializability violations through trace segmentation. In: Formal Methods and Models for Codesign, pp. 99–108 (2011)
Sinha, N., Wang, C.: Staged concurrent program analysis. In: ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 47–56 (2010)
Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: International Symposium on Theoretical Aspects of Software Engineering, pp. 127–135 (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: International Conference on Computer Aided Verification, pp. 709–714 (2009)
Treiber, R.K.: Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)
Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 335–348 (2009)
Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 129–136 (2006)
Vechev, M.T., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: International SPIN Workshop on Model Checking Software, pp. 261–278 (2009)
Vogels, W.: Eventually consistent. Commun. ACM. 52(1), 40–44 (2009)
Wang, C., Ganai, M.: Predicting concurrency failures in generalized traces of x86 executables. In: International Conference on Runtime Verification (2011)
Wang, C., Hoang, K.: Precisely deciding control state reachability in concurrent traces with limited observability. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 376–394 (2014)
Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods, pp. 256–272 (2009)
Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 328–342 (2010)
Wang, C., Yang, Y., Gupta, A., Gopalakrishnan, G.: Dynamic model checking with property driven pruning to detect race conditions. In: International Symposium on Automated Technology for Verification and Analysis, pp. 126–140 (2008)
Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE. Trans. Softw. Eng. 32(2), 93–110 (2006)
Zhang, L., Chattopadhyay, A., Wang, C.: Round-Up: Runtime checking quasi linearizability of concurrent data structures. In: IEEE/ACM International Conference on Automated Software Engineering, pp. 4–14 (2013)
Zhang, L., Wang, C.: Runtime prevention of concurrency related type-state violations in multithreaded applications. In: International Symposium on Software Testing and Analysis, pp. 1–12 (2014)