++++++++++++++++++ FME2001: - Review reports for paper 64 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 64 CATEGORY: 1 TITLE: Proofs of Correctness of Cache-Coherence Protocols AUTHOR(S): Joseph Stoy Xiaowei Shen Arvind -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): two proofs of correctness of a cache-coherence protocol. One proof was accomplished using a term-rewriting system and the other was accomplished using a TLA embedding in PVS. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 5 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The authors have developed a new cache-coherence protocol called Cachet which can be tuned on the fly to efficiently execute under different patterns of shared memory usage. The proof approaches are novel. Nice discussion about limits of model checking and potential of semi-automatic approaches. 6. How WORTHWILE is the goal of the authors? Comment: Multi-processor computer systems will certainly become increasingly important. The cache-coherence problem is a thorny one that can greatly benefit from formal verification. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: goal explained well 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: technical parts are sound. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: practical application of hard-core formal verification techniques. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: well written paper. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: yes Are the references correct?: yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 64 CATEGORY: 1 TITLE: Proofs of Correctness of Cache-Coherence Protocols AUTHOR(S): Joseph Stoy Xiaowei Shen Arvind -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The authors describe and compare a manual (term-rewriting) and a machine assisted (PVS) proof of the correctness of cache coherence protocol. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: Some details of the proofs may be useful for people working on similar problems. However, I don't think that conclusions are general, or interesting, enough to be of broad interest. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating of your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 2 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: By verifying the same system twice, using two different technologies, the authors are able to evaluate the benefits of the two. 6. How WORTHWHILE is the goal of the authors? Comment: The goal seems to be the comparison of the two proofs. As such it does highlight relative advantages and disadvantages of machine assisted verification. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: At no point do the authors say that they have a "goal". Rather they "discuss" their experiences. However, their conclusions seem to be justified. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: It appears so. The machine assisted proof is formally verified and is available on the internet. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: Satisfactory arguments and examples are given. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Writing quality OK. I would suggest drawing a clearer conclusion. A more explicit comparison between the manual and machine assisted proofs might be useful. The paper could also be edited for length - the great technical detail made is quite confusing and benefited me little. 11. Were there any formatting or mechanical problems with this paper?: no Are the figures and length acceptable?: the paper is very long (25 pages) Are the references correct?: It appears so 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: Most of the references in the paper to other verification of cache-coherance protocols are pretty old. Two newer references which could be mentioned are "Verifying Sequential consistency on shared-memory multiprocessor systems" by Henzinger, Qadeer and Rajamani (CAV'99) and "Automatic verification of parametrized cache coherence protocols" by Delzanno (CAV '00) (both available on the internet). However, neither of them seem to have direct baring on this work. +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 64 CATEGORY: 1 TITLE: Proofs of Correctness of Cache-Coherence Protocols AUTHOR(S): Joseph Stoy Xiaowei Shen Arvind -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents overview of verification of an adaptive cache-coherence protocol, Cachet which implements the CRF memory model. The proof is first carried out manually. It is then re-formulated in terms of TLA and checked using the PVS theorem prover. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: The paper presents an overview of 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3.5 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: This paper presents overview of theorem prover based verification of a reasonably complex cache coherence protocol. The CRF memory model and its implementation using the Cachet protocol are also briefly presented (before being verified). 6. How WORTHWILE is the goal of the authors? Comment: Paper is interesting as it makes use of a theorem prover to verify Cachet which is reasonably complex cache coherence protocol. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Unfortunately, most details of the verification are missing from the paper, even at an overview level. The raw PVS files used in verification are available on the web but quite hard to read through. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: Moderate. Details of verification are not given even at an overview level. The paper could have given more details of how the quite complex invariant used in the proof was arrived at, and how the bound functions used in liveness proof were found. What I missed most was description of the abstraction function used in the proof of simulation. This can be quite complex. In its present form, by reading this paper there is very little that the reader can carry over to his own proof of a cache coherence protocol. This is the main reason for my low rating. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: The paper plausibly argues in favour of using theorem proving for verifying complex cache-coherence protocols. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: Well written. 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++