| Autor: |
Paul E. McKenney, Mathieu Desnoyers, Michel Dagenais |
| Rok vydání: |
2013 |
| Předmět: |
|
| Zdroj: |
ACM SIGOPS Operating Systems Review. 47:51-65 |
| ISSN: |
0163-5980 |
| DOI: |
10.1145/2506164.2506174 |
| Popis: |
Modeling parallel algorithms at the architecture level enables exploring side-effects of the weakly ordered nature of modern processors. Formal verification of such models with model-checking can ensure that algorithm guarantees will hold even in the presence of the most aggressive compiler and processor optimizations. This paper proposes a virtual architecture to model the effects of such optimizations. It first presents the OoOmem framework to model out-of-order memory accesses. It then presents the OoOisched framework to model the effects of out-of-order instruction scheduling. These two frameworks are explained and tested using weaklyordered memory interaction scenarios known to be affected by weak ordering. Then, modeling of user-level RCU (Read- Copy Update) synchronization algorithms is presented. It uses the virtual architecture proposed to verify that the RCU guarantees are indeed respected. |
| Databáze: |
OpenAIRE |
| Externí odkaz: |
|
