{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/18363"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/18363","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Verification and Performance of the DeNovo cache coherence protocol","abstract":"With the advent of multicores, parallel programming has gained a lot of importance. For parallel programming to be viable for the predicted hundreds of cores per chip, shared memory programming languages and environments must evolve to enforce disciplined practices like ``determinism-by-default semantics'' and ban ``wild shared-memory behaviors'' like arbitrary data races and potential non-determinism everywhere. This evolution can not only benefit software development, but can also greatly reduce the complexity in hardware. DeNovo is a hardware architecture designed from the ground up to exploit the opportunities exposed by such disciplined software models to make the hardware much simpler and efficient at the same time. This thesis describes an effort to formally verify and evaluate the DeNovo cache coherence protocol. By using a model checking tool, we uncovered three bugs in the protocol implementation which had not been found either in the testing phase or in the simulation runs. All of these bugs were caused by errors in translating the high level description into the implementation. Surprisingly, we also found six bugs in a state-of-the-art implementation of the widely used MESI protocol. Most of these bugs were hard to analyze and took several days to fix. We provide quantitative evidence that DeNovo is a much simpler protocol by showing that the DeNovo protocol has about 15X fewer reachable states when compared to MESI when using the Murphi model checking tool for verification. This translates to about 20X difference in the runtime of the tool. Finally, we show that this simplicity of the DeNovo protocol does not compromise performance for the applications we evaluated. On the contrary, for some applications, DeNovo achieves up to 67\\% reduction in memory stall time and up to 70\\% reduction in network traffic when compared to MESI.","abstract_html":"With the advent of multicores, parallel programming has gained a lot of importance. For parallel programming to be viable for the predicted hundreds of cores per chip, shared memory programming languages and environments must evolve to enforce disciplined practices like ``determinism-by-default semantics'' and ban ``wild shared-memory behaviors'' like arbitrary data races and potential non-determinism everywhere. This evolution can not only benefit software development, but can also greatly reduce the complexity in hardware. DeNovo is a hardware architecture designed from the ground up to exploit the opportunities exposed by such disciplined software models to make the hardware much simpler and efficient at the same time. This thesis describes an effort to formally verify and evaluate the DeNovo cache coherence protocol. By using a model checking tool, we uncovered three bugs in the protocol implementation which had not been found either in the testing phase or in the simulation runs. All of these bugs were caused by errors in translating the high level description into the implementation. Surprisingly, we also found six bugs in a state-of-the-art implementation of the widely used MESI protocol. Most of these bugs were hard to analyze and took several days to fix. We provide quantitative evidence that DeNovo is a much simpler protocol by showing that the DeNovo protocol has about 15X fewer reachable states when compared to MESI when using the Murphi model checking tool for verification. This translates to about 20X difference in the runtime of the tool. Finally, we show that this simplicity of the DeNovo protocol does not compromise performance for the applications we evaluated. On the contrary, for some applications, DeNovo achieves up to 67\\% reduction in memory stall time and up to 70\\% reduction in network traffic when compared to MESI.","abstract_has_math":false,"creators":["Komuravelli, Rakesh"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Adve, Sarita V."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2011,"date_issued":"2011-01-14T22:47:45Z","date_published":"2011-01-14T22:47:45Z","updated_at":"2026-07-22T22:25:11Z","subjects":["Cache Coherence protocol","software-hardware co-design","multicores","shared memory system","compilers, hardware"],"languages":["en"],"rights":["Copyright 2010 Rakesh Komuravelli"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/18363","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Adve, Sarita V."]},{"key":"dc:creator","label":"Author","values":["Komuravelli, Rakesh"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2011-01-14T22:47:45Z","2010-12"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Cache Coherence protocol","software-hardware co-design","multicores","shared memory system","compilers, hardware"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2010 Rakesh Komuravelli"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/18363"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["With the advent of multicores, parallel programming has gained a lot of importance. For parallel programming to be viable for the predicted hundreds of cores per chip, shared memory programming languages and environments must evolve to enforce disciplined practices like ``determinism-by-default semantics'' and ban ``wild shared-memory behaviors'' like arbitrary data races and potential non-determinism everywhere. This evolution can not only benefit software development, but can also greatly reduce the complexity in hardware. DeNovo is a hardware architecture designed from the ground up to exploit the opportunities exposed by such disciplined software models to make the hardware much simpler and efficient at the same time. This thesis describes an effort to formally verify and evaluate the DeNovo cache coherence protocol. By using a model checking tool, we uncovered three bugs in the protocol implementation which had not been found either in the testing phase or in the simulation runs. All of these bugs were caused by errors in translating the high level description into the implementation. Surprisingly, we also found six bugs in a state-of-the-art implementation of the widely used MESI protocol. Most of these bugs were hard to analyze and took several days to fix. We provide quantitative evidence that DeNovo is a much simpler protocol by showing that the DeNovo protocol has about 15X fewer reachable states when compared to MESI when using the Murphi model checking tool for verification. This translates to about 20X difference in the runtime of the tool. Finally, we show that this simplicity of the DeNovo protocol does not compromise performance for the applications we evaluated. On the contrary, for some applications, DeNovo achieves up to 67\\% reduction in memory stall time and up to 70\\% reduction in network traffic when compared to MESI.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-12-08T15:25:33Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Komuravelli_Rakesh.pdf: 331335 bytes, checksum: fe62075a7e7b9ea3581b8735bd16761a (MD5) Komuravelli_Rakesh.pdf: 327701 bytes, checksum: b1666afc43f7077ef8de9bde38bfb933 (MD5)","Made available in DSpace on 2011-01-14T22:47:45Z (GMT). No. of bitstreams: 2 Komuravelli_Rakesh.pdf: 327736 bytes, checksum: 46a4a6b6bc12b30fa0866d882fd460a9 (MD5) license.txt: 4068 bytes, checksum: 2e6e513e925a804c57795abef7074c1c (MD5)"]},{"key":"dc:title","label":"Title","values":["Verification and Performance of the DeNovo cache coherence protocol"]}]}],"canonical_facts":{"dc:contributor":["Adve, Sarita V."],"dc:creator":["Komuravelli, Rakesh"],"dc:date":["2011-01-14T22:47:45Z","2010-12"],"dc:description":["With the advent of multicores, parallel programming has gained a lot of importance. For parallel programming to be viable for the predicted hundreds of cores per chip, shared memory programming languages and environments must evolve to enforce disciplined practices like ``determinism-by-default semantics'' and ban ``wild shared-memory behaviors'' like arbitrary data races and potential non-determinism everywhere. This evolution can not only benefit software development, but can also greatly reduce the complexity in hardware. DeNovo is a hardware architecture designed from the ground up to exploit the opportunities exposed by such disciplined software models to make the hardware much simpler and efficient at the same time. This thesis describes an effort to formally verify and evaluate the DeNovo cache coherence protocol. By using a model checking tool, we uncovered three bugs in the protocol implementation which had not been found either in the testing phase or in the simulation runs. All of these bugs were caused by errors in translating the high level description into the implementation. Surprisingly, we also found six bugs in a state-of-the-art implementation of the widely used MESI protocol. Most of these bugs were hard to analyze and took several days to fix. We provide quantitative evidence that DeNovo is a much simpler protocol by showing that the DeNovo protocol has about 15X fewer reachable states when compared to MESI when using the Murphi model checking tool for verification. This translates to about 20X difference in the runtime of the tool. Finally, we show that this simplicity of the DeNovo protocol does not compromise performance for the applications we evaluated. On the contrary, for some applications, DeNovo achieves up to 67\\% reduction in memory stall time and up to 70\\% reduction in network traffic when compared to MESI.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2010-12-08T15:25:33Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 2 Komuravelli_Rakesh.pdf: 331335 bytes, checksum: fe62075a7e7b9ea3581b8735bd16761a (MD5) Komuravelli_Rakesh.pdf: 327701 bytes, checksum: b1666afc43f7077ef8de9bde38bfb933 (MD5)","Made available in DSpace on 2011-01-14T22:47:45Z (GMT). No. of bitstreams: 2 Komuravelli_Rakesh.pdf: 327736 bytes, checksum: 46a4a6b6bc12b30fa0866d882fd460a9 (MD5) license.txt: 4068 bytes, checksum: 2e6e513e925a804c57795abef7074c1c (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/18363"],"dc:language":["en"],"dc:rights":["Copyright 2010 Rakesh Komuravelli"],"dc:subject":["Cache Coherence protocol","software-hardware co-design","multicores","shared memory system","compilers, hardware"],"dc:title":["Verification and Performance of the DeNovo cache coherence protocol"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:11Z"}