++++++++++++++++++ FME2001: - Review reports for paper 04 +++++++++++++++++++++ - 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: 04 CATEGORY: unspecified TITLE: Some Relations for Communication and Parallelism Elimination and Introduction on Declarative Programs AUTHOR(S): Miquel Bertran Francesc Babot August Climent Miquel Nicolau -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Program transformation rules are defined and proven correct for the elimination of communication in SPL. It is proven that for this purpose no finite set of rules suffices. The approach is illustrated by some simple examples. 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: Although program transformation rules are a valid topic for FME, both the rules and the examples presented here are too simple to be interesting. 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: 1 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: Minor, the rules introduced are simple, I cannot imagine how they could be applied to obtain really interesting transformations, especially simplifications. This is reflected in Section 5 where only trivial examples are presented. 6. How WORTHWILE is the goal of the authors? Comment: The topic of program transformation rules is worthwhile by itself; however, this paper does not convince 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: This is my severest point of critique. As a researcher in the field of concurrency, specification and verification, with some knowledge of SPL, I consider myself as a typical representative of the FME audience. Although I took the time to reread relevant sections from the books by Manna and Pnueli I was not able to understand the details of proofs given in this paper. The style of proofs is informal at best; proofs might be understandable for someone really well-versed in SPL, but the average reader will not be able to read and understand about half of the paper. More specifically, the paper presents a three-page overview of SPL where lots of constructs are introduced that do not play a role in the paper, while other essential constructs like fairness and 'pres(U)' are barely touched. As a result I am not able to understand the final sentence in Proof 1 (p.7) where it is claimed that 'P[a<=T] always terminates ... but P[a<=T;skip] has a non-terminating computation' Explain this! I did not have the time to check the proofs in this paper; the informal style of proofs requires me to write out the underlying definitions and proof steps, a pleasure I will happily leave to the other referees. However, I consider this more a weakness of the paper than a weakness of yours truly. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: As motivated under 7, I did not check the proofs in detail. However, the paper contains a great deal of sloppyness: - Title: 'relations' is too vague a notion, the paper is about rules of inference or rules of transformation that are sound with respect to the equivalence relation defined on programs. - Title: 'declarative programs' is wrong: the paper is about SPL and I don't consider this declarative. - Introduction (p.2): 'our approach is general and can be adapted to ... model checkers' I think this giant leap from theorem proving to model checking needs justification. - Introduction (p.3): 'Notice that the relations which have been used do not hold in SPL' This suggests the inference is not sound. What I hope is meant is something like 'Our transformation rules are new' - Section 3 (p.6): 'Congruences for...' suggests that somehow the equivalence of programs is redefined. Again, 'rules' could be better. - Section 3.1 (p.6): The permutation rules are a logical consequence of the easier to formulate and easier to prove associativity and commutativity - Section 3.2 (p.7): That fact that some rules do not hold belongs in a remark instead of in a lemma. Also, I think the point can be illustrated by a simpler example. As noted above, I don't understand this example: explain! - Section 5. (p.15): The examples seem to demonstrate that simple programs can be made complex by parallellisation? - Section 5.1 (p.15): 'Observe that the laws ... have to be used as well, together with SOME SIMPLE CHANNEL INTRODUCTION LAW' What law? 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: It is suggested that the rules introduced are applicable to program transformations; however, no convincing evidence is presented. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: - Terminology: maintain a clear distinction between syntax, with things like rules and unification and, on the other hand, semantics, with relations and congruences. - Typos: use a spell checker, a quick check reveals about 20 typos. - Abstract: the final sentence suggests a recursive algorith is introduced; the final sentence of the introduction reveals it is not. - Introduction (p.3 top): 'the same communication elimination' must be 'a similar...' - Section 2: Either focus on results and benefits, referring to the details in a technical report, or focus on a subset of SPL and give exact definitions and proofs. You cannot do it all in a mere 20 pages. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: I cannot find a reference to [Hoa78]; there are some typos like 'Mnchen' in [Broy99] and 'Forma Aspects' in [Hoo94] 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: 04 CATEGORY: 2 TITLE: Some Relations for Communication and Parallelism Elimination and Introduction on Declarative Programs AUTHOR(S): Miquel Bertran Francesc Babot August Climent Miquel Nicolau -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper describes congruences and refinements between statements of a declerative programming language (the paper uses SPL, but it should be applicable to other languages). These congruences allow to modify programs to equivalent ones while introducing or removing parallelism and synchronous communication, preserving the correctness of any previously verified property. 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: I do not know whether the transformations presented in the paper are of much use in practice. 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 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: What is new is elimination and introduction of parallelism and synchronous communication for declarative programs, as opposed to similar work which has been done for process algebras and action based systems. The signficance is to save verification work done on programs which are equivalent to programs which have already been verified previously. 6. How WORTHWILE is the goal of the authors? Comment: It is worthwhile, however, the presentation seems very specific to SPL. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: It is explained well, and justified with examples. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper is very technical containing numerous rigorous proofs. The technical quality if very good. 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 work is applicable. For example, one can define a simplilfied version of the traget program. This simplified version is easy to verify. After this, parallelism and synchronous communication can be introduced to derive the program which is really required. The final program is known to be correct without the need to repeat the (more complex) verification process. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The presentation is of high quality, in structure, language. Spelling typo: Page 15 line 7 from the end: change "obseve" to "observe" 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: I found no problems. 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 ++++++++++++++++++++++