K comes from some discussions amongst some developers about how cool and or useful it would be to have language extensions that make it possible to write kernel code more cleanly and with less bugs. An example of this would be do have language support of linked lists, instead of mucking about in MACROspace.

One of the things I would like to be able to do is use the scoping of the language to help me get locking right, something like:

mutex(&sc→mtx) { error = something(sc); if (error != 0) break; error = something_else(sc); if (error != 0) break; error = last_thing(sc); } if (error != 0) return (error);

In this case the compiler will automatically release the mutex whenever the {…} block is exited, no matter how this happens.

Here's another idea with respect to scopes:

for(i = 0; i < 10; i++) { for (j = 0; j < 10; j++) { if (a[i][j] == 2) break(2); } }

Being able to say: “break out of two levels”

I would like a bitmap type, instead of the tedious #define THIS_ONE 0x0000001 #define THAT_ONE 0x0000002 I would prefer to be able to: bitmap { foo, bar, barf };

Structure packing control would be nice too:

struct foo { bigendian uint32_t magic @0; … };

Most CPUs have magic instructions for byte-order and alignment, there is no reason why the compiler can't do this for us.

In the debugging dept, an option to have the compiler watch out for 0xdeadc0de would be neat. Basically whenever a pointer contains something which looks like 0xdeadc0de, panic instead of going haywire. Similarly, avoid jumps through NULL pointers etc:

kcc -Wdeadcode -WNULLderef

And as was said above, in-language support for linked lists instead of macro-madness would be nice as well.

• [http://research.microsoft.com/os/singularity/ Microsoft Singularity] An operating system designed from scratch by both the systems people and the programming languages people at Microsoft Research

• E. Brewer, J. Condit, B. McCloskey, F. Zhou; [http://www.cs.berkeley.edu/~zf/papers/ivy-hotos05.pdf Thirty Years Is Long Enough: Getting Beyond C], HotOS X, 2005

• S Chandra, P McCann, [ftp://cm.bell-labs.com/cm/cs/who/chandra/pubs/packet-types.ps Packet Types] Sigcomm 2000 : Seems like a good basis to look at for bitvectors. It's probably has a bit more than we need but it's good start.

• D. Mandelin, L. Xu, R. Bodík, D. Kimelman [http://www.cs.berkeley.edu/~mandelin/ProspectorPLDI05.pdf Jungloids] PLDI 2005: Another way to deal with lotta API's or in our case lotta macro's

• Linux has [http://developer.osdl.org/dmo/sparse/ Sparse], some sort of static checker

• How much time does it take extra to run GENERIC through Cil?
• Run Ocaml / Cil on BSD
• Do a strawman Bitvector implementation. Try running it on ip_input
• Do a deadc0de check when dereferencing function pointers
• Get p4 branch setup
• Look into licensing issues
  • Ocaml Compiler is QPL and library is LGPL
  • Cil has a BSD License