{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:28:29Z","timestamp":1725888509388},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319602240"},{"type":"electronic","value":"9783319602257"}],"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_3","type":"book-chapter","created":{"date-parts":[[2017,5,27]],"date-time":"2017-05-27T02:26:37Z","timestamp":1495851997000},"page":"33-49","source":"Crossref","is-referenced-by-count":3,"title":["Modularising Opacity Verification for Hybrid Transactional Memory"],"prefix":"10.1007","author":[{"given":"Alasdair","family":"Armstrong","sequence":"first","affiliation":[]},{"given":"Brijesh","family":"Dongol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,28]]},"reference":[{"key":"3_CR1","unstructured":"Armstrong, A., Dongol, B.: Isabelle files for modularising opacity verification for hybrid transactional memory (2016). https:\/\/figshare.com\/articles\/Isabelle_files_for_verification_of_a_hybrid_transactional_mutex_lock\/4868351"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Calciu, I., Gottschlich, J., Shpeisman, T., Pokam, G., Herlihy, M.: Invyswell: a hybrid transactional memory for Haswell\u2019s restricted transactional memory. In: PACT, pp. 187\u2013200. ACM, New York (2014)","DOI":"10.1145\/2628071.2628086"},{"issue":"3","key":"3_CR3","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1145\/1961296.1950373","volume":"46","author":"L Dalessandro","year":"2011","unstructured":"Dalessandro, L., Carouge, F., White, S., Lev, Y., Moir, M., Scott, M.L., Spear, M.F.: Hybrid NOrec: a case study in the effectiveness of best effort hardware transactional memory. SIGPLAN Not. 46(3), 39\u201352 (2011)","journal-title":"SIGPLAN Not."},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15291-7_2","volume-title":"Euro-Par 2010 - Parallel Processing","author":"L Dalessandro","year":"2010","unstructured":"Dalessandro, L., Dice, D., Scott, M., Shavit, N., Spear, M.: Transactional mutex locks. In: D\u2019Ambra, P., Guarracino, M., Talia, D. (eds.) Euro-Par 2010. LNCS, vol. 6272, pp. 2\u201313. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-15291-7_2"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-19249-9_11","volume-title":"FM 2015: Formal Methods","author":"J Derrick","year":"2015","unstructured":"Derrick, J., Dongol, B., Schellhorn, G., Travkin, O., Wehrheim, H.: Verifying opacity of a transactional mutex lock. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 161\u2013177. Springer, Cham (2015). doi: 10.1007\/978-3-319-19249-9_11"},{"key":"3_CR6","unstructured":"Doherty, S., Dongol, B., Derrick, J., Schellhorn, G., Wehrheim, H.: Proving opacity of a pessimistic STM. In: Jim\u00e9nez, E. (ed.) OPODIS (2016, to appear)"},{"issue":"5","key":"3_CR7","doi-asserted-by":"crossref","first-page":"769","DOI":"10.1007\/s00165-012-0225-8","volume":"25","author":"S Doherty","year":"2013","unstructured":"Doherty, S., Groves, L., Luchangco, V., Moir, M.: Towards formally specifying and verifying transactional memory. Formal Asp. Comput. 25(5), 769\u2013799 (2013)","journal-title":"Formal Asp. Comput."},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Guerraoui, R., Kapalka, M.: On the correctness of transactional memory. In: Chatterjee, S., Scott, M.L. (eds.) PPOPP, pp. 175\u2013184. ACM (2008)","DOI":"10.1145\/1345206.1345233"},{"key":"3_CR9","series-title":"Synthesis Lectures on Distributed Computing Theory","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-02002-5","volume-title":"Principles of Transactional Memory","author":"R Guerraoui","year":"2010","unstructured":"Guerraoui, R., Kapalka, M.: Principles of Transactional Memory. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, San Rafael (2010)"},{"key":"3_CR10","series-title":"Synthesis Lectures on Computer Architecture","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01728-5","volume-title":"Transactional Memory","author":"T Harris","year":"2010","unstructured":"Harris, T., Larus, J.R., Rajwar, R.: Transactional Memory. Synthesis Lectures on Computer Architecture, 2nd edn. Morgan & Claypool Publishers, San Rafael (2010)","edition":"2"},{"key":"3_CR11","unstructured":"Intel: Intel 64 and IA-32 Architectures Software Developers Manual (2016)"},{"issue":"4","key":"3_CR12","doi-asserted-by":"crossref","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR13","unstructured":"Lesani, M.: On the correctness of transactional memory algorithms. Ph.D. thesis, UCLA (2014)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-642-32940-1_36","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M Lesani","year":"2012","unstructured":"Lesani, M., Luchangco, V., Moir, M.: A framework for formally verifying software transactional memory algorithms. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 516\u2013530. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32940-1_36"},{"key":"3_CR15","unstructured":"Lesani, M., Luchangco, V., Moir, M.: Putting opacity in its place. In: Workshop on the Theory of Transactional Memory (2012)"},{"key":"3_CR16","volume-title":"Distributed Algorithms","author":"NA Lynch","year":"1996","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann, Burlington (1996)"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC, pp. 137\u2013151. ACM (1987)","DOI":"10.1145\/41840.41852"},{"issue":"4","key":"3_CR18","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1145\/2775054.2694393","volume":"50","author":"A Matveev","year":"2015","unstructured":"Matveev, A., Shavit, N.: Reduced hardware NOrec: a safe and scalable hybrid transactional memory. SIGPLAN Not. 50(4), 59\u201371 (2015)","journal-title":"SIGPLAN Not."},{"key":"3_CR19","volume-title":"Isabelle - A Generic Theorem Prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle - A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994). (with a contribution by Nipkow, T.)"},{"key":"3_CR20","series-title":"Cambridge Tracts in Theoretical Computer Science","volume-title":"Concurrency Verification: Introduction to Compositional and Noncompositional Methods","author":"WP Roever de","year":"2001","unstructured":"de Roever, W.P., de Boer, F.S., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, New York (2001)"}],"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_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,28]],"date-time":"2022-07-28T22:26:49Z","timestamp":1659047209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-60225-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319602240","9783319602257"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-60225-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}