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

[Eric W. Biederman]

Josh Triplett <josh at joshtriplett.org> writes:

> On Sat, Jul 30, 2016 at 02:34:33PM -0500, Eric W. Biederman wrote:
>> Josh Triplett <josh at joshtriplett.org> writes:
>> 
>> > On Sat, Jul 30, 2016 at 01:03:30PM -0500, Eric W. Biederman wrote:
>> >> 
>> >> Josh Triplett <josh at joshtriplett.org> writes:
>> >> 
>> >> > On Tue, Jul 19, 2016 at 10:32:51AM -0500, Eric W. Biederman wrote:
>> >> >> 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?
>> >> >
>> >> > Interesting, yes, but trying to track "ownership" gets complicated
>> >> > *fast* to handle real-world cases.  Rust went through quite a lot of
>> >> > work, and multiple iterations, to get to the system it has now.  I don't
>> >> > think you'd be able to handle many of the cases in the kernel without
>> >> > about that much complexity.
>> >> 
>> >> Politely Rust did it the stupid way.  "ownership" or perhaps better said
>> >> who is allowed to modify the data is an active piece of code thing
>> >> rather than a data thing, and Rust did it as a data thing.
>> >
>> > I'd be interested to hear more details on what you mean by this, because
>> > the way you've described it doesn't make sense to me.  The way lifetimes
>> > are implemented in Rust seems very much like "an active piece of code
>> > thing".  Can you give an example of the distinction you're making?
>> 
>> But that is a lifetime of a piece of data, that isn't ownership of data.
>> The data is still owned by some pointer.
>> 
>> Ownership by code looks roughly like:
>> 
>> 	head = acquire_list(&task_list);
>> 
>> 	/* At the data level head points to the first element of the list */
>>         /* The type of head is a recursive type that includes every
>>          * element on the list.
>>          */
>>          for (ptr = head; ptr; ptr = ptr->next) {
>>          	/* The type of ptr shares with head the type of the list.
>>                  * Which allows both ptr and head to be valid
>>                  * and the code of this function to continue owning the list.
>>                  */
>>                  ptr->scratch++;
>>                  /* As the owner any mutation may be performed on the list elements */
>> 	}
>> 
>> 	release_list(list);
>>         /* Accessing list past this point would be a type error */
>> 
>> Where acquire_list and grabs the appropriate spinlock and then returns
>> ownership of the list to the calling function through a ponter to the
>> first element of the list.
>
> (Nit: I think in that last line you wanted release_list(head);)

Yes.

> What happens if the code saves a copy of either head, ptr, or something
> accessed via ptr, and then some other distant code accesses that after
> release_list?  (For instance, consider a function that takes a pointer
> to "scratch" and retains that pointer.)  In the type system you
> envision, what prevents that?

It depends a bit on how the copy is saved.  Without something special
when you reach the line release_list(head) the return of release_list
consumes the list as free does.

Which type wise means that the pointers you talk of remain valid things,
but you can not dereference them because the type they point to has
become unusable.   Which makes all future derefernces impossible.

> What happens if the code in that region, while looking at one value of
> ptr, changes the list in a way that invalidates ptr?  What prevents
> that?

Depends.  If it invalides ptr.  ptr becomes unusable (at least
undereferenceable).  And using dereferencing pointer past that point
does not type check.

Which is a long way of saying that functions are allowed to change the
destination types of pointers that are passed into them.  This changing
what pointers point to is the type equivalent of having preconditions
and postconditions.

Plus there is the other benefit to being able to change the type of
things by functions.  It is possible to build types that enforce state
machines by changing a the type of a variable and only making methods
available when they are valid to use.

And yes all of this depends upon having enough information to know
(within a small window) where all of the aliases for any value are at
any given time.

Eric