Modeling Memory Coherency during concurrent/simultaneous accesses
The presence of multiple actors that can concurrently modify and read memory complicates the problem of modeling and verifying memory coherency. Practically, it may not be feasible to precisely model the expected value of a memory location observed on a read when there are multiple concurrent writers/readers to the same memory location. In this paper, we develop a framework that can predict the multiple potential coherent values that could be observed upon a read when there are concurrent/simultaneous accesses to memory. Using the concept of window of uncertainty, we store all potential values in our memory model and remove values over time that are known incoherent, thereby verifying coherency even in the presence of uncertainty of outcomes.