what do we got to verify in an os?

From comments below.

Just one more comment: I think we should make a distinction between a tool that can verify threaded code and a tool that can verify the code that implements threading. The latter is what you are looking for here and it is much more difficult. Furthermore it is arguably unnecessary — a reasonable engineering solution is to get someone really good to write the dispatcher/scheduler and then focus verification effort on the mountains of code written by the rest of us that run on top of that core functionality.

I’m not so sure about that. The example below uses threading primitives – it does not implement them. We could even look at a more academic example and see the same problem.

threadA:
    while(1){
                  x = x+1;
                  sem_post(&z);
                  sem_wait(&t);
                  y = y+1;
   }
}
threadB:
   while(1){
       y = y+1;
       sem_post(&t);
       sem_wait(&z);
       x = x+1;
     }

My 20 second inspection tell me this ultra-simple example is right (which means it may have 100 errors). Prove it without having enough machinery to do the code below.

One thought on “what do we got to verify in an os?

  1. I believe that this code really is simpler to verify as it depends only on the semantics of the language and of the semaphore functions. Both of these are fairly tractable and are largely platform-independent. Given a mechanized semantics (which exists for C though not for pthreads, as far as I know) and a good interactive theorem prover I’d expect that you or I could prove the desired property (or falsify it) in minutes.

    On the other hand context switch code cannot be verified without a model of the register file, memory management hardware, and the interface between C and its underlying machine. Very difficult and very platform-dependent.

Comments are closed.