Comments on Eraser

John fixed the minor mistake that was on slides 9 and 12. I would like to add some comments. Recall that two versions of the lockset algorithm are discussed in the Eraser paper. The simplest version, which does not use the state diagram in Figure 4, is used in slide 9. It detects a possible race condition since v is first protected by mu1, then by mu2, and there is no lock that is always held when v is written to. (In this context, let us assume that the "v:=1024" at the top is executed before Eraser starts operating, otherwise the simple version of the lockset algorithm would flag a warning right there.) The remarkable property of this algorithm is that it points out the possibility of a race condition for this code even if only a single thread executes this code.

On slide 12, the second version of the Eraser algorithm is used which will only flag errors if a variable was indeed shared and its candidate set is empty. That is why we assume there that thread T1 sets v to 1024, then thread T2 writes to v while holding mu1, which puts the variable in the shared-modified state. Once thread T1 writes to v while holding mu2, an error is flagged.

Note that this example is a bit contrived. You would be more likely to encounter this example in a form similar to this:

        function f() {
            lock(mu1); 
            v := v + 1;
            unlock(mu1); 
        }
        function g() {
            lock(mu2); 
            v := v + 1;
            unlock(mu2);)
        }
        function body() {
            f();
            g();
        }
        thread t1 = thread_create(body); 
        thread t2 = thread_create(body);

Here, the sequence is first executed in its entirety by one thread, and later another thread executes the same sequence. Eraser will detect a race condition in this less contrived scenario as well (think about how it would do it and what the states of v will be!)

Finally, the example shown on 16/17, which is one of the cases in which even the refined version of Eraser might miss a race condition, can be fixed by adding additional states, as suggested by Seragiotto. John shows the expanded state diagram in an expanded version of his slides (on Slide 22).