{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:53Z","timestamp":1762459553641},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319680330"},{"type":"electronic","value":"9783319680347"}],"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-68034-7_4","type":"book-chapter","created":{"date-parts":[[2017,9,13]],"date-time":"2017-09-13T17:32:45Z","timestamp":1505323965000},"page":"58-77","source":"Crossref","is-referenced-by-count":3,"title":["A Formal Model of Parallel Execution on Multicore Architectures with Multilevel Caches"],"prefix":"10.1007","author":[{"given":"Shiji","family":"Bijo","sequence":"first","affiliation":[]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[]},{"given":"Ka I","family":"Pun","sequence":"additional","affiliation":[]},{"given":"Silvia Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,9,14]]},"reference":[{"issue":"12","key":"4_CR1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"SV Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: a tutorial. IEEE Comput. 29(12), 66\u201376 (1996)","journal-title":"IEEE Comput."},{"issue":"2","key":"4_CR2","doi-asserted-by":"crossref","first-page":"7:1","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M., Cats, H.: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36(2), 7:1\u20137:74 (2014)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-319-44802-2_3","volume-title":"Rewriting Logic and Its Applications","author":"S Bijo","year":"2016","unstructured":"Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: A Maude framework for cache coherent multicore architectures. In: Lucanu, D. (ed.) WRLA 2016. LNCS, vol. 9942, pp. 47\u201363. Springer, Cham (2016). doi: 10.1007\/978-3-319-44802-2_3"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: An operational semantics of cache coherent multicore architectures. In: Proceedings of Symposium Applied Computing (SAC). ACM (2016)","DOI":"10.1145\/2851613.2851718"},{"key":"4_CR5","unstructured":"Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: A formal model of parallel execution in multicore architectures with multilevel caches (long version). Res. rep., Department of Informatics, University of Oslo (2017). http:\/\/violet.at.ifi.uio.no\/papers\/mc-rr.pdf"},{"issue":"2","key":"4_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2024716.2024718","volume":"39","author":"N Binkert","year":"2011","unstructured":"Binkert, N., et al.: The gem5 simulator. SIGARCH Comput. Archit. News 39(2), 1\u20137 (2011)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Carlson, T.E., Heirman, W., Eeckhout, L.: Sniper: exploring the level of abstraction for scalable and accurate parallel multi-core simulation. In: Proceedings of High Performance Computing, Networking, Storage and Analysis (SC), pp. 52:1\u201352:12. ACM (2011)","DOI":"10.1145\/2063384.2063454"},{"key":"4_CR8","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, vol. 4350. Springer, Heidelberg (2007)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Crary, K., Sullivan, M.J.: A calculus for relaxed memory. In: Proceedings of Principles of Programming Languages (POPL), pp. 623\u2013636. ACM (2015)","DOI":"10.1145\/2676726.2676984"},{"key":"4_CR10","volume-title":"Parallel Computer Architecture: A Hardware\/Software Approach","author":"DE Culler","year":"1997","unstructured":"Culler, D.E., Gupta, A., Singh, J.P.: Parallel Computer Architecture: A Hardware\/Software Approach. Morgan Kaufmann, San Francisco (1997)"},{"issue":"3","key":"4_CR11","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1023\/A:1026276129010","volume":"23","author":"G Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. Formal Meth. Syst. Des. 23(3), 257\u2013301 (2003)","journal-title":"Formal Meth. Syst. Des."},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proceedings of Computer Design on VLSI in Computer Processors (ICCD). IEEE (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"4_CR13","unstructured":"Dill, D.L., Park, S., Nowatzyk, A.G.: Formal specification of abstract memory models. In: Proceedings of Symposium Research on Integrated Systems, pp. 38\u201352. MIT Press (1993)"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-39718-9_11","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"B Dongol","year":"2013","unstructured":"Dongol, B., Travkin, O., Derrick, J., Wehrheim, H.: A high-level semantics for program execution under total store order memory. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 177\u2013194. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39718-9_11"},{"key":"4_CR15","volume-title":"Computer Architecture: A Quantitative Approach","author":"JL Hennessy","year":"2011","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach. Morgan Kaufmann, San Francisco (2011)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-11957-6_17","volume-title":"Programming Languages and Systems","author":"R Jagadeesan","year":"2010","unstructured":"Jagadeesan, R., Pitcher, C., Riely, J.: Generative operational semantics for relaxed memory models. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 307\u2013326. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-11957-6_17"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-25271-6_8"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Kandemir, M., et al.: Improving locality using loop and data transformations in an integrated framework. In: Proceedings of ACM\/IEEE International Symposium on Microarchitecture (1998)","DOI":"10.1109\/MICRO.1998.742790"},{"issue":"9","key":"4_CR19","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":"4_CR20","doi-asserted-by":"crossref","unstructured":"Li, Y., Suhendra, V., Liang, Y., Mitra, T., Roychoudhury, A.: Timing analysis of concurrent programs running on shared cache multi-cores. In: Proceedings of Real-Time Systems Symposium (RTSS), pp. 57\u201367. IEEE (2009)","DOI":"10.1109\/RTSS.2009.32"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-642-31424-7_36","volume-title":"Computer Aided Verification","author":"S Mador-Haim","year":"2012","unstructured":"Mador-Haim, S., Maranget, L., Sarkar, S., Memarian, K., Alglave, J., Owens, S., Alur, R., Martin, M.M.K., Sewell, P., Williams, D.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 495\u2013512. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_36"},{"issue":"4","key":"4_CR22","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/1105734.1105747","volume":"33","author":"MMK Martin","year":"2005","unstructured":"Martin, M.M.K., et al.: Multifacet\u2019s general execution-driven multiprocessor simulator (GEMS) toolset. SIGARCH Comput. Archit. News 33(4), 92\u201399 (2005)","journal-title":"SIGARCH Comput. Archit. News"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-54624-2_7","volume-title":"Specification, Algebra, and Software","author":"\u00d3 Mart\u00edn","year":"2014","unstructured":"Mart\u00edn, \u00d3., Verdejo, A., Mart\u00ed-Oliet, N.: Model checking TLR* guarantee formulas on infinite systems. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 129\u2013150. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54624-2_7"},{"issue":"1","key":"4_CR24","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theor. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Miller, J.E., et al.: Graphite: a distributed parallel simulator for multicores. In: Proceedings of the High-Performance Computer Architecture (HPCA), pp. 1\u201312. IEEE (2010)","DOI":"10.1109\/HPCA.2010.5416635"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Nita, M., Grossman, D., Chambers, C.: A theory of platform-dependent low-level software. In: Proceedings of the Principles of Programming Languages (POPL), pp. 209\u2013220. ACM (2008)","DOI":"10.1145\/1328438.1328465"},{"issue":"1","key":"4_CR27","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.jlap.2006.08.007","volume":"71","author":"J Pang","year":"2007","unstructured":"Pang, J., Fokkink, W., Hofman, R.F.H., Veldema, R.: Model checking a cache coherence protocol of a Java DSM implementation. J. Log. Algeb. Prog. 71(1), 1\u201343 (2007)","journal-title":"J. Log. Algeb. Prog."},{"key":"4_CR28","unstructured":"Patterson, D.A., Hennessy, J.L.: Computer Organization and Design: The Hardware\/Software Interface. Morgan Kaufmann (2013)"},{"key":"4_CR29","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algeb. Prog. 60\u201361, 17\u2013139 (2004)","journal-title":"J. Log. Algeb. Prog."},{"issue":"1","key":"4_CR30","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F Pong","year":"1997","unstructured":"Pong, F., Dubois, M.: Verification techniques for cache coherence protocols. ACM Comput. Surv. 29(1), 82\u2013126 (1997)","journal-title":"ACM Comput. Surv."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Ram\u00edrez, S., Rocha, C.: Formal verification of safety properties for a cache coherence protocol. In: Proceedings of the Colombian Computing Conference (10CCC), pp. 9\u201316. IEEE (2015)","DOI":"10.1109\/ColumbianCC.2015.7333399"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Proceedings of PLDI, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993498.1993520"},{"issue":"7","key":"4_CR33","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_CR34","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":"4_CR35","doi-asserted-by":"crossref","unstructured":"Solihin, Y.: Fundamentals of Parallel Multicore Architecture. Chapman & Hall\/CRC (2015)","DOI":"10.1201\/b20200"},{"key":"4_CR36","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. Morgan & Claypool, San Francisco (2011)"},{"key":"4_CR37","unstructured":"Yu, X., Vijayaraghavan, M., Devadas, S.: A proof of correctness for the Tardis cache coherence protocol. CoRR, abs\/1505.06459 (2015)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68034-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,25]],"date-time":"2023-08-25T20:34:56Z","timestamp":1692995696000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68034-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319680330","9783319680347"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68034-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}