Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1145/2506164.2506174 | Operating Systems Review |
Keywords | Field | DocType |
parallel algorithm,ooomem framework,processor optimizations,rcu guarantee,formal verification,architecture level,user-level rcu,virtual architecture,out-of-order instruction scheduling,weaklyordered memory interaction scenario,out-of-order memory access,multi-core system,oooisched framework,model checking,multiprocessor,read copy update,shared memory | Instruction scheduling,Shared memory,Parallel algorithm,Computer science,Parallel computing,Read-copy-update,Real-time computing,Compiler,Systems modeling,Promela,Distributed computing,Formal verification | Journal |
Volume | Issue | Citations |
47 | 2 | 5 |
PageRank | References | Authors |
0.43 | 15 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mathieu Desnoyers | 1 | 58 | 4.89 |
| Paul E. McKenney | 2 | 279 | 30.11 |
| Michel R. Dagenais | 3 | 549 | 61.73 |