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 */
load_memory_management(); /* map in new current */
current = new;
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.