Updated below!
Years ago I proposed the following code snippet as a minimal standard for a useful verification method. Still not quite there.
/* you are not expected to understand this */
if(save()){
load_memory_management(); /* map in new current */
return;
}else {
current = new;
resume();
panic("RESUME RETURNED! KERNEL BROKENn");
}
Not so complicated, but if you can’t do this, you cannot handle operating systems at all- or any threading.
In response to the comment. This is a paraphrase of Dennis Ritchie’s Unix switch code and comment. “Save” saves the registers and the return address for “current” and always returns 0. “Resume” restores the saved registers and return address for current (by doing so, changes stacks) and returns 1 – to that saved return address which is the test of the “if”. So the “if” statement is always evaluated as false when saving and is always evaluated as true when resuming and “resume” never returns to the else. I always took Ritchie’s comment to be a warning that the code and the previous comments were not easy to understand. The state change here is basic thread switching but it is slippery.
Victor– I feel bad that I do not understand this famous old code fragment. I’m guessing that save() and resume() are part of the process dispatcher and that save() returns true on a direct return and false on indirect return?
What is the property to be verified — that panic() is unreachable? How much more code than this needs to be entrained before verification becomes possible? One problem with verifying code like this is that it may require a model both of C code and its underlying machine. Very tricky! It may be better to find a way to separately verify the machine-dependent and machine-independent parts.
See update to the post.
Thanks Victor. 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.