{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T01:49:34Z","timestamp":1769046574898,"version":"3.49.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319602240","type":"print"},{"value":"9783319602257","type":"electronic"}],"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-60225-7_8","type":"book-chapter","created":{"date-parts":[[2017,5,27]],"date-time":"2017-05-27T02:26:37Z","timestamp":1495851997000},"page":"108-123","source":"Crossref","is-referenced-by-count":3,"title":["An Observational Approach to Defining Linearizability on Weak Memory Models"],"prefix":"10.1007","author":[{"given":"John","family":"Derrick","sequence":"first","affiliation":[]},{"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,28]]},"reference":[{"key":"8_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 2009, pp. 13\u201324. ACM (2008)","DOI":"10.1145\/1481839.1481842"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-540-73368-3_49","volume-title":"Computer Aided Verification","author":"D Amit","year":"2007","unstructured":"Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477\u2013490. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-73368-3_49"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-28869-2_5","volume-title":"Programming Languages and Systems","author":"S Burckhardt","year":"2012","unstructured":"Burckhardt, S., Gotsman, A., Musuvathi, M., Yang, H.: Concurrent library correctness on the TSO memory model. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 87\u2013107. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28869-2_5"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-540-74061-2_15","volume-title":"Static Analysis","author":"C Calcagno","year":"2007","unstructured":"Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233\u2013248. Springer, Heidelberg (2007). doi: 10.1007\/978-3-540-74061-2_15"},{"issue":"1","key":"8_CR5","doi-asserted-by":"crossref","first-page":"4:1","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:1\u20134:43 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-642-21437-0_25","volume-title":"FM 2011: Formal Methods","author":"J Derrick","year":"2011","unstructured":"Derrick, J., Schellhorn, G., Wehrheim, H.: Verifying linearisability with potential linearisation points. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 323\u2013337. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-21437-0_25"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-19249-9_12","volume-title":"FM 2015: Formal Methods","author":"J Derrick","year":"2015","unstructured":"Derrick, J., Smith, G.: A framework for correctness criteria on weak memory models. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 178\u2013194. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_12"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-319-10181-1_21","volume-title":"Integrated Formal Methods","author":"J Derrick","year":"2014","unstructured":"Derrick, J., Smith, G., Dongol, B.: Verifying linearizability on TSO architectures. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 341\u2013356. Springer, Cham (2014). doi: 10.1007\/978-3-319-10181-1_21"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-540-30232-2_7","volume-title":"Formal Techniques for Networked and Distributed Systems \u2013 FORTE 2004","author":"S Doherty","year":"2004","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: Frutos-Escrig, D., N\u00fa\u00f1ez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97\u2013114. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30232-2_7"},{"issue":"5","key":"8_CR10","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1145\/1941487.1941501","volume":"54","author":"J Fitzpatrick","year":"2011","unstructured":"Fitzpatrick, J.: An interview with Steve Furber. Commun. ACM 54(5), 34\u201339 (2011)","journal-title":"Commun. ACM"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/978-3-642-33651-5_3","volume-title":"Distributed Computing","author":"A Gotsman","year":"2012","unstructured":"Gotsman, A., Musuvathi, M., Yang, H.: Show no weakness: sequentially consistent specifications of TSO libraries. In: Aguilera, M.K. (ed.) DISC 2012. LNCS, vol. 7611, pp. 31\u201345. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33651-5_3"},{"issue":"3","key":"8_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":"8_CR13","unstructured":"Maranget, L., Sarkar, S., Sewell, P.: A tutorial introduction to the ARM and POWER relaxed memory models (2012). Draft available from http:\/\/www.cl.cam.ac.uk\/~pes20\/ppc-supplemental\/test7.pdf"},{"key":"8_CR14","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"},{"issue":"4","key":"8_CR15","doi-asserted-by":"crossref","first-page":"31:1","DOI":"10.1145\/2629496","volume":"15","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Wehrheim, H., Derrick, J.: A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Log. 15(4), 31:1\u201331:37 (2014)","journal-title":"ACM Trans. Comput. Log."},{"issue":"7","key":"8_CR16","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":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-319-15317-9_22","volume-title":"Formal Aspects of Component Software","author":"G Smith","year":"2015","unstructured":"Smith, G., Derrick, J., Dongol, B.: Admit your weakness: verifying correctness on TSO architectures. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol. 8997, pp. 364\u2013383. Springer, Cham (2015). doi: 10.1007\/978-3-319-15317-9_22"},{"key":"8_CR18","series-title":"Synthesis Lectures on Computer Architecture","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01733-9","volume-title":"A Primer on Memory Consistency and Cache Coherence","author":"DJ Sorin","year":"2011","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, San Rafael (2011)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-319-03077-7_21","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2013","unstructured":"Travkin, O., M\u00fctze, A., Wehrheim, H.: SPIN as a linearizability checker under weak memory models. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol. 8244, pp. 311\u2013326. Springer, Cham (2013). doi: 10.1007\/978-3-319-03077-7_21"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-13338-6_11","volume-title":"Hardware and Software: Verification and Testing","author":"O Travkin","year":"2014","unstructured":"Travkin, O., Wehrheim, H.: Handling TSO in mechanized linearizability proofs. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 132\u2013147. Springer, Cham (2014). doi: 10.1007\/978-3-319-13338-6_11"},{"key":"8_CR21","unstructured":"Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-60225-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,23]],"date-time":"2023-08-23T19:32:14Z","timestamp":1692819134000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-60225-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319602240","9783319602257"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-60225-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}