Refactoring the FreeBSD Kernel with Checked C [pdf]

The numbers on a paper itself are much lower, so I would say it is a worthy idea. If not for "whole" kernel, then at least for the calls that they have replaced.

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#5

Post by superjan » Tue, Feb 02, 2021, 9:22 PM UTC

ornxka wrote: post #2

>Checked C has low performance overhead (only 8.6% on selected benchmarks [25]) Isn't that actually kind of significant?

That 8.6 figure comes from the paper linked below [0]. It’s an average. For many benchmarks, the difference is less than one percent, for others it’s 20 or more. In the freebsd article, they see around 1%.

[0] https://www.microsoft.com/en-us/research/uploads/prod/2018/0...

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#6

Post by sgt » Tue, Feb 02, 2021, 9:58 PM UTC

I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#7

Post by AdmiralAsshat » Tue, Feb 02, 2021, 10:00 PM UTC

Checked C appears to be a relatively recent research project from Microsoft[0][1], so I'm not sure that FreeBSD would be terribly keen on refactoring around it. There have also been many "safer C" languages before, so the only advantage that the paper offers is that Checked C seems to have a higher degree of backwards compatibility. I suppose that would allow the implementation/refactoring to gradually occur over time, rather than requiring a herculean initial effort.

[0] https://www.microsoft.com/en-us/research/project/checked-c/

[1]https://github.com/Microsoft/checkedc

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#8

Post by chubot » Tue, Feb 02, 2021, 10:25 PM UTC

sgt wrote: post #6

I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?

I don’t think pleasure is really the goal. The goal is systems that don’t fail spectacularly on unexpected inputs ...

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#9

Post by saagarjha » Tue, Feb 02, 2021, 10:39 PM UTC

chubot wrote: post #8

sgt wrote: post #6

I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?

I don’t think pleasure is really the goal. The goal is systems that don’t fail spectacularly on unexpected inputs ...

Clearly the pleasure of C is the feeling you get when your software fails spectacularly on unexpected inputs.

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#10

Post by spijdar » Tue, Feb 02, 2021, 11:01 PM UTC

chubot wrote: post #8

sgt wrote: post #6

I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?

I don’t think pleasure is really the goal. The goal is systems that don’t fail spectacularly on unexpected inputs ...

My (overly charitable?) interpretation is, "Is Checked C so painful to write that we'd be better off just using a better managed language"

Of course, if it's feasible to refactor existing C code like in the paper, this seems like a good path forward, vs trying to "start over" with whatever other checked language of choice you pick.