7 ms·

> It's also not enough to prove the property. Errr, yes, you're right. I noticed I messed up after I posted my comment, then edited it accordingly. I don't see

> It's also not enough to prove the property. Errr, yes, you're right. I noticed I messed up after I posted my comment, then edited it accordingly. I don't see why I need to perform induction on the program counter, though. I posit that, no matter how you interleave your processes, there is some distinguished index i such that x[i] is written by process i before it is read by process `(i+1) mod N`. To prove this, I use induction on N: (0) If N = 1, then i = 0. (1) If N = M + 1, inductively assume that we have a collection of M processes with distinguished index i. Now consider the effect of adding one more process, respecting the interleaving of the original processes: (1.a) If the new process is added at any index other than `i+1`, then the original processes i and `(i+1) mod M` still have contiguous indices in the new collection, and the former still writes to the common variable before the latter reads it. (1.b) If the new process is added at index `i+1`, then at least one of the two following things must happen: (1.b.i) The original process i writes to x[i] before the new process reads it. (1.b.ii) The new process writes to x[i+1] before the original process `(i+1) mod M` (now `(i+2) mod N`) reads it. No analysis of the program counter was required, and as a result we get a far more beautiful proof. You used a sledgehammer, I used a sculptor's chisel. > Properties that are easily checked by simple type systems like those of Haskell and SML can always be satisfied by much simpler programs (in fact, a FSM or, if polymorphic recursion is used, then a PDA). I never claimed that I could delegate the entirety of the formal verification task to a type system like that of Haskell or SML. And, to be honest, I don't even think using computers to verify everything is such a good idea. What I want is automation for the boring and repetitive parts (the vast majority), so that I can concentrate exclusively on the hard ones. (Which isn't to say that I'm happy with the little amount of work Damas-Milner does for me. It's possible to do much better, without sacrificing automation.)

pron 10y ago
> and the former still writes to the common variable before the latter reads it. This is not true. At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. > then at least one of the two following things must happen: This, too, is untrue. The events may occur in the precise opposite order. If this were true, then it would have been an invariant that either process N-1 or process 0 would necessarily write 1, but this is not the case. > No analysis of the program counter was required, and as a result we get a far more beautiful proof. You used a sledgehammer, I used a sculptor's chisel. Excellent, except that my "sledgehammer" is a proof technique that's been proven complete, i.e. if a program property is provable, it is provable via an inductive invariance, which is amenable to mechanical proof checking (and, indeed, I mechanically checked it in TLA+). Good luck getting your proof (which is called "behavioral") -- even if it were correct -- to verify formally. Chord is a distributed algorithm that was published in 2001 and quickly became popular. It got thousands of citations and plenty of industry implementations. In 2011 it even won a "test of time award". Its authors said, "Three features that distinguish Chord from many peer-to-peer lookup protocols are its simplicity, provable correctness, and provable performance". They, of course, provided proofs. However, in 2012, Pamela Zave, using a model checker, showed that "of the seven properties claimed invariant of the original version, not one is actually an invariant". The point is that when algorithms are concerned, "proofs" are often not proofs. See: https://brooker.co.za/blog/2014/03/08/model-checking.html https://brooker.co.za/blog/2014/03/08/model-checking.html and https://www.youtube.com/watch?v=iCRqE59VXT0 https://www.youtube.com/watch?v=iCRqE59VXT0 > I never claimed that I could delegate the entirety of the formal verification task to a type system like that of Haskell or SML. Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification. Formal proof means using natural deduction or sequent calculus. This is too hard, so a machine-checked proof is acceptable. But any proof or any other kind of verification not carried out or verified by a computer is not formal.
- catnaroek 10y ago
  > At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. I didn't say anything about “the last process”, though. I just took a collection of M processes, with some valid interleaving, and inserted one more process, at whatever index j, displacing all pre-existing proceses j...M-1 one place to the right. >> then at least one of the two following things must happen: > The events may occur in the precise opposite order. Let A and B be processes with adjacent indices (for my purposes, M-1 and 0 are considered “adjacent”), such that A's write happens before B's read. If we insert a new process C in between A and B, then A and B no longer manipulate a shared variable, but instead A writes to a variable C reads, and C writes to a variable B reads. Then at least one of the two following things must be true: (0) A's write happens before C's read. (1) C's write happens before B's read. This follows from these facts: (0) A's write must happen before B's read. (1) C's write must happen before C's read. Was that too hard to understand? If it was, you need to relearn to prove things by hand. > Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification. While the proof I gave above is most certainly informal, you can prove things formally using pen and paper. The formality comes from the use of explicitly given deduction rules, not from the use of a computer.
  - pron 10y ago
    > I didn't say anything about “the last process”, though Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to consider various interleavings. It also doesn't require induction on N. > The formality comes from the use of explicitly given deduction rules, not from the use of a computer. That's true and I said as much, but doing so is extremely laborious. Do you actually use natural deduction?
    - catnaroek 10y ago

pron 10y ago

> and the former still writes to the common variable before the latter reads it. This is not true. At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. > then at least one of the two following things must happen: This, too, is untrue. The events may occur in the precise opposite order. If this were true, then it would have been an invariant that either process N-1 or process 0 would necessarily write 1, but this is not the case. > No analysis of the program counter was required, and as a result we get a far more beautiful proof. You used a sledgehammer, I used a sculptor's chisel. Excellent, except that my "sledgehammer" is a proof technique that's been proven complete, i.e. if a program property is provable, it is provable via an inductive invariance, which is amenable to mechanical proof checking (and, indeed, I mechanically checked it in TLA+). Good luck getting your proof (which is called "behavioral") -- even if it were correct -- to verify formally. Chord is a distributed algorithm that was published in 2001 and quickly became popular. It got thousands of citations and plenty of industry implementations. In 2011 it even won a "test of time award". Its authors said, "Three features that distinguish Chord from many peer-to-peer lookup protocols are its simplicity, provable correctness, and provable performance". They, of course, provided proofs. However, in 2012, Pamela Zave, using a model checker, showed that "of the seven properties claimed invariant of the original version, not one is actually an invariant". The point is that when algorithms are concerned, "proofs" are often not proofs. See: https://brooker.co.za/blog/2014/03/08/model-checking.html https://brooker.co.za/blog/2014/03/08/model-checking.html and https://www.youtube.com/watch?v=iCRqE59VXT0 https://www.youtube.com/watch?v=iCRqE59VXT0 > I never claimed that I could delegate the entirety of the formal verification task to a type system like that of Haskell or SML. Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification. Formal proof means using natural deduction or sequent calculus. This is too hard, so a machine-checked proof is acceptable. But any proof or any other kind of verification not carried out or verified by a computer is not formal.

catnaroek 10y ago
> At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. I didn't say anything about “the last process”, though. I just took a collection of M processes, with some valid interleaving, and inserted one more process, at whatever index j, displacing all pre-existing proceses j...M-1 one place to the right. >> then at least one of the two following things must happen: > The events may occur in the precise opposite order. Let A and B be processes with adjacent indices (for my purposes, M-1 and 0 are considered “adjacent”), such that A's write happens before B's read. If we insert a new process C in between A and B, then A and B no longer manipulate a shared variable, but instead A writes to a variable C reads, and C writes to a variable B reads. Then at least one of the two following things must be true: (0) A's write happens before C's read. (1) C's write happens before B's read. This follows from these facts: (0) A's write must happen before B's read. (1) C's write must happen before C's read. Was that too hard to understand? If it was, you need to relearn to prove things by hand. > Just to be sure: proof with pen and paper isn't formal verification. It is pretty the very definition of informal verification. While the proof I gave above is most certainly informal, you can prove things formally using pen and paper. The formality comes from the use of explicitly given deduction rules, not from the use of a computer.
- pron 10y ago
  > I didn't say anything about “the last process”, though Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to consider various interleavings. It also doesn't require induction on N. > The formality comes from the use of explicitly given deduction rules, not from the use of a computer. That's true and I said as much, but doing so is extremely laborious. Do you actually use natural deduction?
  - catnaroek 10y ago