Serious kernel bug caused by programming in C

[Barry Schwartz]

I presume this could have been avoided more easily without testing,
were the kernel written in ATS:

https://bugs.gentoo.org/show_bug.cgi?id=525548

I was running that kernel until yesterday and suppose I should now do
filesystem checks.

[gmhwxi]

Yes or no, depending on how the code is written in ATS.

Say we have the following if-statement:

If
(mytest())
{
 do_something();
} else {
 do_something_else();
}

And a rule says that
do_something() can be called only if mytest() returns true.

In C, the programmer is responsible for enforcing the rule.
If mytest() changes into !mytest(), the rule is broken and the programmer
may not notice it.

The rule can be enforced in ATS through typechecking: do_something is
required to take a proof argument and such a proof can only be returned if
mytest() returns true. In this way, if mytest() changes into !mytest(), the
typechecker will complain. This is really the essence of programming with
theorem-proving.

[Raoul Duke]

i think this particular bug would easily be detected if people used
proper safe type aliases instead of raw primitive types, which seems
easier to advertise than saying anything with the word "proof" in it
:-)

[Barry Schwartz]

gmhwxi <gmh...@gmail.com> skribis:

> Yes or no, depending on how the code is written in ATS.
>
> Say we have the following if-statement:
>
> If
> (mytest())
> {
> do_something();
> } else {
> do_something_else();
> }
>
> And a rule says that
> do_something() can be called only if mytest() returns true.
>
> In C, the programmer is responsible for enforcing the rule.
> If mytest() changes into !mytest(), the rule is broken and the programmer
> may not notice it.
>
> The rule can be enforced in ATS through typechecking: do_something is
> required to take a proof argument and such a proof can only be returned if
> mytest() returns true. In this way, if mytest() changes into !mytest(), the
> typechecker will complain. This is really the essence of programming with
> theorem-proving.

I was thinking along the lines of using more precise types, the sort
of thing you could do in ML as well, if it were suitable for Linux
kernel code. Maybe one could do it in C++ with its C-incompatible
(grrrr) enums and such.

In C usually the best you can hope for is to get a compiler to issue a
warning. (And there is a compiler popular these days that issues so
many extremely noisy warnings by default that it must have the effect
of desensitizing people, but I’m not naming names.)

[Hongwei Xi]

I looked it again. Strangely, I originally had the impression that the bug was

caused by a misplaced negation (!). It is not. As you said, this one is really trivial

to detect in a typed language. Now, tell it to the Scheme people :)

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4iYbh-F1BKQeN4zLc8LbEvsSbMFsvvy0LfxYGBv4f6nw%40mail.gmail.com.

[Barry Schwartz]

Hongwei Xi <gmh...@gmail.com> skribis:

> I looked it again. Strangely, I originally had the impression that the bug was
>
> caused by a misplaced negation (!). It is not. As you said, this one
> is really trivial
>
> to detect in a typed language. Now, tell it to the Scheme people :)

Typed Racket exists. :)

I have thought about it a lot, and have come to operate by a succinct
principle: running software to test should be considered inherently
bad. Tremendous communal effort ought to be brought to bear towards
progressively getting rid of the need to run software.

Attempts to ‘fix the wetware’ are mostly misguided; they tend to
consist, for instance, of mimicking civil engineering processes that
get bridges built correctly and on time, thinking they must be magical
processes, and expecting magic to happen. And I absolve programmers of
immediate responsibility for most of the bugs we see.

(I think back fondly to when ‘A Discipline of Programming’ and
‘Algorithms + Data Structures = Programs’ were well known books.)