[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 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.

Similarly release_list takes a pointer to the first element of a list
and the ownership of the list releases the lock.

In the area in which you have ownership of the list you can use as many
different pointers as you like and they are all valid and all may be
used because the code can see all of the aliases, and nothing special
needs to be done because the code owns the list not any particular
pointer.

Which means that since one element of the list does not contain a
pointer owning the next element of the list, doubly linked lists
are not a problem.

This is not to say there are not tricky bits, but things like borrows
are replaced by simpler concepts.


I hope that is enough to clarify where I am coming from.  If not I
suspect it will have to wait until I can find the time to release my
proof of concept and documentation of all of this.

Eric