A Unifying Theory of Correct Concurrent Executions
Banu Özden, Avi Silberschatz · 1993
An ideal system is one that performs program operations in the order specified by the program and executes atomic program segments exclusively. Although this system model simplifies the task of reasoning about both sequential and concurrent programs, its straightforward implementation yields poor performance. To enhance performance, concurrency and pipelining techniques can be used, which may result in data accesses that are performed in an order which is different from the order specified by the program, which may result in incorrect executions. An execution is correct if its result is equivalent to the result that could have been obtained had the execution taken place on the ideal system. In this paper, we develop a unified general theory of correct executions where the access orders differ from the access order on the ideal system. Our unifying theory is applicable to a variety of programming paradigms, application domains, and architectures. It provides a verification tool to test the correctness of an execution, and allows us to devise more efficient protocols for various systems.