Taming release-acquire consistency
| Autor: | Viktor Vafeiadis, Nick Giannarakis, Ori Lahav |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Fence (finance)
Theoretical computer science Sequential consistency Programming language Computer science Consistency model 020207 software engineering 02 engineering and technology C11 computer.software_genre Operational semantics 020202 computer hardware & architecture Consistency (database systems) Fragment (logic) 0202 electrical engineering electronic engineering information engineering Memory model computer |
| Zdroj: | POPL |
| DOI: | 10.1145/2837614.2837643 |
| Popis: | We introduce a strengthening of the release-acquire fragment of the C11 memory model that (i) forbids dubious behaviors that are not observed in any implementation; (ii) supports fence instructions that restore sequential consistency; and (iii) admits an equivalent intuitive operational semantics based on point-to-point communication. This strengthening has no additional implementation cost: it allows the same local optimizations as C11 release and acquire accesses, and has exactly the same compilation schemes to the x86-TSO and Power architectures. In fact, the compilation to Power is complete with respect to a recent axiomatic model of Power; that is, the compiled program exhibits exactly the same behaviors as the source one. Moreover, we provide criteria for placing enough fence instructions to ensure sequential consistency, and apply them to an efficient RCU implementation. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|