Re: [Ksummit-discuss] [CORE TOPIC] More useful types in the linux kernel

[ebiederm@xmission.com (Eric W. Biederman)]

James Bottomley <James.Bottomley@HansenPartnership.com> writes:

> On Tue, 2016-07-19 at 10:32 -0500, Eric W. Biederman wrote:
>> Historically the types in C came about because the machines
>> fundamentally supported different data types either with different
>> sizes or different characteristics (i.e. u8, u16, float, double).
>> These data types and the C type system were built so programmers
>> could tell the machine what they needed it to do.
>> 
>> There is another genesis of types that started with the simply typed
>> lambda calculs that is about eliminating common errors and otherwise
>> helping a programmer get their code right.
>> 
>> In the years since C was invented there has been a lot of activity
>> and a
>> little bit of progress in this area.  Would people be receptive to
>> improvements in this area?
>> 
>> I would like to talk to folks and gague what it would take to make
>> improvements in this area acceptable, practical, and useful.
>> 
>> Would a gcc plugin that checks the most interesting things that 
>> sparse checks on every build be interesting? (endianness of integer 
>> types for example)
>
> How would this be different from simply automatically running sparse in
> the kernel build if the binary is present (effectively making make C=1
> the default)?

Nothing.  I am just honestly looking at ways that we can get things to
always or almost always run.   Sparse isn't getting run regularly now so
I was suspect that would not be as good of a solution.

>> Would a type system for pointers derived from separation logic that
>> has the concept that a piece of data is owned by a piece of running
>> code rather than another piece of data be interesting?
>
> By this you mean a thread of execution that should be expected to free
> the data pointed to when it finishes?  Sort of like a self garbage
> collecting reference?

Not really.  The big idea is to make expressable in the type system the
key concepts on how a programmer reasons about their data structures,
instead of trying to make programmers perform some convoluted logic to
express things in concepts that are trivial to implement in a type
system.

Another way to talk about it would be complete alias analysis at type
checking time.

Which means that the type system then knows essentially everything the
programmer knows about aliases and object lifetimes and if you don't
pass something on or free it, the type checker then knows you made
a mistake.

>>   * This cleanly allows for doubly linked lists.
>>   
>>   * This is useful to ensure that data is either put in another data
>>     structure where it is remembered or it is freed.
>> 
>>   * This is useful to ensure reference counts are not leaked.
>> 
>>   * This is useful to ensure that every lock is paired with an
>> unlock.
>> 
>> My personal filter for things like this are types that can be checked
>> in time proportional to the amount of code to be built so that it is
>> roughly the same situation we are in now.
>> 
>> 
>> Given it's heritage and it's history the type system in C has serious
>> limitations that I don't know if they are correctible, when it comes 
>> to catching programmer mistakes: silent truncation of unsigned types
>> into smaller unsigned types, casts, etc.  Would people be willing to
>> consider a simple, link compatible alternative to C for some of the 
>> code in the kernel that had the same low level control of the machine 
>> but had a type system that made catching mistakes easier?
>> 
>> 
>> Deploying solutions like this will take a fair bit of grunt work, and
>> time similar or worse than the big kernel lock removal.  Given how
>> widely Linux is used and how annoying some of these bugs can be I 
>> think it is worthwhile to dig in and see what kind of improvements 
>> can be made.
>> 
>> I would really like to get a feel among kernel maintainers and
>> developers if this is something that is interesting, and what kind of
>> constraints they think something like this would need to be usable 
>> for the kernel?
>
> I've got to say that rewriting in some as yet undefined language simply
> to get better typing and conversions looks very daunting.  Before even
> considering this, can you answer why an extension to sparse, which
> would mostly flag the problems if we use the correct annotations,
> wouldn't work just as well?  We'd still have to add the additional
> annotations (and someone would have to update sparse) but it would
> still be a lot easier than rewriting and giving the kernel a build
> dependency on whatever the rewrite is done in.

That is a very good question.  The short answer is that I am not yet
convinced I can figure out how to retrofit the type checks I want onto
C's type system.  I have implemented the type checks I am looking at in
a fresh language I am toying with where I can throw out inconvinient
unnecessary corner cases.  After I finished boiling the ocean the basic
types were similar enough to C's type system that I think I can make
the connection but I haven't tried yet.

Assuming things can be sorted so they coexist nicely C's types.  No
advantage.  If it turns out that to make the code not a pain to write we
need better syntax or some basic type inference there is a large
advantage in converting code.

The first place I can think of where I might get hung up in the area of
discriminated unions.  I am pretty certain that some cases of type
safety will require them and C doesn't have anything like that today.  A
practical example would be a type system that ensures you call
IS_ERR(ptr) before you use a pointer as a pointer.

Ordinary C unions and type casts that serve the same purpose would at the
end of the day all have to be reabstracted.  Because otherwise memory
safety cound not be analyized.

Some of that reabstraction I will need to introduce type variables which
a completely foreing concept to C.

On the flip side since the linux kernel and low level programming where
precise control of the machine happens is my target audience it is
definitely worth looking at what can be done in a context like sparse.
That is the fastest way to connect the tools with the real world
problems.  If it can't be done or if it can't be made nice simple
and easy to use then there will be good arguments for why we need a new
syntax.

Mostly I asked the question because the type system would be so much
easier in a green field setting, and I wanted to be lazy.  So hearing
the common sense request (Please fix C.) Is helpful to get that lazy
part of myself in gear.

The end game for me is a type system that doesn't permit memory errors,
reference counting errors, locking errors, or deadlocks, while at the
same time allowing pretty much the code and data structures that we use
in the kernel today.

Eric