Friday, November 13, 2009

19.6 Lockset Analysis













19.6 Lockset Analysis


Data races are hard to reveal with testing, due to nondeterministic interleaving of threads in a concurrent program. Statically exploring the execution space is computationally expensive, and suffers from the approximated model of computation, as discussed in Chapter 8. Dynamic analysis can greatly amplify the sensitivity of testing to detect potential data races, avoiding the pessimistic inaccuracy of finite state verification while reducing the optimistic inaccuracy of testing.


Data races are commonly prevented by imposing a locking discipline, such as the rule every variable shared between threads must be protected by a mutual exclusion lock. Dynamic lockset analysis reveals potential data races by detecting violation of the locking discipline.


Lockset analysis identifies the set of mutual exclusion locks held by threads when accessing each shared variable. Initially, each shared variable is associated with all available locks. When a thread accesses a shared variable v, lockset analysis intersects the current set of candidate locks for v with the locks held by that thread. The set of candidate locks that remains after executing a set of test cases is the set of locks that were always held by threads accessing that variable. An empty set of locks for a shared variable v indicates that no lock consistently protects v.



The analysis of the two threads in Figure 19.4 starts with two locks associated with variable x. When thread A locks lck1 to access x, the lockset of x is intersected with the locks hold by A. When thread B locks lck2 to access x, the intersection of the lockset of x with the current set of locks becomes empty, indicating that no locks consistently protect x.






Open table as spreadsheet














Thread



Program trace



locks held



lockset (x)



thread A



lock(lck1)
x=x+1;
unlock(lck1)



{ }
{lck1}



{lck1, lck2}
{lck1}



thread B



lock(lck2)
x=x+1;
unlock(lck2)



{ }
{lck2}
{ }



{ }






Figure 19.4: Threads accessing the same shared variable with different locks. (Adapted from Savage et al. [SBN+97])

This simple locking discipline is violated by some common programming practices: Shared variables are frequently initialized without holding a lock; shared variables written only during initialization can be safely accessed without locks; and multiple readers can be allowed in mutual exclusion with single writers. Lockset analysis can be extended to accommodate these idioms.


Initialization can be handled by delaying analysis till after initialization. There is no easy way of knowing when initialization is complete, but we can consider the initialization completed when the variable is accessed by a second thread.


Safe simultaneous reads of unprotected shared variables can also be handled very simply by enabling lockset violations only when the variable is written by more than one thread. Figure 19.5 shows the state transition diagram that enables lockset analysis and determines race reports. The initial virgin state indicates that the variable has not been referenced yet. The first access moves the variable to the exclusive state. Additional accesses by the same thread do not modify the variable state, since they are considered part of the initialization procedure. Accesses by other threads move to states shared and shared-modified that record the type of access. The variable lockset is updated in both shared and shared-modified states, but violations of the policy are reported only if they occur in state shared-modified. In this way, read-only concurrent accesses do not produce warnings.






Figure 19.5: The state transition diagram for lockset analysis with multiple read accesses.

To allow multiple readers to access a shared variable and still report writers' data races, we can simply distinguish between the set of locks held in all accesses from the set of locks held in write accesses.














No comments:

Post a Comment