Verifying a Quantitative Relaxation of Linearizability via Refinement
详细信息 查看全文
- 作者：Kiran Adhikari (18)
James Street (18)
Chao Wang (18)
Yang Liu (19)
ShaoJie Zhang (20) - 刊名：Lecture Notes in Computer Science
- 出版年：2013
- 出版时间：2013
- 年：2013
- 卷：7976
- 期：1
- 页码：43-60
- 全文大小：665KB
- 参考文献：1. Afek, Y., Korland, G., Yanovsky, E.: Quasi-Linearizability: Relaxed consistency for improved concurrency. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol.聽6490, pp. 395鈥?10. Springer, Heidelberg (2010) CrossRef
2. Aspnes, J., Herlihy, M., Shavit, N.: Counting networks. J. ACM聽41(5), 1020鈥?048 (1994) CrossRef
3. Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics, 2nd edn. John Wiley & Sons, Inc., Publication (2004)
4. Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: PLDI, pp. 330鈥?40 (2010)
5. 膶ern媒, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.聽6174, pp. 465鈥?79. Springer, Heidelberg (2010) CrossRef
6. Farzan, A., Madhusudan, P.: Causal atomicity. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.聽4144, pp. 315鈥?28. Springer, Heidelberg (2006) CrossRef
7. Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.聽5123, pp. 52鈥?5. Springer, Heidelberg (2008) CrossRef
8. Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: PLDI, pp. 338鈥?49 (2003)
9. Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann (2008)
10. Herlihy, M., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst.聽12(3), 463鈥?92 (1990) CrossRef
11. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)
12. Kirsch, C.M., Payer, H., R枚ck, H., Sokolova, A.: Performance, scalability, and semantics of concurrent FIFO queues. In: Xiang, Y., Stojmenovic, I., Apduhan, B.O., Wang, G., Nakano, K., Zomaya, A. (eds.) ICA3PP 2012, Part I. LNCS, vol.聽7439, pp. 273鈥?87. Springer, Heidelberg (2012) CrossRef
13. Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Computers聽28(9), 690鈥?91 (1979) CrossRef
14. Liu, Y., Chen, W., Liu, Y., Zhang, S., Sun, J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Transactions on Software Engineering (2013)
15. Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.聽5850, pp. 321鈥?37. Springer, Heidelberg (2009) CrossRef
16. Lynch, N.: Distributed Algorithms. Morgan Kaufmann (1997)
17. Payer, H., R枚ck, H., Kirsch, C.M., Sokolova, A.: Scalability versus semantics of concurrent fifo queues. In: PODC, pp. 331鈥?32 (2011)
18. Sadowski, C., Freund, S.N., Flanagan, C.: Singletrack: A dynamic determinism checker for multithreaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.聽5502, pp. 394鈥?09. Springer, Heidelberg (2009) CrossRef
19. Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: TASE, pp. 127鈥?35 (2009)
20. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.聽5643, pp. 709鈥?14. Springer, Heidelberg (2009) CrossRef
21. Treiber, R.K.: Systems Programming: Coping with Parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)
22. Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., M眉ller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.聽5403, pp. 335鈥?48. Springer, Heidelberg (2009) CrossRef
23. Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: P膬s膬reanu, C.S. (ed.) SPIN 2009. LNCS, vol.聽5578, pp. 261鈥?78. Springer, Heidelberg (2009) CrossRef
24. Vogels, W.: Eventually consistent. Commun. ACM聽52(1), 40鈥?4 (2009) CrossRef
25. Wang, C., Limaye, R., Ganai, M., Gupta, A.: Trace-based symbolic analysis for atomicity violations. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.聽6015, pp. 328鈥?42. Springer, Heidelberg (2010) CrossRef
26. Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE Trans. Software Eng.聽32(2), 93鈥?10 (2006) CrossRef - 作者单位：Kiran Adhikari (18)
James Street (18)
Chao Wang (18)
Yang Liu (19)
ShaoJie Zhang (20)
18. Virginia Tech, Blacksburg, Virginia, USA
19. Nanyang Technological University, Singapore
20. Singapore University of Technology and Design, Singapore - ISSN：1611-3349
文摘
Concurrent data structures have found increasingly widespread use in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a relaxation of linearizability to allow more implementation freedom for performance optimization. However, ensuring the quantitative aspects of this correctness condition is an arduous task. We propose a new method for formally verifying quasi linearizability of the implementation model of a concurrent data structure. The method is based on checking the refinement relation between the implementation and a specification model via explicit state model checking. It can directly handle concurrent programs where each thread can make infinitely many method calls, and it does not require the user to write annotations for the linearization points. We have implemented and evaluated our method in the PAT verification framework. Our experiments show that the method is effective in verifying quasi linearizability or detecting its violations.