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.

Currently we have a more general implementation [http://www.cs.ucla.edu/~rxu/coupled.tgz coupled.tgz] that can couple two C statements together within a scope. However, we do not extend the C syntax to allow the code above. We use a keyword function void coupled() that if coupled() is called in the beginning of a block, then the next statement is the statement to be executed whenever the block is exited and the statement after next is the statement to be executed when the block is entered. A macro is used to make things look pretty. For example,

#define COUPLED(before, after) coupled(); after; before;

    do {
	COUPLED(lock(), unlock())
	error = something(); 
	if (error != 0)
	    break; 
	 error = something(); 
	 if (error != 0)
	    break;
	 error = something();
    } while (0);

Whenever the while block is entered, the first statement in COUPLED is executed: lock()}} in this case. Whenever the while block is exited, the second statement in {{{COUPLED is executed: unlock() in this case. The code is transformed to

while (1) {
  while_0_continue: /* CIL Label */ ;
  lock();
  error@main = something();
  if (error@main != 0) {
    {
    unlock();
    goto while_0_break;
    }
  }
  error@main = something();
  if (error@main != 0) {
    {
    unlock();
    goto while_0_break;
    }
  }
  error@main = something();
  {
  unlock();
  goto while_0_break;
  }
}
while_0_break: /* CIL Label */ ;
}

Note that there is now an unlock(); placed in front of each break statement. The current implementation just addresses the exit issue. It does not handle entrance to block from other means. For example, there could be a goto from elsewhere in the program that enters the block and that “goto” will not have acquired the lock. Although I think that case is rare, the next implementation will take account of that case.

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)
                        breakn(2);
        }
}

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

Cil can convert this to:

i@main = 0;
{
while (1) {
  while_0_continue: /* CIL Label */ ;
  if (! (i@main < 10)) {
    goto while_0_break;
  }
  j@main = 0;
  {
  while (1) {
    while_1_continue: /* CIL Label */ ;
    if (! (j@main < 10)) {
      goto while_1_break;
    }
    if ((*((*(a@main + i@main)) + j@main)) == 2) {
      {
      goto while_0_break; 
      }
    }
    j@main ++;
  }
  while_1_break: /* CIL Label */ ;
  }
  i@main ++;
}
while_0_break: /* CIL Label */ ;
}

Try it at [http://www.cs.ucla.edu/~rxu/breaks.tgz breaks.tgz]. Basically, call the function void blastn(int n) to break out of n levels. For more help, look at the example in ./test to figure out how to use it.

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.

The examples [http://www.cs.ucla.edu/~rxu/breaks.tgz breaks.tgz] and [http://www.cs.ucla.edu/~rxu/coupled.tgz coupled.tgz] are purely in the development stages and do not have a nice build system. To build and run these examples, first download Ocaml 3.08 which is available as a port and then download the [http://manju.cs.berkeley.edu/cil/ Cil] library. The installation for Ocaml should be straightforward. Cil needs to be built but the instructions (./configure; make; make quicktest) should work without a hitch.

To make the examples, you need to modify the Makefile. In Makefile, change COMPILEFLAGS to include the location of Cil. In Makefile.ocaml.build, change the directories to point to the location of Cil. After those modification, run make and the executables will be placed in ./obj. You can the run the executables on the *.c files in the ./test directory.

./obj/doCoupled.asm.exe ./test/coupled.c
./obj/doBreaks.asm.exe ./test/wiki.c

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

• Do a strawman Bitvector implementation. Try running it on ip_input
  • convert chunks of header files to use bit fields
• Use coupled and break(n) code in BSD somewhere.
• Get Cil to work with RELENG_6 GENERIC
  • Fix linking
  • Check warnings (chances are most are spurious)
• Get p4 branch setup

• Coupled statements within a block or scope

• How much time does it take extra to run GENERIC through Cil?
  • From Daniel, for 4.10 GENERIC kernel
  • Normal build: 221.177u 33.490s 4:47.93
  • CIL build w/ derefernce checking: 835.489u 143.103s 18:29.99
• Do a deadc0de check when dereferencing function pointers
• Break(n)
• Look into licensing issues
  • Ocaml Compiler is QPL and library is LGPL
  • Cil has a BSD License