{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T15:12:47Z","timestamp":1725808367603},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319119359"},{"type":"electronic","value":"9783319119366"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_20","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T19:12:03Z","timestamp":1414177923000},"page":"264-280","source":"Crossref","is-referenced-by-count":0,"title":["Efficiently and Completely Verifying Synchronized Consistency Models"],"prefix":"10.1007","author":[{"given":"Yi","family":"Lv","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luming","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaochun","family":"Ye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dongrui","family":"Fan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peng","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: Baer, J., Snyder, L., Goodman, J.R. (eds.) ISCA 1990, pp. 15\u201326. ACM (1990)","DOI":"10.1145\/325096.325102"},{"issue":"4","key":"20_CR2","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s002240000097","volume":"31","author":"L. Iftode","year":"1998","unstructured":"Iftode, L., Singh, J.P., Li, K.: Scope consistency: A bridge between release consistency and entry consistency. Theory of Computing Systems\u00a031(4), 451\u2013473 (1998)","journal-title":"Theory of Computing Systems"},{"issue":"2","key":"20_CR3","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MM.2012.32","volume":"32","author":"D. Fan","year":"2012","unstructured":"Fan, D., Zhang, H., Wang, D., Ye, X., Song, F., Li, G., Sun, N.: Godson-T: An efficient many-core processor exploring thread-level parallelism. IEEE Micro\u00a032(2), 38\u201347 (2012)","journal-title":"IEEE Micro"},{"issue":"5","key":"20_CR4","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1109\/TCAD.2012.2235914","volume":"32","author":"A. Naeem","year":"2013","unstructured":"Naeem, A., Jantsch, A., Lu, Z.: Scalability analysis of memory consistency models in NoC-based distributed shared memory SoCs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a032(5), 760\u2013773 (2013)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Hansson, A., Goossens, K., Bekooij, M., Huisken, J.: CoMPSoC: A template for composable and predictable multi-processor system on chips. ACM Trans. Des. Autom. Electron. Syst.\u00a014(1), 2:1\u20132:24 (2009)","DOI":"10.1145\/1455229.1455231"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Gibbons, P.B., Korach, E.: On testing cache-coherent shared memories. In: SPAA 1994, pp. 177\u2013188. ACM (1994)","DOI":"10.1145\/181014.181328"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Chen, Y., Lv, Y., Hu, W., Chen, T., Shen, H., Wang, P., Pan, H.: Fast complete memory consistency verification. In: HPCA 2009, pp. 381\u2013392. IEEE Computer Society (2009)","DOI":"10.1109\/HPCA.2009.4798276"},{"issue":"4","key":"20_CR8","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1109\/TC.2011.41","volume":"61","author":"W. Hu","year":"2012","unstructured":"Hu, W., Chen, Y., Chen, T., Qian, C., Li, L.: Linear time memory consistency verification. IEEE Transactions on Computers\u00a061(4), 502\u2013516 (2012)","journal-title":"IEEE Transactions on Computers"},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-1-4615-3604-8_2","volume-title":"Scalable Shared Memory Multiprocessors","author":"P. Sindhu","year":"1992","unstructured":"Sindhu, P., Frailong, J.M., Cekleov, M.: Formal specification of memory models. In: Dubois, M., Thakkar, S. (eds.) Scalable Shared Memory Multiprocessors, US, pp. 25\u201341. Springer, Heidelberg (1992)"},{"issue":"3","key":"20_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2200\/S00346ED1V01Y201104CAC016","volume":"6","author":"D.J. 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\u00a06(3), 1\u2013212 (2011)","journal-title":"Synthesis Lectures on Computer Architecture"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S.V. Adve","year":"1996","unstructured":"Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer\u00a029, 66\u201376 (1996)","journal-title":"IEEE Computer"},{"issue":"5","key":"20_CR12","doi-asserted-by":"publisher","first-page":"800","DOI":"10.1145\/1017460.1017464","volume":"51","author":"C.S. Robert","year":"2004","unstructured":"Robert, C.S., Gary, J.N.: A unified theory of shared memory consistency. J. ACM\u00a051(5), 800\u2013849 (2004)","journal-title":"J. ACM"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Bershad, B., Zekauskas, M., Sawdon, W.: The Midway distributed shared memory system. In: COMPCON 1993. Digest of Papers, pp. 528\u2013537 (1993)","DOI":"10.21236\/ADA264645"},{"issue":"8","key":"20_CR14","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1109\/12.868026","volume":"49","author":"G. Gao","year":"2000","unstructured":"Gao, G., Sarkar, V.: Location consistency: a new memory model and cache consistency protocol. IEEE Transactions on Computers\u00a049(8), 798\u2013813 (2000)","journal-title":"IEEE Transactions on Computers"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-19835-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Alglave","year":"2011","unstructured":"Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running tests against hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 41\u201344. Springer, Heidelberg (2011)"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Park, S., Dill, D.L.: An executable specification, analyzer and verifier for RMO (relaxed memory order). In: SPAA 1995, pp. 34\u201341. ACM (1995)","DOI":"10.1145\/215399.215413"},{"key":"20_CR17","unstructured":"Yang, Y., Gopalakrishnan, G., Lindstrom, G., Slind, K.: Nemos: a framework for axiomatic and executable specifications of memory consistency models. In: IPDPS 2004, pp. 31\u201340. IEEE Computer Society (2004)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-70545-1_12","volume-title":"Computer Aided Verification","author":"S. Burckhardt","year":"2008","unstructured":"Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 107\u2013120. Springer, Heidelberg (2008)"},{"issue":"1","key":"20_CR19","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/TDSC.2007.70243","volume":"6","author":"A. Meixner","year":"2009","unstructured":"Meixner, A., Sorin, D.: Dynamic verification of memory consistency in cache-coherent multithreaded computer architectures. IEEE Transactions on Dependable and Secure Computing\u00a06(1), 18\u201331 (2009)","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"issue":"1","key":"20_CR20","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MM.2007.5","volume":"27","author":"S. Lu","year":"2007","unstructured":"Lu, S., Tucek, J., Qin, F., Zhou, Y.: AVIO: Detecting atomicity violations via access-interleaving invariants. IEEE Micro\u00a027(1), 26\u201335 (2007)","journal-title":"IEEE Micro"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"DeOrio, A., Wagner, I., Bertacco, V.: Dacota: Post-silicon validation of the memory subsystem in multi-core designs. In: HPCA 2009, pp. 405\u2013416. IEEE Computer Society (2009)","DOI":"10.1109\/HPCA.2009.4798278"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Hangal, S., Vahia, D., Manovit, C., Lu, J.Y.J.: TSOtool: A program for verifying memory systems using the memory consistency model. In: ISCA 2004, pp. 114\u2013123. IEEE Computer Society (2004)","DOI":"10.1145\/1028176.1006710"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"Manovit, C., Hangal, S.: Efficient algorithms for verifying memory consistency. In: SPAA 2005, pp. 245\u2013252. ACM (2005)","DOI":"10.1145\/1073970.1074011"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/11817963_46","volume-title":"Computer Aided Verification","author":"A. Roy","year":"2006","unstructured":"Roy, A., Zeisset, S., Fleckenstein, C., Huang, J.: Fast and generalized polynomial time memory consistency verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 503\u2013516. Springer, Heidelberg (2006)"},{"key":"20_CR25","unstructured":"Manovit, C., Hangal, S.: Completely verifying memory consistency of test program executions. In: HPCA 2006, pp. 166\u2013175. IEEE Computer Society (2006)"},{"key":"20_CR26","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: Proceedings of the 4th Workshop on Declarative Aspects of Multicore Programming, DAMP 2009, pp. 13\u201324. ACM (2009)","DOI":"10.1145\/1481839.1481842"},{"key":"20_CR27","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., et al.: An axiomatic memory model for POWER multiprocessors. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 495\u2013512. Springer, Heidelberg (2012)"},{"key":"20_CR28","unstructured":"Lv, Y., Sun, L., Ye, X., Fan, D., Wu, P.: Efficiently and completely verifying synchronized consistency models. Technical Report ISCAS-SKLCS-14-07, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences (2014), \n                  \n                    http:\/\/lcs.ios.ac.cn\/~lvyi\/MODV\/files\/ISCAS-SKLCS-14-07.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,28]],"date-time":"2019-05-28T07:24:32Z","timestamp":1559028272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}