Model checking a cache coherence protocol of a Java DSM implementation