[cap-talk] Hybrid Cap Systems redux

Jonathan S. Shapiro shap at eros-os.com
Tue Feb 19 09:36:56 EST 2008


On Mon, 2008-02-18 at 21:46 -0800, David Wagner wrote:
> Jonathan Shapiro writes:
> >Two problems here:
> >
> >  1. C is unsafe, therefore these safety checks violate C semantics (and
> >     do so in practice, not just on paper).
> >
> >  2. It is a continuing source of wonder to me that people think it is
> >     good to induce failure in working C programs by adding checks that
> >     cause perfectly good programs to fail.
> >
> >It isn't good enough to guarantee that misbehaved programs fail. What we
> >need is to guarantee that programs do not misbehave.
> 
> Can you explain these two comments?  If you mean something more
> than "safety checks alone are not sufficient", I'd like to understand
> what you mean.  I know you've thought about this a lot and so I suspect
> you may be hinting at something non-obvious...

Well, obvious to me, but only in hindsight, and hardly a new insight.
But let me preface this: sometimes, in discussions here and elsewhere, I
only seem to do half of a context switch, and I respond to something in
one discussion from an inconsistent context. It's a particular problem
when I am responding quickly, which is all too often. I think that is
what happened above.

On to answer your question.


Dynamic checks cannot render a program correct. They can only render a
program "fail-faster". My main focus of attention at the moment is on
critical systems, where the requirement is that the program not fail.
Adding checks that fail the program explicitly doesn't really help in
that context.

I think what happened above is that I made a left turn because of an
unrelated discussion. Since it is tangentially relevant, let me play it
back.

As I'm sure you (DAW) probably realize, we've encountered a lot of
publication resistance to the BitC work in the PL community. Of course
there are always people who don't "get it", but we have gotten lots of
comments of the form "but X already does that", where X is one of
[cqual, cyclone], and hopefully Deputy will soon be getting mentioned as
well. Somewhere along the way we realized that there is a subtle point
we had utterly failed to make.

Cqual, Deputy, Cyclone, and friends are focused on the problem "How do
we make an existing [variant of] C safe[r] to run?" Each of them, I
think, offers an interesting approach that is good and useful work.

BitC is focused on the problem "How do we make a systems program in
which both safety and liveness are assured, while satisfying the
requirement that low-level representation is never perturbed?" This is
prompted in part by discussions with Rod Chapman about Spark/ADA. One of
the big deals about the Spark verification condition generator is that
they can prove that fairly large codes are exception free, which
justifies turning off the exception and bounds checks that are normally
emitted by the compiler.

But for systems codes involving tagged unions and pointers (as in BitC)
that problem becomes very very nasty very quickly (Spark doesn't have
pointers for this and other reasons). We chose to engineer a lot of that
problem out of BitC rather than try to do hard verification conditions.
About the only property left that we need to discharge is array bounds
checking, and for a number of reasons that one isn't that hard (not
easy, mind you, just not that hard).



shap



More information about the cap-talk mailing list