{p}S0{r}, {r} {S1 ... Sn} {q} ---------------------------------- {p} {S0 S1 ... Sn} {q} {p}S0{r} -------- {p}{S0}{r} > Given a statement, a pair of pre- and post-conditions and a set of assumptions, a... why not just "Given a Hoare triple, ..." What is the set of assumptions? In Fig. 2.2, explain what are X and Y. (symolic constants?) What is the purpose of them? Are they necessary? Fig. 2.2: I think you meant y=abs(x) for the conclusion, and everywhere else within the proof. Not x=abs(y). Fig. 2.2: overfull hbox. Maybe get rid of some of the white space, like y:=x instead of y = x You could use the standard notation for abs(x), |x| to save space. This is OK since it is in a formula, not code. Fig 2.2 even after the fix (y=abs(x)), the derivation is not strictly correct. 1.2 is not an instance of the assignment rule. x<0 is not the result of substituting -x for y in x=|y|. x=|-x| is. (or -x=|x| after the fix). Example 2.1: it says "C code" but it is not C. Say the final formula equivalent to "true", so the original triple is valid. >"Design by ContractTM (DbC) a methodology originated with Hoare logic. It was coined by Bertrand Meyer in [68]" First sentence is missing a verb. Maybe: Design by Contracts (DbC) is a methodology developed by Bertrand Meyer for ....\footnote{The term was trademarked and the trademark is now owned by Eiffel Software}. >The idea of DbC is to use pre- and post-conditions to document, as well as check the >correctness of, program procedures. In Eifel and Bertrand's work, I think there is a lot more to it that pre and post conditions. Class invariants are very emphasized because it is all about object oriented design. There may be other kinds of invarinats. And of course frame conditions. "Other than Eiffel": not sure what this means. I would just delete this sentence and start the next paragraph with: "Contracts are widely used in deductive program verification tools". Fig. 2.3: overfull hbox, and there is no need for it. the box just needs to be shrunk Again, it should be y=|x|. ---- > Both of them at the same time also refer to the deductive verifiers that can prove the functional correctness of Why3 and Boogie programs respectively. Need a comma before "respectively". > A number of verification tools for higher level programming languages are built on top of Why3 and Boogie, such as HAVOC [6,53] and Frama-C [21] with its plug-in WP [22] for C, Spark-2014 [3] for Ada, KeY [10] for Java, Spec# [8] for C# and the verifier for Dafny [56]. Need comma after "C#", and what is the name of the tool and the name of the language in the case of Dafny? > Hoare logic is not suitable for specifying and proving concurrent programs. I think many people would disagree with this, and point to Owick-Greis's logic, etc. If what you mean is that Hoare's original logic only applies to sequential programs, fine. But what do you mean exactly by "Hoare logic"? Maybe this is understood more generally. > Owicki and Gries [71], Lamport [54] and Takaoka [86] introduced their tech- niques inheriting Hoare’s style for proving properties of concurrent programs Maybe say they "introduced extension to the original Hoare logic for proving properties of concurrent programs". "Owicki and Gries introduced their technique in [71] ...." Don't say "their", it doesn't belong to them. Maybe "...introduced a new technique..." "cobegin S0//...//Sn" : I don't think // are in the typewriter font. See if you can figure out how to get them to be. > Formal semantics of the two statements is defined as reasoning rules, just like what Hoare logic does. Formal semantics for these two statement are defined with new Hoare-style rules. >The most important idea in this work... Better: The key idea in this work... >...except for the term "interference-free". Let pre(S) ... There needs to be some transition between these two sentences. Maybe ...except for the term "interference-free," which is defined as follows. Let pre(S)... Also, it is just a peculiarity of English writing that a comma or period always goes within the closing quote, as in: ...the term "interference-free." "Let pre(S) be the pre-condition of a statement S, a statement T...". What is a pre-condition of a statement? I may be mis-remembering, but I thought the idea of non-interference was that something didn't interfere with the expressions occurring in a proof of something else. [I think the idea is that you can construct a "proof outline" and then every sub-statement has a unique pre and postconditions...and there is some way to make that precise.] Also, these are two separate sentences, so they cannot be separated by a comma. Maybe: Let pre(S) be the pre-condition of a statement S. A statement T is said to ... In 2., what are P' and Q'? Do you need to quantify over formulas P' and Q' too? In 2., you write pre S', but before it was pre(S'). ---- >Lamport ... {P}S{Q} to that 1) P must ... Lamport ... {P}S{Q} so that (1) P must ... >In addition, each vertex will be attached with an assertion. ...each vertex has an associated assertion. or: In addition, an assertion is attached to each vertex. >parallel programs contains parallel programs contain >contains synchronous statements. synchronizing statements? >“wait for ” “wait for” >the waited process waited is not a word. I think the best way to say this is to give the procs names. Process p and "wait for" another process q...until q executes accept. >program graph based program-graph-based >assertions that are suppose to hold assertions that are supposed to hold >The proof is constructed by showing the validity of those assertions for every program location. Isn't it more that the proof requires showing every edge preserves the invariants? >Techniques for proving liveness properties including the ... Techniques for proving liveness properties include the... This sentence is too long. Break up into more sentences. I think a bit more could be said about rely-guarantee. It seems more related since it is also about decomposing the verification tasks. However, it is a process-wise decompostion (if I understand it correctly), as opposed to a procedure-wise decomposition. Is it COMPLX or COMPLEX? (You write both) >imperial programming languages imperative? I feel the tool list could use a little more relation to what came before. You can have a few sentences about separation logic, which I think is in the Hoare logic tradition. And then concurrent separation logic. And what are permissions and how do they relate to what came before? There is always a theory preceding the tool. ------------------ Model Checking: I think the key difference between model checking and the previous section is that it begins by forming a finite-state model of the program you want to analyze. Transforming to a finite-state model can be accomplished through abstraction, by imposing bounds on parameters, numbers of processes, and so on, or a combination of these and other means. Then you can talk about the algorithmic methods for enumerating states, and so on. commutative executions: I think you can have two commuting transitions, but not two commuting executions. Symbolic Execution: >a boolean formula, path condition a boolean formula, the path condition >PC denotes the condition, under which PC denotes the condition under which Can you say the "symbols" are known as "symbolic constants". They are "constants" in the sense that their value does not change during the execution of the program, they stand in for a program constant like "7.0". >the true value true should be italicized since you are not using it in its regular English meaning >the exploring path the path being explored Example 2.2: would it help to create a diagram of the symbolic state space? If not, the line numbers are not helping you here. Also, they are jammed too close to the code. MPI >different language such as C and Fortran. I think it's exactly C and Fortran, no? default communicator: why not just say at this point it is named MPI_COMM_WORLD. >non-deterministic I think it is usually written with no hyphen, but check: nondeterministic >FIFO yes, except that by using tags in the MPI_Recv, you can break the FIFO ordering by pulling out a message that was not first in (it was the first in with that tag). However, there is no nondeterminism involve (there is exactly one oldest message with that tag), in contrast with the MPI_ANY_SOURCE. Why not actually name MPI_ANY_TAG and MPI_ANY_SOURCE here. >Constructs defined in MPI library all start Constructs defined in the MPI library all start Fig 2.4: maybe call it a C/MPI program >to process of rank 1 to the process of rank 1 >from process of rank 0 from the process of rank 0 Related Work >ISP [89] and DMAPI [93] are MPI model checkers I think it's worth calling them dynamic model checkers and the point is that in dynamic model checkers model=program. There is no abstraction. Am I right? Instead you are picking concrete numbers for everything (nprocs, inputs, etc.). But you jiggle the schedules. So it more like a hybrid between testing and model checking. Say something about the advantages/disadvantages. This is important related work. >with a configuration. what's a configuration? >These schedules differ from the matches that the MPI wildcard receive operations can make These schedules differ in the matches that the MPI wildcard receive operations make Don't they also differ in interleaving possibly? >able to verify free of deadlock and assertion violation properties of an MPI program. able to verify freedom from deadlock and assertion violations in an MPI program. And other safety properties? >MPI-SV [95] uses the symbolic execution engine to explore different paths of an MPI program. What is "the" symbolic execution engine? I think it is "a" symbolic execution engine. Maybe say someting about that engine. >CSP what does it stand for? >MOPPER [30] and HERMES [49] are similar tools to MPI-SV MOPPER [30] and HERMES [49] are similar to MPI-SV >multi-paths programs multi-path programs >it takes only one execution. what does "takes" mean? I think this should be expanded a bit. It isn't clear what a multi-path program is >HERMES uses symbolic execution to explore all paths and is sound for multi-path programs. This sounds great. How does it work and what are the limitations? >a state is associated with a path condition, a path condition is associated to each state. >MPI-Spin provides libraries in Promela language MPI-Spin provides libraries in the Promela language >CIVL uses an inter- mediate verification language, CIVL-C, I think what is missing from some discussion is some commentary. Some opinion on the pluses and minuses of these approaches. It is like a list of facts, with no evaluation of the facts. What is good about MPI-Spin compared to other things? What are the drawbacks. How does it differ from CIVL. What is the reason for using an intermediate verification language and what are the impacts of using it? >The number of states in the state space of a program grows exponentially along with the increasing of the number of processes. The number of states in the state space of a program grows exponentially with the number of processes. I would add "typically" above since it doesn't *always* grow exponentially. >model checking based tools can hardly be scaled to verify large codebases with realistic configurations. What does "hardly" mean? And I would agree with this statement for *monolithic* verification, but not if you are decomposing the problem, such as you do in this dissertation. >Compare to model checkers, Compared to model checkers, >static analysis based tools static analysis tools I think you should clarify that unlike the dynamic model checkers, these tools reason about all possible inputs too. (if that's true). But they also have limitations. Are there any effective static analysis tools for showing an MPI program is deadlock free, or has no assertion violations? Those are the properties you talked about for the previous (model checking) tools. You need to carry through that discussion here and say something like, these static analysis tools are totally automated, work for all inputs, scale well, but are used to check easier (simpler?) properties. Not deadlock free, assertions, but only .... (If this is true). In summary: when comparing different things (tools, techniques, approaches, ...) you need to compare them on the same terms: which properties do they check? sound? complete? scalable? ... I think a chart like the one we made for EuroMPI paper would be very helpful here. > MPI specific MPI-specific The bib entry for MPI-Checker shows MPI-checker. Maybe you need {C}. What are the limitations of MPI-Checker? It sounds like it solves all problems. >MPI-Checker was applied to MPI applications, of which the code size is as large as tens of thousands of lines. MPI-Checker was applied to MPI applications, some of which had tens of thousands of lines of code. >Besides the AST, the control-flow graph In addition to the AST, the control-flow graph This paragraph is trying to do too many different things. Break it up. >are made to CFG are made to the CFG. >parametric what does this mean? >There are runtime verification tools, Here now, you should compare on same terms as previous tools. Do these reason about all possible inputs? All possible interleavings? Wildcard matches? Etc. >They detect MPI errors by taking the use of runtime information. Huh? ---- >MUST do not report false alarm but its error checking depends on runtime executions. MUST does not report... I think what you are trying to say is that it may fail to detect defects if they are not revealed on executions to which it is applied. >All the related work described so far falls into the category of automated approaches.... I find this dichotomy between automated and not automated to be inaccurate. There are varying degrees of automation. MPI-Spin is not very automated if you take into consideration the work it takes to build a Promela model of a program by hand. Even CIVL is not so automated since you have to do things like build drivers and assertions and make assumptions, figure out how to bound parameters, and so on. >PARTYPES [60] verifies an MPI program with a protocol. Can you say a little more about the protocol and what it specifies. I think it is basically a sequentialization of the communication actions. Also, what does it have to do with types? >deadlock free deadlock-free >cannot deal with the wildcard receive operation cannot deal with the wildcard receive operation, i.e., with MPI_ANY_SOURCE. (Isn't MPI_ANY_TAG also a wildcard?) >The matches of the MPI communication operations supported by PARTYPES in an MPI program are deterministic. Can you be a little more precise? Do you mean, in order for ParTypes to succeed, the way sends are matched with receives must be independent of ... (inputs? interleavings?...). Maybe say something like, on any execution of the program for given inputs, the way sends are matched with receives will always be the same. (if that's true) >In [70], Oortwijn et al. present their preliminary work for specifying and verifying MPI programs modularly. Again I am missing the evaluation on the same terms as the other techniques. What are the advantages and limitiations of this approach? Can it handle arbitrary number of procs, or bounded? All inputs, or just specific ones? Wildcards? C? And so on. Why is it preliminary? >A different preliminary work for message-passing deductive verification is done by Luo et al. [62]. I would mention that this is the approach proposed by Ashcroft(?) years ago. And again, the evaluation. Arbitrary number of procs? Inputs? How much work (lots of annotations?). How complicated/difficult is the invariant (refers extensivesly to buffered messages, etc.).