Re: Failure Modes and Ranges of Operation

On Feb 3, 12:43 pm, Bob Badour <bbad..._at_pei.sympatico.ca> wrote:
> Marshall wrote:
> >
>
> > In general, we find that "forward" computations, those
> > that are built out of successive lower level computations,
> > do not cause us problems. Given the ordered naturals,
> > we can speak of the successor function; given successor,
> > we can construct addition, which gives rise to multiplication,
> > which gives rise to exponentiation, which given rise to
> > tetration, ad infinitum. Each of these functions is total.
>
> Successor is only total if one has an infinite set. For a finite
> computational model, successor fails at some point, and the question
> then becomes: How does it fail? Likewise for addition, multiplication,
> exponentiation, factorial etc.

Well, it depends on the "style" of integer we are speaking of. In Tony Hoare's Turing Award paper, "An Axiomatic Basis for Computer Programming" he lists three styles, which he calls "strict" (faults on overflow), "firm" (return maxint on overflow) and modulo. We can also consider arbirtary precision. Each of these four has different behavior on overflow, and each thereby comes with different axioms and theorems. For example, with strict, addition is not total; with firm addition is total but we lose certain algebraic properties that might be useful. (a, b > 0 => a+b>a, a+b>b) or even simple associativity for addition of the integers. With arbitrary precision, we still get totality, but at a cost of both space and time: unlike the other tree, arbitrary means we also have to consider variable memory usage.

The good news is that whatever is chosen, we can build a formal system to model it.

I find it encouraging that mathematics considers modular arithmetic interesting enough to study it even without computer memory considerations as motivation. Modular ints, both signed and unsigned, form a ring, so we have a well-known abstraction ready-made for describing fixed size ints.

What is less encouraging is to realize that the Hoare paper reads today as fresh and interesting and full of unrealized possibilities, and it was written in 1969.

> > The integers solve this issue, and make subtraction total.
> > Multiplication is total even when we extend it to the integers,
> > but most pairs of integers divided don't make an integer.
> > So we get the rationals, but we still have a problem at zero.
> > At the next level, the forward function, exponentiation, is
> > fine, but at this level we have *two* inverse functions, because
> > exponentiation is not commutative. We get logs and roots,
> > and neither one is closed under the rationals.
>
> > But it is entirely possible to restrict ourselves to functions
> > that we know are total, or functions restricted to defined
> > inputs.
>
> Assuming we have infinite resources.

Even in the absence of infinite resources, we can still operate and insist on certain strict properties. We could for example build an effects system that will let us guarantee that there are no overflows, rendering any differences between modular and integer arithmetic moot. Again, there is always a cost in expressiveness and in the effort of proof generation.

> > However, this code will always work, independent of
> > the values of x and y:
>
> > int x, y;
> > if (y != 0)
> > return x/y;
> > else
> > return 0;
>
> And in a way, this is the point that failure mode analysis begins. What
> will happen when it returns zero instead of some super huge number?

Sure. We have to analyze all of the code we want to say anything about. And we have to analyze it not only for guaranteeing the presence or absence of whatever effects we care about, but also that it meets the formal specs.

> > Most compilers aren't smart enough to know that the
> > first return cannot fault, but there are a few research
> > compilers that can figure this out, and I think it's just
> > a matter of time until this capability becomes more
> > commonplace.
>
> I suspect the automated provers already handle this sort of thing.

Indeed yes. Coq is pretty cool and pretty impressive in what it can do. Hard to learn, though.

> After
> all, anyone would object to dividing both sides of an equation by x
> without simultaneously restricting the domain to exclude x=0. I think it
> would be extremely useful to have a proof checker that catches such things.

Yes! In fact I have this idea that it would be very sweet to have this integrated into the language at a deep level. And use the *same* mechanism as one uses for declarative integrity checks. At that point, one uses the same language (FOL probably) to propose whatever formula one cares to, and whether it becomes a runtime check (as is standard for a dbms) or a proof obligation (as in a theorem prover) could be a compiler flag. This could come with fine-grain control, allowing the programmer to say of each constraint that it must be proven, must be checked, or may be assumed. Furthermore this choice could shift over the course of development. One could go still further and use the same constraint language to state properties of both code and data in a uniform way.

> > There is also resource usage to consider. Given a
> > finite machine and a given program, how can we
> > be sure it is free of stack overflows, or out of memory
> > errors? It turns out to be possible to know this with
> > an effects system. The principle is simple: for every
> > effect one wishes to consider (maximum memory usage,
> > nontermination, etc.) one needs to have an algebra
> > for every kind of node in the language's abstract syntax
> > that can propagate the state of this effect based on
> > its child nodes.
>
> Nontermination? Isn't that one a stretch? Or are you suggesting the
> language restricts one to algorithms for which one can determine halting?

It is a useful option to have. I don't think it should be the default requirement, though.

Another proposed mode for termination analysis is using it selectively. An interactive program might have a main loop that could run forever, but one might want a guarantee that each command would complete in finite time. (Possibly even within a specific bound.)

> > For example, recursion makes many of these calculations
> > harder, so there are systems in which it is simply not
> > allowed. You pay a cost in expressiveness, and you get
> > a benefit: without recursion, termination analysis is much
> > easier.
>
> Is it? It seems to me a turing machine doesn't exactly support recursion
> and didn't somebody once prove one cannot prove whether every algorithm
> halts using one?

A turing machine has GOTO, though, which is even harder to analyze than recursion. (And no more computationally powerful.)

> > As an aside, I'll also mention Erlang, which, while
> > not on the same formal basis as the other stuff
> > I've mentioned, nonetheless has an excellent
> > reliability record on the basis of an unusual error
> > handling philosophy called "Let it Crash." The basic
> > idea being that the consequence of any kind of failure,
> > divide by zero, abrupt socket closure, etc. is dealt
> > with by the death of the thread in which the fault
> > occurred. No try/catch here! Instead there is a clean
> > system of supervisor processes which monitor and
> > detect thread faults and respond according to policy.
> > In practice this works exceedingly well; Erlang software
> > has some of the highest uptime in the industry.
>
> Uptime is one thing. But what happens to a physical device under the
> control of a thread that just disappears?

An interesting result from a paper I read off the SPARK/Ada site was that they said they found that the utility of the proof system broke down at the edges of the architecture, in terms of dealing with the humans and in dealing with the hardware. For example, it was difficult to prove that drawCircle() produced a round glyph on the monitor. It was impossible to prove much about the devices themselves. We sent the buzzer a tone; prove it was loud enough to hear.

But they also claimed, with numerical evidence, that doing the proofs found more bugs earlier and at lower cost than other methodologies, such as unit testing.

Marshall Received on Sat Feb 03 2007 - 23:42:29 CET