{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:15:45Z","timestamp":1743088545871,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319486277"},{"type":"electronic","value":"9783319486284"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-48628-4_4","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T07:45:31Z","timestamp":1488354331000},"page":"61-91","source":"Crossref","is-referenced-by-count":2,"title":["A Proof Method for Linearizability on TSO Architectures"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Alglave, J., Fox, A., Ishtiaq, S., Myreen, M.O., Sarkar, S., Sewell, P., Nardelli, F.Z.: The semantics of power and arm multiprocessor machine code. In: Petersen, L., Chakravarty, M.M.T. (eds.) DAMP \u201909, pp. 13\u201324. ACM (2008)","DOI":"10.1145\/1481839.1481842"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Amit, D., Rinetzky, N., Reps, T.W., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007, Volume of 4590 LNCS, pp. 477\u2013490. Springer (2007)","DOI":"10.1007\/978-3-540-73368-3_49"},{"key":"4_CR3","volume-title":"Understanding the Linux Kernel","author":"D Bovet","year":"2005","unstructured":"Bovet, D., Cesati, M.: Understanding the Linux Kernel, 3rd edn. O\u2019Reilly, Sebastopol (2005)","edition":"3"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012, volume 7211 of LNCS, pp. 87\u2013107. Springer (2012)","DOI":"10.1007\/978-3-642-28869-2_5"},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis,V.: Modular safety checking for fine-grained concurrency. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007, volume 4634 of LNCS, pp. 233\u2013238. Springer (2007)","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Chase, D., Lev, Y.: Dynamic circular work-stealing deque. In: Gibbons, P.B., Spirakis, P.G. (eds.) SPAA, pp. 21\u201328. ACM (2005)","DOI":"10.1145\/1073970.1073974"},{"key":"4_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4471-5355-9","volume-title":"Refinement in Z and Object-Z: Foundations and Advanced Applications","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and Object-Z: Foundations and Advanced Applications, 2nd edn. Springer, Berlin (2014)","edition":"2"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Proving linearizability via non-atomic refinement. In: Davies, J., Gibbons, J. (eds.) IFM 2007, volume 4591 of LNCS, pp. 195\u2013214. Springer (2007)","DOI":"10.1007\/978-3-540-73210-5_11"},{"issue":"1","key":"4_CR9","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/1889997.1890001","volume":"33","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisabilty with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011, volume 6664 of LNCS, pp. 323\u2013337. Springer (2011)","DOI":"10.1007\/978-3-642-21437-0_25"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: iFM 2014, volume 8739 of LNCS, pp. 341\u2013356 (2014)","DOI":"10.1007\/978-3-319-10181-1_21"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Derrick, J., Smith, G., Groves, l., Dongol, B.: Using coarse-grained abstractions to verify linearizability on TSO architectures. In: HVC2014, volume 8855 of LNCS (2014)","DOI":"10.1007\/978-3-319-13338-6_1"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de\u00a0Frutos-Escrig, D., Nunez, M. (eds.) FORTE 2004, volume 3235 of LNCS, pp. 97\u2013114. Springer (2004)","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Dongol, B., Derrick, J.: Verifying linearisability: a comparative survey. ACM Comput. Surv. 48(2):19:1\u201319:43 (2015)","DOI":"10.1145\/2796550"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M. (ed.) DISC 2012, volume 7611 of LNCS, pp. 31\u201345. Springer (2012)","DOI":"10.1007\/978-3-642-33651-5_3"},{"issue":"3","key":"4_CR16","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":"4_CR17","doi-asserted-by":"crossref","unstructured":"Liu, F., Nedev, N., Prisadnikov, N., Vechev, M.T., Yahav, E.: Dynamic synthesis for relaxed memory models. In: Vitek, J., Lin, H., Tip, F. (eds.) PLDI, pp. 429\u2013440. ACM (2012)","DOI":"10.1145\/2254064.2254115"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Morrison, A., Afek, Y.: Fence-free work stealing on bounded TSO processors. In: ASPLOS, pp. 413\u2013426. ACM (2014)","DOI":"10.1145\/2541940.2541987"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Automated Deduction, pp. 13\u201339. Kluwer (1998)","DOI":"10.1007\/978-94-017-0435-9_1"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic (2014)","DOI":"10.1145\/2629496"},{"issue":"7","key":"4_CR21","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P Sewell","year":"2010","unstructured":"Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Smith, G., Derrick, J., Dongol, B.: Admit your weakness: Verifying correctness on TSO architectures. In: FACS, volume 8997 of LNCS. Springer (2015)","DOI":"10.1007\/978-3-319-15317-9_22"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence. Synthesis Lectures on Computer Architecture. Morgan & Claypool Publishers (2011)","DOI":"10.2200\/S00346ED1V01Y201104CAC016"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.), HVC2013, volume 8244 of LNCS, pp. 311\u2013326. Springer (2013)","DOI":"10.1007\/978-3-319-03077-7_21"},{"key":"4_CR25","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T02:15:47Z","timestamp":1568859347000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_4","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"type":"print","value":"1860-0131"},{"type":"electronic","value":"2197-6597"}],"subject":[],"published":{"date-parts":[[2017]]}}}