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.