|
To prove that a preemptive multithreaded system is working correctly, often some form of tracing is used. Most forms of tracing however are intrusive. The trace code influences the systems behavior in such a way that the result of the trace may not be considered proof of the systems correctness. There are a number of reasons for this. First, the added trace code influences the timing behavior of the system, trace statements take time. Especially when the system contains race conditions these might well go undetected because of the added cycles. With trace statements the system works correctly and without it doesn’t. But let’s assume there are no race conditions. The different threads making up the system are well synchronized and tracing is added to check whether the different threads are activated in the order as dictated by the design. Then another problem pops up. Most types of tracing use a shared resource. Take the most basic form, printf. This is used to write some diagnostic text to a file. Access to this file can not be preempted and therefore when using this type of tracing the printf statements must be executed atomically which is accomplished by using a mutex. The effect of this is that when two or more threads try to trace at the same moment, only one can continue and the others will be preempted. This changes the complete scheduling model of the system. Again, the trace is no proof of the systems correctness. Because printf does impose a relative large performance penalty, often use is made of some circular memory buffer. The threads place trace information in this buffer. This buffer however suffers from the same problem as the file used with printf. It is a shared resource which must be protected by a mutex, again ruining the scheduling. The final solution observed is that each thread is given its own buffer which prevents the aforementioned problem. The trace statements are then written with a time stamp and after the test run the contents of the different buffers is merged based on this time stamp. This has as a big disadvantage that it is complex to implement, uses a lot of system resources (time and memory) and still is not completely reliable since the resolution of the time stamps need to be very high in order to obtain a reliable model of the thread activation
Even if one succeeds in adding tracing while preventing the mentioned problems, still tracing in user code does often not provide the desired information. In principle a thread can be preempted at any point in the code. It might well be the preemption takes place just before the trace statement, making it look as if the thread ran at a later moment. Likewise the thread can be preempted immediately after the trace statement leading to the inverse problem. Often this is solved by adding many trace statements which in turn magnifies the aforementioned problems. The actual difficulty with this type of tracing is that it is added to user code and not to the scheduler itself. Only the scheduler has the correct information as when a thread is activated or deactivated. Top of page...
|