[M3devel] ESC

[Hendrik Boom]

On Thu, Dec 30, 2010 at 11:13:57PM +0000, Daniel Alejandro Benavides D. wrote:
> Hi all:
> it makes and abstraction of the code in terms of Guarded commands of 
> Dijkstra, then applies the static checking of the calculus of weakest 
> preconditions type checking as a normal program too the code

This will be difficult for loops.  Dijkstra's formalism more or less 
requires a variant to decrease around the loop.  In fact, in his "A 
Discipline of Programming", he shows multiple examples where the 
choice of variant and invariant that are used to prove the program 
correct more -r less determines the program itself.  A lovely book.

> and then translates to first order logic formulae, if the annotated 
> program can be satisfied then it will give no output, but if does 
> prove that the program doesn't produce the anottated output, it will 
> complain on where it fails, wherever it doesn't like the proof.

> The important thing is that if the checker satisfies all of his 
> conditions, it doesn't mean it does not break, i.e it could be that 
> the checker will no complain but still can't prove absolutely that is 
> not to crash, is a kind of liberal, perhaps because of its logic 
> calculus.

That's definitely not Dijkstra's weakest preconditions, then, but 
something similar.

> There is also the case of possible false alarms, which could be 
> triggered, but this is almost the case in any compiler and here too, 
> even the M3 compiler (something called completeness, just very simple 
> known type systems have), so we can't expect to type check in the 
> semantic analyser it wrong and to accept it in the checker, but we 
> could instead just to make that a unsound program, lets say unsafe, 
> will not lock or crash because and specific error because of the 
> non-completeness issue. However the ESC didn't accept some special 
> kind of almost safe programs, recursive, partly I believe because of a 
> problem exposed below, is perhaps that the program doesn't end, unlike 
> a for loop. 

Dijkstra in his calculus in "A Discipline of Programming" didn't 
consider recursion.

So far I get the impression that ESC didn't guarantee that the program 
would run properly if it passed all the checks, nor that failure to pass 
the checks implied invalidity.  It just sort of points put things that 
may need attention.  Kind of like a formal verificatin system that's 
implemented half-heartedly.
  
> There is also the need of a efficient and smarter automatic theorem 
> prover, Simplify is one of the best available for some time now, 

Is it?  Got references?  I recall that formula simplification was a 
basic technique in one of the first formal-verification systems back in 
the late 60's, and that it solved a lot of complicated cases.  They 
originated by substituting into standard formulas that expressed 
particular predicate transformations.  You got a lot of things like i > 
0 & i >= 0 & i < 2, which can be simplified to i = 0 if you know i is in 
integer.  There were a huge number of these simplifications, trivial and 
tedious, and often they sufficed to shos one formula was equivalend to 
another.

> but still, the same problems arise on it, it could be that because 
> of the first order logic, the program could not terminate but the 
> prover believe it will and it apparently does it, but that its 
> proofs will be not totally proved for all cases, if so, then we would 
> need to take care of those by applying hand formal verification 
> measures like below I explain a case.

> Also Simplify could rise that he can't prove that something is not 
> provable by itself, but turn that it is doable, just that it can't by 
> its own, so we need to also verify those cases.

> In the end, the best case our checks will end, but sometimes, the 
> first order logic could be an endless proof or undefined, in those 
> cases we would need a threshold given by the experience, so we might 
> start sooner than later to make our own.

> The best of this is that are many things that have room for 
> improvement as Dr Greg Nelson told me some time ago, would be nice 
> thing to have the TODO list from him.

> My personal wish is to make Modula-3 totally verifiable, learning this 
> by hand would be harder, but by the tools we could make it for using 
> its internal logic, the most critical part, the Professor Greg Nelson 
> did some work on that part of that I believe.

Formal verification is a hard problem.

> Then the important parts are the semantic checker which it self is 
> built on its internal logic, e.g a biased logic (i.e an unsound one, 
> the proofs could not end or be too large to finish and unable to 
> realize that after it spends time on it) it could be that never ends a 
> proof or check it badly as good, the most perfect it checks it would 
> be less efficient at some point (perhaps this was the reason to not 
> check the total correctness besides the effort needed) so might be 
> easier to pass the checks but less profitable in the checking. I 
> really would like the most inner parts to be self provable, like more 
> functional style programming then, but those are not verifiable by the 
> ESC checker, it just doesn't do that, similar to when I had a problem 
> on the checker I used sasylf.org,

I'll have to look into that.

> it had unimplemented the mutual 
> induction proving part by that time of a course back in 2008, this is 
> a theorem proof technique you need to use in advanced type theory of 
> type system soundness proofs, sasylf is a programming language by 
> itself to proof it is sound, so it turns out that if we can trust on 
> them more than in any part of the checker we could move on from there 
> to more advanced techniques, also this is harder I believe based on my 
> small experience of type systems proofing. 

I was working with Martin-Lof's type theory in the eighties.  I ended up 
with a verifier, and manages to mechanically proof-check a 
merge-sort, written in the lazy functional language that's implicit in 
the logic.  It was difficult to use, and really taxed the resources of 
our Vax 780, even though it has a whole 5 megabytes of memory!  And the 
first verified sort had a bug -- not that it didn't sort; that had been 
proved, but that it wasn't the merge sort I had intended; it took 
quadratic time.

That verifier is where I learned you have to debug the specifications as 
well as the code.

Right now, the most sophisticated poof-checker of this kind seems to be 
coq, but some users of coq find they have to more-or-less rewrite coq to 
achieve efficiency of effort.
 
> ESC developers say, the most provable source of those mis-checkings is 
> automatic theorem prover, not in checker, then it might be more 
> valuable to start there than in the checker's logic by itself, being 
> more practical, more pragmatic. I have some experience with the use of 
> automatic theorem provers part use by hand with sasylf, writing the 
> proofs and let it check for one (say I was the ESC checker and sasylf 
> was the automatic theorem prover), and it turns out not to be so 
> difficult to use after some work and time of use, still there are many 
> challenges open in the checkers for now, so the room for improvements 
> there is also too big (i.e we can check more things, say, the Modula-3 
> arithmetic over and/or under flow, recurrence, by improving the core 
> logic calculus and later working on the "second pass" or backend first 
> order logic prover).

> A special feature was the Locking level notation developed by writing 
> the Trestle library,

Those locking levels were something special.  I remember thinking deeply 
about the way those assertions worked, deciding that they were the right 
kind of assertions to base proofs on, and proceeded to ignore them when 
I read the rest of the code.

> as it was coded threaded, it is perhaps the most 
> advanced part of it, more details than that I don't now, but more 
> probably coming on the way. I just know its logic is more advanced 
> from what I recall, it requires some clever reasoning and calculus too 
> I guess.

Yeah... this is what we'd need to catch races and deadlocks and such.  
And it does seem to be mostly independent of the partial-correctness 
theorem proving described above.  Deadlock and races are global issues.

> So we can have a lot discussion, perhaps the first kick is given now. 

> I also hope its not too much blah, ... sorry for the long message

Mostly you've outlined some traditional verification technology.  ESC 
seems to use that, possibly with a restricted class of assertions (not 
clear just which ones), and has the limitations of the same.

But the locking levels in trestle do seem to be something else.

> Thanks in advance 

You're welcome.  It seems to be a big project. to answer one of my 
original questions.  The question is, whether there are smaller 
subprojects that are more feasible and will lead to a checker with code 
structure that can be easily grown.  Without small successes, the 
motivation is often absent to proceed on to the large successes.  That's 
especially true with FLOSS.  Once you have something that actually does 
something useful, people start to use it, and suddenly your users 
realise how it could be improved, tell you, and if you're lucky, start 
to make the improvements themselves.

---

My view of formal verification is that the proof has to be primary.  You 
write a proof that there is some code that satisfies a spec, and the 
details of the proof reveal the program.  This is completely different 
from the inductive-assertion method, in that you can use general 
theorems about particular loop structures, for example, and specialize 
then as necessary.  In fact, I suspect that the theoretical feasibility 
of this approach is possibly the only reason why people can understand 
programs at all.  You look at some code, decide after a while that 
there's a nest of six corecursive procedures, look at how parameters are 
passed down, and realize that it's recursion on a particulat tree 
structure -- at least you hope it's a tree structure, because its 
finite, noncyclic structure is nowhere explicit in the code.  You reason 
backwards from patterns in the code to the reasoning the original 
programmer must have had in mind when he wrote it -- reasoning 
which rarely appears in the code, rarely even in comments.

But using any of these methods for formal verification
is still impractical except where the requirements for reliability 
justify extreme efforts.

And I suspect strongly that the logic -- and the particular 
easy-to-use theorems about synthesizing program structures --  
should dictate the structure of the programming language, which 
quite possibly won't end up being Modula 3.

But who knows?  The logic people use to decompose problems into 
implementable program components are largely independent of the 
pangauge they use, except for
  * restrictions of parameterization
  * absenes of convenient coding patterns for desired code 
structures
  * reliance on the particular properties that the language 
implementation guarantees (and therefore needs less explicit thought).

I can imagine that the higher-order logics involved are similar for many 
programming languages, just as things like the Deduction Theorem 
are similar in many quite different formal logics (though the details 
of the proofs can be quite different).

-- hendrik



> 
> --- El mié, 29/12/10, Hendrik Boom <hendrik at topoi.pooq.com> escribió:
> 
> > De: Hendrik Boom <hendrik at topoi.pooq.com>
> > Asunto: Re: [M3devel] gui problems? BadBricks? columns?
> > Para: m3devel at elegosoft.com
> > Fecha: miércoles, 29 de diciembre, 2010 22:26
> > On Wed, Dec 29, 2010 at 08:23:12PM
> > -0500, Coleburn, Randy wrote:
> > > Daniel et al:
> > > 
> > > I tried a year or so ago to pursue getting the sources
> > for the ESC.
> > > I'd have to dig up my old emails, but my recollection
> > is that I ran into a dead end getting the sources and the
> > permission to put them in our repository.
> > > I don't think the Modula-3 edition was kept up when
> > the project moved on to other languages.
> > 
> > What does the ESC do that's relevant to threading?  I
> > mean, not just an 
> > answer like "deadlock and race detection", but what
> > algorithms does it 
> > use to accomplish it?  Does the Modula 3 compiler
> > construct the proper 
> > data structures that could provide the raw data those
> > algorithms would 
> > need?  How much work would it be to reimplement this
> > from scratch?
> > 
> > -- hendrik
> > 
> 
> 
>