ksummit.lists.linux.dev archive mirror
 help / color / mirror / Atom feed
From: ebiederm@xmission.com (Eric W. Biederman)
To: Josh Triplett <josh@joshtriplett.org>
Cc: ksummit-discuss@lists.linuxfoundation.org
Subject: Re: [Ksummit-discuss] [CORE TOPIC] More useful types in the linux kernel
Date: Tue, 19 Jul 2016 21:36:05 -0500	[thread overview]
Message-ID: <87inw1ave2.fsf@x220.int.ebiederm.org> (raw)
In-Reply-To: <20160719212645.GA14203@x> (Josh Triplett's message of "Tue, 19 Jul 2016 14:26:45 -0700")

Josh Triplett <josh@joshtriplett.org> writes:

> On Tue, Jul 19, 2016 at 10:32:51AM -0500, Eric W. Biederman wrote:
>> Would a gcc plugin that checks the most interesting things that sparse
>> checks on every build be interesting? (endianness of integer types for example)
>
> I'd like to see those checks more widely available, ideally not just as
> plugins.  Some exploration of that occurred upstream:
>
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59852 (bitwise/endian types)
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59856 (contexts/locking)
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59851 (nocast: no implicit conversions)
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59850 (address spaces)
> https://gcc.gnu.org/bugzilla/show_bug.cgi?id=59855 (designated_init; done)
>
> I'd love to see someone pick those up and get them into upstream GCC.

Interesting.

Whatever I do I intend to start and the hard problem of types that know
where all of your aliases are because I have something that works and is
very interesting there, so I won't volunteer for those but that does
look like a reasonable part of the discussion.

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

So "ownership" may be the wrong word.  See my reply to James Bottomley.
Rust never advanced past what are effectively smart pointers, and smart
pointers are the wrong concept for tracking aliases.

To get past that it takes some turning of all of your trained exceptions
of what a type system is tracking inside out (or at least it did for me)
but when you are done there is something that is much more expressive
and simpler than what Rust implemented.

Our fundamental complexity with smp synchronization may add up the
complexity again but it is undoubtedly possible to do better than Rust.
The way our kernel is built all of the core kernel would need to be in a
Rust unsafe block.  So I would not even consider doing what Rust did.

>> 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 think the biggest constraint is that new tools get very slow adoption,
> and it's incredibly difficult to introduce a new *mandatory* tool or
> compiler version (with the exception of tools that ship with the
> kernel).  And optional ones have a tendency to break due to patches from
> people not running them.  Apart from that: false positive rate.
>
> Ideally, build something you can opt into using, such that if you
> explicitly use it, the false positive rate should be *zero* by design.

With types what you do get a *zero* false positive rate by desgin.
Although sometimes you get a lot of const correctness kinds of
conversion requitements that are a royal PITA.

Eric

  reply	other threads:[~2016-07-20  2:49 UTC|newest]

Thread overview: 82+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2016-07-19 15:32 Eric W. Biederman
2016-07-19 17:31 ` Mark Brown
2016-07-19 18:52   ` Jiri Kosina
2016-07-19 20:39     ` Eric W. Biederman
2016-07-20 15:53     ` Mark Brown
2016-07-20 17:04       ` [Ksummit-discuss] [CORE TOPIC] [TECH TOPIC] Support (or move towards to) LLVM Jiri Kosina
2016-07-20 18:35         ` Alexey Dobriyan
2016-07-20 18:52           ` Mark Brown
2016-07-21  9:54         ` David Woodhouse
2016-07-21 13:41           ` Shuah Khan
2016-07-21 14:02             ` David Woodhouse
2016-07-21 16:21               ` Mark Brown
2016-07-23  3:28                 ` Behan Webster
2016-07-21 18:38           ` Jiri Kosina
2016-07-21 20:47             ` Paul Turner
2016-07-26 11:22             ` David Woodhouse
2016-07-19 21:08 ` [Ksummit-discuss] [CORE TOPIC] More useful types in the linux kernel James Bottomley
2016-07-20  0:08   ` Eric W. Biederman
2016-07-20  7:32     ` Julia Lawall
2016-07-20 12:11     ` Jan Kara
2016-07-28  3:33       ` Steven Rostedt
2016-07-19 21:26 ` Josh Triplett
2016-07-20  2:36   ` Eric W. Biederman [this message]
2016-07-30 18:03   ` Eric W. Biederman
2016-07-30 18:49     ` Josh Triplett
2016-07-30 19:34       ` Eric W. Biederman
2016-07-30 20:56         ` Josh Triplett
2016-07-30 22:21           ` Eric W. Biederman
2016-07-21 15:05 ` David Howells
2016-07-21 23:33   ` Dmitry Torokhov
2016-07-22  6:00   ` Hannes Reinecke
2016-07-22  6:14     ` Julia Lawall
2016-07-22 13:57       ` Hannes Reinecke
2016-07-22 14:40         ` Julia Lawall
2016-07-22 19:12         ` Arnd Bergmann
2016-07-26 11:48         ` David Woodhouse
2016-07-26 12:53           ` Hannes Reinecke
2016-07-26 13:59             ` Alexey Dobriyan
2016-07-26 13:53           ` Alexey Dobriyan
2016-07-27 12:40           ` Julia Lawall
2016-07-27 13:25             ` James Bottomley
2016-07-27 13:33               ` David Woodhouse
2016-07-27 17:21                 ` Bird, Timothy
2016-08-01 22:17                   ` Rob Herring
2016-08-12  1:29                     ` Stephen Boyd
2016-08-11 15:44         ` Dan Carpenter
2016-08-12  0:38           ` NeilBrown
2016-08-12 20:56             ` Dan Carpenter
2016-08-12  3:51           ` Matthew Wilcox
2016-08-12  4:01             ` Josh Triplett
2016-08-12  4:07               ` Matthew Wilcox
2016-08-12  5:29                 ` Alexey Dobriyan
2016-08-12  5:38                   ` Michael S. Tsirkin
2016-08-12  6:04                     ` Julia Lawall
2016-08-12  6:09                       ` Michael S. Tsirkin
2016-08-12  6:23                         ` Matthew Wilcox
2016-08-12  6:37                         ` Julia Lawall
2016-08-12  5:50                   ` Matthew Wilcox
2016-08-04  7:15       ` NeilBrown
2016-08-04 11:19         ` Julia Lawall
2016-07-22  7:03   ` David Howells
2016-07-22 10:10     ` Alexey Dobriyan
2016-07-22 10:13     ` David Howells
2016-07-22 10:22       ` Alexey Dobriyan
2016-07-22 10:53         ` Vlastimil Babka
2016-07-22 11:05         ` David Howells
2016-07-22 17:18           ` Julia Lawall
2016-07-22 18:19     ` Dmitry Torokhov
2016-07-22 19:43       ` Guenter Roeck
2016-07-28  3:40   ` Steven Rostedt
2016-07-28  7:12   ` David Howells
2016-08-02 10:48   ` Jani Nikula
2016-08-04 11:31     ` David Woodhouse
2016-08-04 12:07       ` Jani Nikula
2016-07-22 11:19 ` David Howells
2016-07-22 12:44   ` Linus Walleij
2016-07-22 13:26   ` David Howells
2016-08-12  4:42 ` Michael S. Tsirkin
     [not found]   ` <871t1ulfvz.fsf@notabene.neil.brown.name>
2016-08-12  5:34     ` Michael S. Tsirkin
2016-08-12  6:23       ` NeilBrown
     [not found]       ` <87y442jytb.fsf@notabene.neil.brown.name>
2016-08-15 23:26         ` Michael S. Tsirkin
2016-08-12  6:23   ` NeilBrown

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=87inw1ave2.fsf@x220.int.ebiederm.org \
    --to=ebiederm@xmission.com \
    --cc=josh@joshtriplett.org \
    --cc=ksummit-discuss@lists.linuxfoundation.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox