{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,3]],"date-time":"2022-06-03T21:51:11Z","timestamp":1654293071855},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,3,18]],"date-time":"2015-03-18T00:00:00Z","timestamp":1426636800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,8]]},"DOI":"10.1007\/s10009-015-0373-2","type":"journal-article","created":{"date-parts":[[2015,3,17]],"date-time":"2015-03-17T13:42:14Z","timestamp":1426599734000},"page":"393-407","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying a quantitative relaxation of linearizability via refinement"],"prefix":"10.1007","volume":"18","author":[{"given":"Kiran","family":"Adhikari","sequence":"first","affiliation":[]},{"given":"James","family":"Street","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Shaojie","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,3,18]]},"reference":[{"key":"373_CR1","doi-asserted-by":"crossref","unstructured":"Afek, Y., Korland, G., Yanovsky, E.: Quasi-linearizability: relaxed consistency for improved concurrency. In: International Conference on Principles of Distributed Systems, pp. 395\u2013410 (2010)","DOI":"10.1007\/978-3-642-17653-1_29"},{"issue":"5","key":"373_CR2","doi-asserted-by":"crossref","first-page":"1020","DOI":"10.1145\/185675.185815","volume":"41","author":"J Aspnes","year":"1994","unstructured":"Aspnes, J., Herlihy, M., Shavit, N.: Counting networks. J. ACM. 41(5), 1020\u20131048 (1994)","journal-title":"J. ACM."},{"key":"373_CR3","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed computing: fundamentals, simulations, and advanced topics","author":"H Attiya","year":"2004","unstructured":"Attiya, H., Welch, J.: Distributed computing: fundamentals, simulations, and advanced topics, 2nd edn. John Wiley and Sons Inc., Publication, New Jersey (2004)","edition":"2"},{"key":"373_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013340 (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"373_CR5","doi-asserted-by":"crossref","unstructured":"Cern\u00fd, 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\u2013479 (2010)","DOI":"10.1007\/978-3-642-14295-6_41"},{"key":"373_CR6","doi-asserted-by":"crossref","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: International Conference on Computer Aided Verification, pp. 52\u201365 (2008)","DOI":"10.1007\/978-3-540-70545-1_8"},{"key":"373_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Qadeer, S.: A type and effect system for atomicity. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 338\u2013349 (2003)","DOI":"10.1145\/780822.781169"},{"key":"373_CR8","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1109\/ASE.2011.6100134"},{"key":"373_CR9","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2482767.2482789"},{"key":"373_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013328 (2013)","DOI":"10.1145\/2429069.2429109"},{"key":"373_CR11","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The art of multiprocessor programming. Morgan Kaufmann, USA (2008)"},{"issue":"3","key":"373_CR12","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM. Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM. Trans. Program. Lang. Syst."},{"key":"373_CR13","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Prentice Hall, Englewood Cliffs (1985)"},{"key":"373_CR14","doi-asserted-by":"crossref","unstructured":"Kirsch, C.M. Payer, H.: Incorrect systems: it\u2019s not the problem, it\u2019s the solution. In: Proceedings of the Design Automation Conference, pp. 913\u2013917 (2012)","DOI":"10.1145\/2228360.2228523"},{"key":"373_CR15","doi-asserted-by":"crossref","unstructured":"Kirsch, C.M., Payer, H., R\u00f6ck, H., Sokolova, A.: Performance, scalability, and semantics of concurrent fifo queues. In: ICA3PP, pp. 273\u2013287 (2012)","DOI":"10.1007\/978-3-642-33078-0_20"},{"issue":"9","key":"373_CR16","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"28","author":"L Lamport","year":"1979","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE. Trans. Comput. 28(9), 690\u2013691 (1979)","journal-title":"IEEE. Trans. Comput."},{"key":"373_CR17","doi-asserted-by":"crossref","unstructured":"Liu, Y., Chen, W., Liu, Y., Zhang, S., Sun, J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE. Trans. Softw. Eng. (2013)","DOI":"10.1109\/TSE.2012.82"},{"key":"373_CR18","doi-asserted-by":"crossref","unstructured":"Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model checking linearizability via refinement. In: International Symposium on Formal Methods, pp. 321\u2013337 (2009)","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"373_CR19","volume-title":"Distributed algorithms","author":"N Lynch","year":"1997","unstructured":"Lynch, N.: Distributed algorithms. Morgan Kaufmann, USA (1997)"},{"key":"373_CR20","doi-asserted-by":"crossref","unstructured":"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\u201354 (2009)","DOI":"10.1145\/1594835.1504186"},{"key":"373_CR21","doi-asserted-by":"crossref","unstructured":"Payer, H., R\u00f6ck, H., Kirsch, C.M., Sokolova, A.: Scalability versus semantics of concurrent fifo queues. In: ACM Symposium on Principles of Distributed Computing, pp. 331\u2013332 (2011)","DOI":"10.1145\/1993806.1993869"},{"key":"373_CR22","doi-asserted-by":"crossref","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an SMT-based analysis. In: NASA Formal Methods, pp. 313\u2013327 (2011)","DOI":"10.1007\/978-3-642-20398-5_23"},{"key":"373_CR23","doi-asserted-by":"crossref","unstructured":"Sinha, A., Malik, S., Wang, C., Gupta, A.: Predicting serializability violations: SMT-based search vs. DPOR-based search. In: Haifa Verification Conference, pp. 95\u2013114 (2011)","DOI":"10.1007\/978-3-642-34188-5_11"},{"key":"373_CR24","doi-asserted-by":"crossref","unstructured":"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\u2013108 (2011)","DOI":"10.1109\/MEMCOD.2011.5970516"},{"key":"373_CR25","doi-asserted-by":"crossref","unstructured":"Sinha, N., Wang, C.: Staged concurrent program analysis. In: ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 47\u201356 (2010)","DOI":"10.1145\/1882291.1882301"},{"key":"373_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013135 (2009)","DOI":"10.1109\/TASE.2009.32"},{"key":"373_CR27","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: International Conference on Computer Aided Verification, pp. 709\u2013714 (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"373_CR28","unstructured":"Treiber, R.K.: Systems programming: coping with parallelism. Technical Report RJ 5118, IBM Almaden Research Center (1986)"},{"key":"373_CR29","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 335\u2013348 (2009)","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"373_CR30","doi-asserted-by":"crossref","unstructured":"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\u2013136 (2006)","DOI":"10.1145\/1122971.1122992"},{"key":"373_CR31","doi-asserted-by":"crossref","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: International SPIN Workshop on Model Checking Software, pp. 261\u2013278 (2009)","DOI":"10.1007\/978-3-642-02652-2_21"},{"issue":"1","key":"373_CR32","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1145\/1435417.1435432","volume":"52","author":"W Vogels","year":"2009","unstructured":"Vogels, W.: Eventually consistent. Commun. ACM. 52(1), 40\u201344 (2009)","journal-title":"Commun. ACM."},{"key":"373_CR33","doi-asserted-by":"crossref","unstructured":"Wang, C., Ganai, M.: Predicting concurrency failures in generalized traces of x86 executables. In: International Conference on Runtime Verification (2011)","DOI":"10.1007\/978-3-642-29860-8_2"},{"key":"373_CR34","doi-asserted-by":"crossref","unstructured":"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\u2013394 (2014)","DOI":"10.1007\/978-3-642-54013-4_21"},{"key":"373_CR35","doi-asserted-by":"crossref","unstructured":"Wang, C., Kundu, S., Ganai, M., Gupta, A.: Symbolic predictive analysis for concurrent programs. In: International Symposium on Formal Methods, pp. 256\u2013272 (2009)","DOI":"10.1007\/978-3-642-05089-3_17"},{"key":"373_CR36","doi-asserted-by":"crossref","unstructured":"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\u2013342 (2010)","DOI":"10.1007\/978-3-642-12002-2_27"},{"key":"373_CR37","doi-asserted-by":"crossref","unstructured":"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\u2013140 (2008)","DOI":"10.1007\/978-3-540-88387-6_11"},{"issue":"2","key":"373_CR38","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/TSE.2006.1599419","volume":"32","author":"L Wang","year":"2006","unstructured":"Wang, L., Stoller, S.D.: Runtime analysis of atomicity for multithreaded programs. IEEE. Trans. Softw. Eng. 32(2), 93\u2013110 (2006)","journal-title":"IEEE. Trans. Softw. Eng."},{"key":"373_CR39","doi-asserted-by":"crossref","unstructured":"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\u201314 (2013)","DOI":"10.1109\/ASE.2013.6693061"},{"key":"373_CR40","doi-asserted-by":"crossref","unstructured":"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\u201312 (2014)","DOI":"10.1145\/2610384.2610405"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0373-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0373-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0373-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T02:33:43Z","timestamp":1566441223000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0373-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,18]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,8]]}},"alternative-id":["373"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0373-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,18]]}}}